Control.Category: now with kind polymorphism

Just a quick update.

The other day, I pushed a patch to the Haskell base library that will enable kind polymorphism for the Category type class. That change will come to the public when GHC 7.8.1 is released.

This is a simple change that makes Category far more general, while not breaking any code already out there. (The change was originally proposed by none other than Edward Kmett, although he’s not the only one wanting it.)

Out with the old, in with the new

The typical definition of Category looks like:

class Category cat where
  id  :: cat a a
  (.) :: cat b c -> cat a b -> cat a c

Which is all great. But there’s a problem with this. By default, the type variable cat has a kind something like (cat :: * -> * -> *) - meaning a Category can only be created from types where a and b are of kind *.

This isn’t very rich or expressive. In fact, there are many legal Category instances which cannot be created with the above definition, as the parameters (a and b) are of a more exotic kind - for example, not of kind * but of kind (*,*) - the kind of promoted tuples.

Luckily for us, GHC has kind polymorphism. So we just needed to enable it. This is a completely backwards compatible change as well.

With that little addition of LANGUAGE PolyKinds, we can now host much richer instances of Category. With -XPolyKinds, kind generalization occurs automatically. So at pretty much no cost, the change turned:

class Category (cat :: * -> * -> *) where

into:

class Category (cat :: k -> k -> *) where

where the k stands for a kind variable, and can be instantiated to various new kinds, not just *.

In GHC 7.8, if you ask for the kind of Category, you will get:

Prelude> import Control.Category
Prelude Control.Category> :i Category
class Category (k :: BOX) (cat :: k -> k -> *) where
  Control.Category.id :: cat a a
  (Control.Category..) :: cat b c -> cat a b -> cat a c
       -- Defined in ‛Control.Category’
instance Category * (->) -- Defined in ‛Control.Category’
Prelude Control.Category> :k Category
Category :: (k -> k -> *) -> Constraint
Prelude Control.Category>

(For the curious: the (k :: BOX) annotation cannot be given explicitly, and is a form introduced as a result of PolyKinds, where kind parameters are introduced ‘implicitly’ in their definition.)

Logical entailment

There’s a simple instance of Category which we already know and love: the instance for function types. Let the type variable cat become (->) and we get:

id :: cat a a
  = { given the equality, cat = (->) }
id :: (->) a a
  = { by syntactic equality }
id :: a -> a

(.) :: cat b c -> cat a b -> cat a c
  = { given the equality, cat = (->) }
(.) :: ((->) b c) -> ((->) a b) -> ((->) a c)
  = { by syntactic equality }
(.) :: (b -> c) -> (a -> b) -> (a -> c)

And these are the regular types of Prelude.id and (Prelude..), so:

instance Category (->) where
  id  = Prelude.id
  (.) = (Prelude..)

Another example Edward brought up though, is logical entailment (or logical implication.) This is an entertaining example because it’s easy and looks very similar to the above types. With modern GHC features, we can formulate this using the new Constraint kind.

Let Dict be the ultimate reified dictionary, using a GADT:

data Dict :: Constraint -> * where
  Dict :: ctx => Dict ctx

Given a term of type Dict x, we can witness the constraint x. Max Bolingbroke wrote some stuff about this trick when he implemented ConstraintKinds.

Now, let the type a |- b read ‘a entails b’, implemented as:

newtype (|-) a b = Sub (a => Dict b)

I’ll get to the explanation in a moment. If we peer through the looking glass we can see the term Sub Dict as a kind of evidence that some statement a |- b holds. So now there are some obvious statements we can make about entailment. For one, there is the simple property of reflexivity: “if a, then a”, or in other words a |- a:

reflexive :: a |- a
reflexive = Sub Dict

Another property is transitivity. Given the implication a |- b, and b |- c, we can derive the statement a |- c.

First, we must introduce a helper. Given a term r which requires context b, we may derive a term r requiring context a, iff a |- b.

In other words, we may substitute the constraint under which a given term occurs:

(\\) :: a => (b => r) -> (a |- b) -> r
r \\ Sub Dict = r

Remember the definition of (|-) which is Sub (a => Dict b). Given a dictionary of b, we automatically derive the constituent a for the constraint. Dict will imply the constraint b, but Dict is a term, and thus we can ‘peel it off’ by abandoning the Dict like the above, leaving only a.

Now we can define the property of transitivity:

transitive :: (b |- c) -> (a |- b) -> (a |- c)
transitive f g = Sub (Dict \\ f \\ g)

We can view the transitive function as taking two pieces of evidence and returning a third. We use the helper (\\) to ‘build’ the final evidence piecewise: first we get Dict \\ f which replaces c for b, and then we replace b for the constraint a. This then ‘trivially’ witnesses the fact we can replace c for a.

But these definitions are the exact instances of Category for (|-), and they directly mirror the instances for (->) too:

id        :: a -> a
reflexive :: a |- a

(.)        :: (b -> c) -> (a -> b) -> (a -> c)
transitive :: (b |- c) -> (a |- b) -> (a |- c)

And therefore:

instance Category (|-) where
  id  = reflexive
  (.) = transitive

Note that the kind of entailment is: (|-) :: Constraint -> Constraint -> *

With a kind-polymorphic Category, the type (|-) can now be a valid instance where it couldn’t be before.

By the way, the above definitions are all available as part of Edward’s constraints package.

Conclusion

This change was proposed a while ago, and could have been implemented as early as GHC 7.4 technically. But it’s a nice addition to top off what will already be an awesome 7.8 release.

Full code can be found here.