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
About these ads

3 comments on “The Constraint kind

  1. […] I talked about the Constraint kind, a recent addition to Haskell. There is a write-up of my talk on my personal blog. […]

  2. 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?

    • 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 the ConstraintKinds, but also the TypeFamilies extension. ConstraintKinds is very new, and also TypeFamilies is not very old. So I suppose that this generalized Monad 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 uses Rank2Types.

When replying to another comment, please press that comment’s “Reply” button first.

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s