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.

Phantom types for crypto keys

Phantom types and GADTs are well-known techniques in Haskell for helping build programs that enforce certain kinds of type refinement: they essentially are used to help serve witness to some type equality. This type equality generally enforces constraints on the nature of your code. In the case of GADTs, your witnesses are the data type constructors (which actually carry around an equality constraint,) and with phantom types, you typically build valid terms from an encapsulated data type, using provided APIs.

While working on salt I recently found the types I used for various key types to be a bit inexpressive. I want the library to be type safe in a way that avoids common misusage, and helps the user write correct code: the API should be explanatory and simple.

My old API looked like this:

newtype PublicKey = PublicKey { unPublicKey :: ByteString } deriving ...
newtype SecretKey = SecretKey { unSecretKey :: ByteString } deriving ...

type KeyPair = (PublicKey, SecretKey)

And then you had things like the public-key encryption API, which looked like:

createKeypair :: IO KeyPair
encrypt :: Nonce       -- Nonce
        -> ByteString  -- Plaintext
        -> PublicKey   -- Receiver public key
        -> SecretKey   -- Sender secret key
        -> ByteString  -- Ciphertext

I thought for a little bit and eventually came up with a key API that is shared for all interfaces, very minimal and a bit more explanatory. I took the idea from repa: to tag the type constructor with type variables, and use them for distinguishing the kind of data.

So the new API looks like this:

newtype Key s i = Key { unKey :: ByteString }

data Public
data Secret

type KeyPair i = (Key Public i, Key Secret i)

And now encryption looks like this:

data PublicEncryptionKey
createKeypair :: IO (KeyPair PublicEncryptionKey)
encrypt :: Nonce
        -> ByteString
        -> Key Public PublicEncryptionKey
        -> Key Secret PublicEncryptionKey
        -> ByteString

The API is a bit wordier, but for the most part, keys will be either parametric in the key types or the key type is fixed for an API, so there’s not too much need to be so specific I imagine.

I actually like this new API quite a bit because it’s easy to see at a glance what a key is for, and type-checking makes sure you won’t make simple mistakes. It’s also quite self-explanatory, I think.

I’m working on reducing the wordiness of imports and the APIs further, so hopefully this can be improved on.

Ur/Web at Hac φ

I'll be giving a short talk and presentation on Ur/Web at the next Haskell Hackathon, Hac φ. The talks are scheduled to be between 10-15 minutes, so I'm aiming to have a short spiel for the people who are there in person. But I'm also keeping the slides fairly complete and detailed as possible for those who are interested, but won't be able to make it. I know, slides aren't the best, but I don't think there will be any video recording for the talks, so I'll try to make them as self-contained as I can.

On that note, Pandoc is awesome.

If you're going to be there or want to talk, get in touch with me!

Edit: It's been done, and Hac Phi was a ton of fun! I didn't get the slides as complete as I wanted to (partially due to laziness, gaming and a million other things,) but for the interested, you can find the slides online here.

OPA: now open source

I've been doing a bit of programming with Ur/Web and OPA in the last week, because they're both pretty similar frameworks in some sense, but with a lot of important differences. I'll maybe write something about this soon.

But in the mean time, OPA has now gone open source! No more need for an invite, so go grab it yourself: https://github.com/MLstate/opalang