### Constraint kinds in Haskell, finally bringing us constraint families

#### by dorchard

Back in 2009 Tom Schrijvers and I wrote a paper entitled *Haskell Type Constraints Unleashed* [1] which appeared at FLOPS 2010 in April. In the paper we fleshed out the idea of adding *constraint synyonyms* and *constraint families* to GHC/Haskell, building upon various existing proposals for *class families*/*indexed constraints*. The general idea in our paper, and in the earlier proposals, is to add a mechanism to GHC/Haskell to allow constraints, such as type class or equality constraints, to be indexed by a type in the same way that type families and data families allow types to be indexed by types.

As an example of why constraint families are useful, consider the following type class which describes a simple, polymorphic, embedded language in Haskell (in the “*finally tagless*“-style [2]) (this example appears in [1]):

class Expr sem where constant :: a -> sem a add :: sem a -> sem a -> sem a

Instances of `Expr` provide different evaluation semantics for the language. For example, we might like to evaluate the language for numerical values, so we might try and write the following instance:

data E a = E {eval :: a} instance Expr E where constant c = E c add e1 e2 = E $ (eval e1) + (eval e2)

However, this instance does not type check. GHC returns the type error:

No instance for (Num a) arising from a use of `+' In the second argument of `($)', namely `(eval e1) + (eval e2)' ...

The `+` operation requires the `Num a` constraint, yet the signature for `add` states no constraints on type variable `a`, thus the constraint is never satisfied in this instance. We could add the `Num a` constraint to the signature of `add`, but this would restrict the polymorphism of the language: further instances would have this constraint forced upon them. Other useful semantics for the language may require other constraints e.g. `Show a` for pretty printing. Should we just add more and more constraints to the class? By no means!

*Constraint families*, as we describe in [1], provide a solution: by associating a constraint family to the class we can vary, or *index*, the constraints in the types of `add` and `constant` by the type of an instance of `Expr`. The solution we suggest looks something likes:

class Expr sem where constraint Pre sem a constant :: Pre sem a => a -> sem a add :: Pre sem a => sem a -> sem a -> sem a instance Expr E where constraint Pre E a = Num a ... -- methods as before

`Pre` is the name of a constraint family that takes two type parameters and returns a constraint, where the first type parameter is the type parameter of the `Expr` class.

We could add some further instances:

data P a = P {prettyP :: String} instance Expr P where constraint Pre P a = Show a constant c = P (show c) add e1 e2 = P $ prettyP e1 ++ " + " ++ prettyP e2

e.g.

*Main> prettyP (add (constant 1) (constant 2)) "1 + 2"

At the time of writing the paper I had only a prototype implementation in the form of a preprocessor that desugared constraint families into some equivalent constructions (which were significantly more awkward and ugly of course). There has not been a proper implementation in GHC, or of anything similar. Until now.

At CamHac, the Cambridge Haskell Hackathon, last month, Max Bolingbroke started work on an extension for GHC called “constraint kinds”. The new extensions unifies types and constraints such that the only distinction is that constraints have a special *kind*, denoted `Constraint`. Thus, for example, the |Show| class constructor is actually a type constructor, of kind:

Show :: * -> Constraint

For type signatures of the form `C => t`, the left-hand side is now a type term of kind `Constraint`. As another example, the equality constraints constructor `~` now has kind:

~ :: * -> * -> Constraint

i.e. it takes two types and returns a constraint.

Since constraints are now just types, existing type system features on type terms, such as synonyms and families, can be reused on constraints. Thus we can now define *constraint synonyms* via standard type synonms e.g.

type ShowNum a = (Num a, Show a)

And most excitingly, *constraint families* can be defined via type families of return kind `Constraint`. Our previous example can be written:

class Expr sem where type Pre sem a :: Constraint constant :: Pre sem a => a -> sem a add :: Pre sem a => sem a -> sem a -> sem a instance Expr E where type Pre E a = Num a ...

Thus, `Pre` is a type family of kind `* -> * -> Constraint`. And it all works!

The constraint kinds extension can be turned on via the pragma:

{-# LANGUAGE ConstraintKinds #-}

Max 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 be hitting the streets with version 7.4 of GHC. But if you can’t wait it is already in the GHC HEAD revision so you can checkout a development snapshot and give it a whirl.

In my next post I will be showing how we can use the constraint kinds extension to describe abstract structures from category theory in Haskell that are defined upon *subcategories*. I already have a draft note about this (edit July 2012: draft note subsumed by my TFP 2012 submission)

submission if you can’t wait!

** **

### References

[1] Orchard, D. Schrijvers, T.: *Haskell Type Constraints Unleashed*, FLOPS 2010, [author’s copy with corrections] [On SpringerLink]

[2] Carrete, J., Kiselyov, O., Shan, C. C.: *Finally Tagless, Partially Evaluated*, APLAS 2007

From the draft paper: “If a type class of only endofunctors restricted to Hask is still required a definition similar to the original Functor type class, perhaps named EndoFunctor, can still be provided.”

With a small change to the definition of SubCat, EndoFunctor can be recovered automatically:

class Hask a

instance Hask a

class Functor f where

type SubCat f :: * -> Constraint

type SubCat f = Hask

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

instance Functor [] where

fmap = map

instance Functor S.Set where

type SubCat S.Set = Ord

fmap = S.map

type EndoFunctor f = (Functor f, SubCat f ~ Hask)

I don’t think this loses any expressive power, although it makes some details more annoying. Instead of writing

type SubCat Foo a = (Read a, Show a)

we now have to write a new class (not even a type synonym, since type synonyms can’t be partially applied):

class (Read a, Show a) => ReadShow a

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

type SubCat Foo = ReadShow

Cool example, thanks!

Note that (~) is actually kind-polymorphic, rather than having just the concrete kind * -> * -> Constraint; it is valid to write things such as (Maybe ~ f). Currently this is just a baked-in special treatment of (~), but soon (http://hackage.haskell.org/trac/ghc/wiki/GhcKinds) we hope to have more general kind polymorphism.

@Brent:

Thanks. Exciting stuff, I had heard on the grapevine that kind polymorphism is on the way.

So does this mean the kind of (~) is:

`(~) :: forall k . k -> k -> Constraint`

Similarly for tupling?:

`(,) :: forall k . k -> k -> k`

Incidentally, when Max started on the constraint kinds extension at the Hackathon we had a long discussion about having kind variables and extending the kind hierarchy to group different kinds together into sorts, e.g. types and constraints are of one sort (that say, permit tupling), but unboxed types are of another. Ultimately we abandoned going down that road for simplicity, and so GHC lies to you (or at least is selective with the truth!) when you ask what is the kind of (~) or (,).

@anderskaseorg:

Thanks for the comment. I really like the idea.

Sadly, I’m not sure if it is worth it, as having to write extra classes, in order to allow partially applied constraints, is fairly inelegant.

Perhaps a language solution would be to separate the parameters of a type family into indices and parameters. For example:

type family SubCat f | a :: Constraint

is a type family of kind :: * -> * -> Constraint where “f” is an index of the SubCat family and “a” is a type parameters; the pipe character ‘|’ separates indices form type parameters.

Thus, SubCat must be fully-applied in its indices, but can be partially applied in its type parameters. For example, the following is valid:

type EndoFunctor f = (Functor f, SubCat f ~ Hask)

because SubCat has fully applied indices, but the following is not:

type Foo = SubCat

Instances could look like:

instance family SubCat F | a = ....

but multiple instances for different instantiations of “a” would not be allowed. I think this would be a pretty useful extension for type families.

Do we need to invent new syntax for this, or could we just make

type family SubCat f :: * -> Constraint

type instance SubCat F a = (Show a, Read a)

do the right thing?

Answering my own question, apparently no:

http://hackage.haskell.org/trac/ghc/ticket/3714#comment:4

Yes, you might be right. I don’t think this would be a big deal i.e. I don’t think this would cause any problems in the type checker.

Ok on reflection I take it all back. I suppose this would allow type-level lambda which is difficult in the context of the GHC type checker (see: http://comments.gmane.org/gmane.comp.lang.haskell.cafe/68653)

Humph.

[…] my previous post I discussed the new constraint kinds extension to GHC, which provides a way to get type-indexed […]

Have you noticed that the prettyP example doesn’t type check?

I have also noticed that.

Thank you Dominic and Clifford. I have finally fixed this.