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:

{-# LANGUAGE UndecidableInstances,
             MultiParamTypeClasses,
             KindSignatures,
             Rank2Types,
             ConstraintKinds,
             FlexibleInstances,
             OverlappingInstances #-}

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

Let’s have some imports as well:

import qualified Data.Set as S

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:

type Func cxt a = cxt a => a -> a
 
incc :: Func Num a
incc = (+1)

Or we can even use type synonyms as constraint synonyms:

type Stringy a = (Show a, Read a)
     
viaString :: Stringy a => a -> a
viaString = read . show

Simulating this without the extension is a little more cumbersome:

class (Show a, Read a) => Stringy a where
instance Stringy a where

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:

class RMonad m where
    type RMonadCtxt m a :: Constraint
    return :: RMonadCtxt m a => a -> m a
    (>>=) :: (RMonadCtxt m a, RMonadCtxt m b) => m a -> (a -> m b) -> m b

Lists can of course be an instance of this class:

instance RMonad [] where
    type RMonadCtxt [] a = ()
    return x = [x]
    (>>=) = flip concatMap

But now so can sets:

instance RMonad S.Set where
    type RMonadCtxt S.Set a = Ord a
    return = S.singleton
    mx >>= fxmy = S.fromList [y | x <- S.toList mx, y <- S.toList (fxmy x)]

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:

class RMonad m where
    type RMonadCtxt m a :: Constraint
    type RMonadCtxt m a = ()
    return :: ...
    (>>=) :: ...

(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:

data ShowDict a where
    ShowDict :: Show a => ShowDict a
     
showish :: ShowDict a -> a -> String
showish ShowDict x = show x
 
use_showish :: String
use_showish = showish ShowDict 10

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

data Dict ctxt where
    Dict :: ctxt => Dict ctxt
     
showish' :: Dict (Show a) -> a -> String
showish' Dict x = show x
 
use_showish' :: String
use_showish' = showish' Dict 10

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:

class (cxt a) => Data cxt a where
    gmapQ :: Proxy cxt -> (forall b. Data cxt b => b -> r) -> a -> [r]

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:

data Proxy (ctxt :: * -> Constraint) = Proxy

We can define Data instances for some built in types:

instance (cxt Int) => Data cxt Int where
    gmapQ _ f n = []
   
  instance (cxt [a], Data cxt a) => Data cxt [a] where
    gmapQ _ f [] = []
    gmapQ _ f (x:xs) = [f x, f xs]

Now we can define a generic function gsize:

class Size a where
    gsize :: a -> Int

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

instance Size Int where
    gsize x = x

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

instance Data Size t => Size t where
    gsize t = 1 + sum (gmapQ (Proxy :: Proxy Size) gsize t)

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:

use_gsize :: Int
use_gsize = gsize (1 :: Int) + gsize [1 :: Int, 2]

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.