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