Constraint kinds in Haskell, finally bringing us constraint families

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 :: a}

instance Expr P where
    constraint Pre P a = Show a
    constant c = P c
    add e1 e2 = P $ prettyP e1 ++ prettyP e2

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

About these ads

10 thoughts on “Constraint kinds in Haskell, finally bringing us constraint families

  1. anderskaseorg

    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

    Reply
    1. dorchard Post author

      @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 (,).

      Reply
  2. dorchard Post author

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

    Reply
    1. anderskaseorg

      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?

      Reply
      1. dorchard Post author

        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.

  3. Pingback: Subcategories & “Exo”functors in Haskell « ..never odd or even..

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s