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


11 Responses to “Constraint Kinds for GHC”

  • illissius Says:

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

  • Ivan Miljenovic Says:

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

  • illissius Says:

    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. :-)

  • Adam M Says:

    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?

  • Max Says:

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

  • Philip H Says:

    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?

  • Philip H Says:

    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?

  • Max Says:

    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.

  • Constraint kinds in Haskell, finally bringing us constraint families « ..never odd or even.. Says:

    [...] 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 [...]

  • Anders Kaseorg Says:

    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)

  • Max Says:

    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.