Title: The Constraint kind
Author: Wolfgang Jeltsch
Date: 14 February 2013
Tags: category theory, Constraint (kind), containers (Haskell
package), functional programming, GHC, Haskell,
Institute of Cybernetics, kind, literate programming,
monad, multi-parameter type class, talk, Theory Lunch,
type class, type family
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
write-up of my [Theory Lunch][theory-lunch] talk from
7\ February\ 2013. The source of this article is a literate
Haskell file, which you can [download][article-source] and load
into GHCi.
[theory-lunch]:
http://theorylunch.wordpress.com/
"Theory Lunch"
[article-source]:
http://darcs.wolfgang.jeltsch.info/blog/2013/02/14/the-constraint-kind.lhs
"The Constraint kind"
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 first-class 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][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.
[previous-post]:
http://jeltsch.wordpress.com/2013/02/09/some-interesting-features-of-haskells-type-system.lhs
"Some interesting features of Haskell’s type system"
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` through `k_n` is
a type of kind `k_1 -> k_n -> Constraint`.
* Each tuple type `(t_1, ..., t_n)` where `t_1` through `t_n`
are of kind `Constraint` is also of kind `Constraint` and
denotes the conjunction of `t_1` through `t_n`. As a corner
case, the nullary tuple type `()` is also of type
`Constraint` 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`{.haskell} 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`{.haskell} 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