A recent language extension of the Glasgow Haskell Compiler (GHC) is the Constraint
kind. In this blog post, I will show some examples of how this new feature can be used. This is a writeup of my Theory Lunch talk from 7 February 2013. The source of this article is a literate Haskell file, which you can download and load into GHCi.
Prerequisites
The example code in this article needs support for the Constraint
kind, of course. So we have to enable the appropriate language extension (which is surprisingly called ConstraintKinds
instead of ConstraintKind
). Furthermore, we want to make use of type families. All in all, this leads to the following LANGUAGE
pragma:
{# LANGUAGE ConstraintKinds, TypeFamilies #}
We will define our own version of the Monad
class. Therefore, we have to hide the Monad
class from the Prelude:
import Prelude hiding (Monad (..))
We will need the module Data.Set
from the containers
package for some example code:
import Data.Set
Last, but not least, we have to import the kind Constraint
:
import GHC.Exts (Constraint)
The general picture
Originally, classes and contexts were not firstclass citizens in Haskell. The introduction of the Constraint
kind has changed this. Classes and contexts can now be used as parameters of types, for example. This is because they are now types themselves.
However, classes and contexts are still not types in the strict sense. There are still no values of type Eq
or Eq Integer
, for example. As I have explained in my previous post, Haskell’s notion of type is more general than the usual one. In particular, functions on types are types themselves. However, they are not types of kind *
. The same holds for classes and contexts. They are not types of kind *
, but they are types of some other kinds, so that they can generally be used in places where types can be used.
The new kind Constraint
, which is exported by GHC.Exts
, is the kind of all contexts. Classes and contexts are now handled as follows:

Each class with parameters of kinds
k_1
throughk_n
is a type of kindk_1 > k_n > Constraint
. 
Each tuple type
(t_1, ..., t_n)
wheret_1
throught_n
are of kindConstraint
is also of kindConstraint
and denotes the conjunction oft_1
throught_n
. As a corner case, the nullary tuple type()
is also of typeConstraint
and denotes the constraint that is always true. 
A context can be any type of kind
Constraint
.
These rules guarantee that classes and contexts can be used as before. For example, (Read val, Show val)
is still a context, because Read
and Show
are types of kind * > Constraint
, so Read val
and Show val
are types of kind Constraint
, and therefore (Read val, Show val)
is a type of kind Constraint
.
However, classes and constraints can be used in new ways now. Here are some examples:

Classes can be partially applied, and the results can be used like classes again.

Classes, partially applied classes, and contexts can be parameters of types and instances of classes.

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.
In the remainder of this article, I will illustrate the last two of these points.
Context aliases
Sometimes, the same conjunction of several contexts appears in multiple types. In such cases, it can become cumbersome to always write these conjunctions explicitly. For example, there might be several functions in a library that deal with values that can be turned into strings and generated from strings. In this case, the types of these functions will typically have a context that contains constraints Show val
and Read val
. With the Constraint
kind, we can define context aliases Text val
as follows:
type Text val = (Show val, Read val)
Instead of Show val, Read val
, we can now simply write Text val
in contexts.
A few years ago, there was an attempt to implement support for context aliases (often called class aliases) in GHC. With the Constraint
kind, this is now obsolete, as context aliases are now just a special kind of type aliases.
Context families
We will illustrate the use of context families by defining a generalized version of the Monad
class.
The actual definition of a monad from category theory says that a monad on a category 𝒞 consists of an endofunctor on 𝒞 and some natural transformations. In Haskell, however, a monad is defined to be an instance of the Monad
class, which contains the two methods return
and (>>=)
. Haskell monads are monads on the category Hask, the category of kind*
types and functions.
There are monads in the category theory sense that are almost monads in the Haskell sense, but not quite. One example is the monad behind Haskell’s Set
type. There are reasonable implementations of return
and (>>=)
for Set
:
setReturn :: el > Set el
setReturn = singleton
setBind :: (Ord el, Ord el') =>
Set el > (el > Set el') > Set el'
setBind set1 gen2 = unions (Prelude.map gen2 (toList set1))
The problem is that the type of setBind
is too restrictive, as it restricts the choice of element types by a context, whereas there is no such restriction in the type of (>>=)
. The reason for the restriction on element types is that the Set
monad is not a monad on the category Hask, but on the full subcategory of Hask whose objects are the instances of Ord
.
Using context families, we can generalize the Monad
class such that restrictions on the type parameters of Monad
instances become possible. We introduce a type synonym family Object
such that Object mon val
is the constraint that the parameter val
must fulfill when working with the Monad
instance mon
. We provide a default definition for Object
that does not restrict monad parameters. Finally, we change the types of return
and (>>=)
such that they restrict their Monad
instance parameters accordingly. The new declaration of the Monad
class is as follows:
class Monad mon where
type Object mon val :: Constraint
type Object mon val = ()
return :: Object mon val =>
val > mon val
(>>=) :: (Object mon val, Object mon val') =>
mon val > (val > mon val') > mon val'
We can now make Set
an instance of Monad
:
instance Monad Set where
type Object Set el = Ord el
return = setReturn
(>>=) = setBind
We can make every instance of the original Monad
class an instance of our new Monad
class. Because of the default definition of Object
, we do not need to define Object
in these cases. So the instance
declarations can look exactly like those for the original Monad
class. Here is an example for the []
type:
instance Monad [] where
return x = [x]
(>>=) = flip concatMap
Pingback: The Constraint kind  Theory Lunch
This is a really informative post; thank you for writing it. I don’t tend to comment much because my Haskell knowledge is at a level where I don’t have much to add to the dialogue, but I just wanted to express my appreciation for your blog, I’ve learnt a great deal from following it.
The example you give of generalizing the Monad type class is fantastic, as it seems to have no downsides, since any previously allowable instance can use the existing instance definition. Apart from the dependence on ConstraintKinds, is there any negative to this Monad definition? Is there any movement to thus generalize it? If not, why not? A reluctance to rely on an extension for a base library?
LikeLike
It is nice to hear that you like my blog. Thank you for expressing your appreciation.
The
Monad
class given (but not invented) by me uses not only theConstraintKinds
, but also theTypeFamilies
extension.ConstraintKinds
is very new, and alsoTypeFamilies
is not very old. So I suppose that this generalizedMonad
class will not make it into base very soon. We would have to ask the folks on the GHC or the library mailing list to know for sure.That said, relying on extensions for base does not seem to be a problem as such, as base is already beyond standard Haskell. For example,
Control.Monad.ST
usesRank2Types
.LikeLike
Pingback: Constrained monads « Wolfgang Jeltsch
Nice. I grokked everything except the last 3 words of this sentence:
Does it mean that “contexts can be parameters of instances of classes”? Or does it mean that “contexts can be instances of classes”? Either way I’d appreciate some elaboration.
LikeLike
It means that contexts can be parameters of types and that they can also be instances of classes.
T
of kindConstraint > *
. Then you can applyT
to(Read a, Show a)
, for example, resulting in the typeT (Read a, Show a)
of kind*
.instance C T where […]
is not an instance, and it also does not define an instance. Instead, it makes the typeT
and instance of the classC
. Types are instances of classes. So when I said that contexts can be instances of classes, I meant that you can have, for example, an instance declarationinstance C (Read a, Show a) where […]
, meaning thatC
must have kindConstraint > Constraint
.LikeLike
Did you mean “can’t generally be used”?
LikeLike
No, I meant that they can generally be used in places where types can be used, since, while not being types of kind
*
, they are types of some other kinds. So they can be used as parameters of types and instances of classes, for example. The only place where they cannot be used, but types of kind*
can, are type annotations. For example, you cannot writex :: Eq
.LikeLike