I recently implemented a powerful new extension to GHC HEAD called ConstraintKinds. This (Literate Haskell) post will explain what this means, and how we can exploit it to do some cool stuff.

(For long-time readers, this stuff is a generalisation of my earlier post about constraint families which was later also expounded on by Dominic Orchard and Tom Schrijvers in Type Constraints Unleashed. The proposal in its current form is due to Conor McBride.)

First of all, we’re going to turn on a whacking great load of extensions:

(Yes, some of the cooler examples will require UndecidableInstances. Never mind!)

Let’s have some imports as well:

When we talk about constraints in Haskell, we usually mean one of the following things:

• Class contexts such as Show a
• Implicit parameters, such as ?x::Int
• Equality assertions, such as a ~ Int
• Tuples of any of the above, such as (Show a, Read a)

Is standard Haskell, these constraints can only occur to the left of => arrow, and they are the only thing that can appear there. With the ConstraintKinds extension, we instead allow any type of a brand-new kind Constraint to appear to the left of =>. Naturally, all of the constraints we already mentioned are parsed as types, and are all given an appropriate kind:

• Show :: * -> Constraint
• (?x::Int) :: Constraint
• (a ~ Int) :: Constraint
• (Show a, Read a) :: Constraint

## Constraint synonyms

At the simplest level, this unification of constraints and types means that code like the following is valid:

Or we can even use type synonyms as constraint synonyms:

Simulating this without the extension is a little more cumbersome:

## Indexed constraints

But it doesn’t stop there. Since constraints are just types, we can type-index them using type functions! We can use this to solve the well-known problem where lists can be an instance of the Monad type class, but sets cannot. This problem arises because the elements of a set must be orderable, but e.g. the return method of the Monad class allows an element of any type to be made into an “element” of the monad — not only the orderable ones.

A restricted monad is a monad where we need to impose some constraints on the elements it can contain. Existing Hackage packages such as Ganesh Sittampalam’s rmonad package provide a way to define these monads in unextended Haskell. However, with our new extension we get a much smoother user experience by reusing the type function mechanism to encode a class of restricted monads:

Lists can of course be an instance of this class:

But now so can sets:

Another feature I added to GHC recently is associated type defaults. With this, we can change the RMonad class definition so that normal Monads which do not make any special demands of their element types can be defined without giving an explicit instance for RMonadCtxt:

(Associated type defaults were always described in the published papers about associated types, but were never implemented until now).

## Reified dictionaries

A common trick is to reify a constraint as an explicit dictionary using a GADT:

With our extension we can generalise this so you can define one reified dictionary to rule them all:

## Generic programming

In “Scrap Your Boilerplate With Class”, Simon Peyton Jones and Ralf Laemmel proposed an encoding for generic functions in terms of type classes. However, their presentation was impeded by the fact that they could not abstract over type classes, and they had to have a heavy encoding mechanism to make it work. With our new extension we can write generic functions in their style in a much cleaner fashion.

First, we define the class of Data which has a generic mapping operation that applies a type-indexed function one level down in the data structure, returning all the results as a list:

The cxt type variable will later be instantiated to a type class corresponding to the generic function we wish to apply. The Proxy cxt argument to gmapQ is an unfortunate artifact of fact that Haskell still has no explicit type applications, so we have to use dummy value arguments to disambiguate which cxt we actually mean when we call gmapQ. The definition is trivial:

We can define Data instances for some built in types:

Now we can define a generic function gsize:

We can say how gsize works on particular types by giving an instance:

If no other instance is available, an overlapping instance based on gmapQ will be used:

We can now evaluate gsize at both types Int and [Int] even though we never said explicitly what it means to take the size of a list:

## Wrapping up

The ConstraintKinds extension makes these three idioms much neater, but I’m sure there are plenty of other places where this new power will come in useful. Try it out for yourself in GHC 7.4 and find out!

Thanks are due to Simon Marlow for organising CamHac, where I started working on the implementation, and Dominic Orchard and Nicolas Wu who collaborated with me during the early stages of coding. Thanks also to Simon Peyton Jones for invaluable advice that finally let me merge it into GHC.