GADT allows us to reify a constraint as an explicit dictionary. With ConstraintKinds, we can further generalize this trick. In this post, I will explain how this trick works.

In his article, Constraint Kinds for GHC, Max Bolingbroke showed a trick of reifying a constraint as an explicit dictionary using a GADT:

{-# LANGUAGE GADTs #-}

data ShowDict a where
  ShowDict :: Show a => ShowDict a

showish :: ShowDict a -> a -> String
showish ShowDict x = show x

use_showish :: String
use_showish = showish ShowDict 10

How does this trick work? GADTs extension plays an essential role here. When GADTs is enabled, a type-class context given in the constructor is available by pattern matching. In this example above, pattern matching on ShowDict makes the Show a type-class context available in the body of the showish function.

Operationally, the ShotDict constructor has a hidden field that stores the (Show a) dictionary that is passed to ShowDict; so when pattern matching that dictionary becomes available for the right-hand side of the match. Section 9.4.7 of the GHC user guide explains this behavior in details.

We can observe the (Show a) dictionary instance hidden in the constructor by dumping the GHC simplifier output. Pattern matching on the constructor reveals the hidden dictionary $dShow_aKG as follows.

showish_roY :: forall a_ayV. ShowDict a_ayV -> a_ayV -> String
[GblId, Arity=2, Caf=NoCafRefs, Str=DmdType]
showish_roY =
  \ (@ a_aKE) (ds_d10M :: ShowDict a_aKE) (x_ayW :: a_aKE) ->
    case ds_d10M of _ [Occ=Dead] { ShowDict $dShow_aKG ->
    show @ a_aKE $dShow_aKG x_ayW
    }

With ConstraintKinds extension, we can further generalize this idea by passing an arbitrary context to the constructor.

{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE GADTs #-}

data Dict ctxt where
  Dict :: ctxt => Dict ctxt

showish' :: Dict (Show a) -> a -> String
showish' Dict x = show x

use_showish' :: String
use_showish' = showish' Dict 10

In this blog post, I will show some examples of using the ConstraintKinds GHC extension.

Constraints

Constraints in Haskell mean one of the following things:

• Class constraints, e.g. Show a
• Implicit parameter constraints, e.g. ?x::Int (with the -XImplicitParams flag)
• Equality constraints, e.g. a ~ Int (with the -XTypeFamilies or -XGADTs flag)
• Tuples of any of the above, e.g., (Show a, a ~ Int)

These constraints can only occur to the left of => arrow in standard Haskell.

Kinds

In Haskell, types have types which are called kinds.

• The kind * is for types that have terms (even though not every type of kind * needs be inhabited if we exclude ⊥).
• k -> l forms a function kind to indicate types of kind l that are parameterized over types of kind k.

Examples:

• kind *: Char, Bool, Char -> Bool, Maybe Int, [Int]
• kind * -> *: Maybe, []
• kind * -> * -> *: Either, (,)

While data introduces types of kind *, classes introduce types of kind Constraint.

• Classes such as Show, Eq or Ord are of kind * -> Constraint. They form a class constraint when applied to types of kind *.
• Classes such as Functor or Monad are of kind (* -> *) -> Constraint. They form a class constraint when applied to type constructors of kind * -> *.

We can use tuple syntax to create empty constraints and combine constraints.

type NoConstraint = (() :: Constraint)
type Text a = (Read a, Show a)

ConstraintKinds

Classes and contexts were not first-class citizens in Haskell, but the introduction of the Constraint kind has changed this and allows them to be used as parameters of types.

{-# LANGUAGE ConstraintKinds #-}

With this extension, constraints can be used in new ways:

• Aliases of classes, partially applied classes, and contexts can be defined using type declarations
• Families of classes, partially applied classes, and contexts can be defined using type synonym families

Let’s visit each use case with concrete examples.

Constraint synonyms

Since constraints are now just types, type synonyms can be reused on constraints.

type Text a = (Show a, Read a)

Here is a real world example of constraint synonyms defined in the Haskell Tool Stack.

-- | Constraint synonym for all of the common environment instances
type HasEnv r = (HasLogOptions r, HasTerminal r, HasReExec r, HasSticky r)

-- | Constraint synonym for constraints commonly satisifed by monads used in stack.
type StackM r m =
    (MonadReader r m, MonadIO m, MonadBaseControl IO m, MonadLoggerIO m, MonadMask m, HasEnv r)

Or we can define Func in terms of two type arguments ctx and a where ctx is a context of kind * -> Constraint.

type Func cxt a = cxt a => a -> a

inc :: Func Num a
inc = (+1)

Constraint families

Constraint families allow constraints to be indexed by a type in the same way that type families and data families allow types to be indexed by types.

For example, constraint families let us define a generalized version of the Monad class where we can impose some constraints on the element it can contain. Wolfgang Jeltsch’s The Constraint kind and Max Bolingbroke’s Constraint Kinds for GHC explain this classic example in details.

rmonad provides a collection of restricted monads based on associated datatypes.

class RMonad m where
  type RMonadCtxt m a :: Constraint
  type RMonadCtxt m a = ()

  return :: RMonadCtxt m a => a -> m a
  (>>=) :: (RMonadCtxt m a, RMonadCtxt m b) => m a -> (a -> m b) -> m b

instance RMonad S.Set where
  type RMonadCtxt S.Set a = Ord a
  return = S.singleton
  mx >>= fxmy = S.fromList [y | x <- S.toList mx, y <- S.toList (fxmy x)]      

instance RMonad [] where
  return x = [x]
  (>>=) = flip concatMap

Algorithm W is the best known algorithm for implementing Hindley-Milner type inference. But it is a bit complicated as it intermingles two separate processes: constraint generation and solving.

There is an alternative approach based on constraints generation. In this approach, constraints are collected by bottom-up traversal, and then solved independently. Heeren’s Generalizing Hindley-Milner Type Inference Algorithms paper describes the algorithm in details.

Here’s my implementation of Heeren’s algorithm. I forked Stephen Diehls’s Poly and modified the type checker to use the Heeren’s algorithm.