## Constraint Kinds for GHC

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 `Monad`

s 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.

September 10th, 2011 at 10:27 pm

This is the most exciting new extension to GHC/Haskell since I've been using it. By quite a margin. I'm still trying to wrap my head around the kind of things it would enable.

(Granted, that's only since 6.12... but it'd likely stay true even if I'd been around longer.)

September 10th, 2011 at 10:49 pm

I _definitely_ like the Constraint Synonyms!

I'm also intrigued by how you can implement RMonad without the withConstraintsOf and withResConstraints functions (though you still have the convoluted type signature happening, though I suppose that's unavoidable...).

September 10th, 2011 at 10:51 pm

Here's another idiom it lets you generalise:

data Some (cls :: * -> Constraint) where

Some :: forall a. cls a => a -> Some cls

instance Show (Some Show) where

show (Some a) = show a

It's too bad you can't abstract over the instance declarations.

September 14th, 2011 at 7:53 pm

Wow, this sounds great. Is it scheduled to be part of the official GHC 7.4?

Also, does this mean that you've introduced a third production in the in System FC2 grammar for Kinds? Currently it has * and k~>k as the only alternatives where k1~>k2 is (basically) the kind of (forall a::k1 . (t::k2)). It sounds like this would add k1==>k2 which is the kind of (a::k1 => (t::k2)). Or are the two kinds actually the same?

September 14th, 2011 at 9:11 pm

Adam: it's not that complicated! It just adds the base kind Constraint to the grammar of kinds. This is a kind of types inhabited by values, just like the existing kinds * and #.

September 21st, 2011 at 3:06 pm

I've been waiting for this feature for quite a while, now, so thank you very much for implementing it!

I wanted to experiment with a prelude that has a few improvements over the standard one, but break backward compatibility (stuff like adding Applicative as a constraint on the Monad class). I figured I would immediately implement Functor, Monad, et al. using your RMonad strategy. I did this in the GHC source tree (base/GHC/Base.lhs) defining Functor as:

class Functor f where

type FunctorCtxt f a :: Constraint

type FunctorCtxt f a = ()

fmap :: (FunctorCtxt f a, FunctorCtxt f b) => (a -> b) -> f a -> f b

However, this causes an interface file error:

Declaration for R:FunctorCtxt[]a:

Iface type variable out of scope: a

Cannot continue after interface file error

Maybe this isn't the best forum for bug-reports, but I thought I would let you know I ran into this. Am I doing something wrong, or should I set up a ticket?

September 21st, 2011 at 4:18 pm

Oops... I'm a bit ashamed now; it seems I just broke something in the build-tree of GHC. If I use the definition for Functor as in my previous post, but in a 'local' module, no such interface error occurs.

You couldn't possibly point me into the direction of the ghc-tree where I broke things, could you?

September 21st, 2011 at 4:45 pm

Philip: my first thought was that this was caused by the fact that the Functor/fmap names are wired-in to GHC and it may make some assumptions about what their type signatures actually are.

(See PrelNames.lhs for the list of wired-in names)

However, consulting the source code I can't immediately see any such violated assumptions (at least in the code you are likely to be writing - monad comprehensions *may* be broken by your change). So perhaps file a ticket?

You should probably experiment with your new prelude outside of the base library first - this will be easier since you won't have to worry about breaking GHC's assumptions. You can use NoImplicitPrelude to replace the standard prelude with your own.

September 22nd, 2011 at 10:45 am

[...] has written about the extension over at his blog, which has some more examples, so do go check that out. As far as I am aware the extension should [...]

September 28th, 2011 at 2:50 am

This is very exciting stuff!

I note that type synonyms don’t work quite as well as constraint synonyms should, because type synonyms can’t be partially applied:

type Stringy a = (Show a, Read a)

type Stringiest = Stringy

-- (error: Type synonym `Stringy' should have 1 argument, but has been given none)

class Stringy a => Stringier a

instance Stringy a => Stringier a

type Stringiest = Stringier

-- (works)

September 28th, 2011 at 6:21 am

Yes, the lack of partial application can be annoying. A workaround is to use a trivial class declaration:

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

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

This is analogous to having to use a newtype declaration if you want to partially apply a type synonym.