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:
(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 Monad
s 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.
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?
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.
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?
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.)
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...).
Yes, the lack of partial application can be annoying. A workaround is to use a trivial class declaration:
This is analogous to having to use a newtype declaration if you want to partially apply a type synonym.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?
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 #.
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. :-)
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)