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.

Should that be "data Dict :: ..." rather than "dict Dict :: ..."?

ReplyDeleteFixed. Thank you Ivan!

ReplyDelete