The Constraint kind

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 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 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, 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 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 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