• Me
• Publications
• Teaching
• Software
• Blog

Categories over pairs of types

Today Dan Burton remarked that Pipe is a category-like thing, and to express it we would need "type bundling". I myself said something similar a while ago. More formally, rather than a category where the objects are Haskell types, we have a category where the objects are pairs of types.

It turns out that with a bunch of recent Ghc extensions we can actually write this in Haskell.

{-# LANGUAGE PolyKinds, DataKinds, KindSignatures #-}
{-# LANGUAGE MultiParamTypeClasses, TypeFamilies #-}

For the purposes of this blogpost I'll use a dummy type for Pipe, there are plenty of other blog posts that give an actually functional one. The important thing to note is that in the type of (>+>), there are two types that are composed over, input/output io and upstream/downstream result ur.

-- Ceci n'est pas une pipe
data Pipe i o u m r = Pipe { runPipe :: Either i u -> m (Either o r) }

(>+>) :: Monad m
      => Pipe io1 io2 ur1 m ur2
      -> Pipe io2 io3 ur2 m ur3
      -> Pipe io1 io3 ur1 m ur3
(>+>) (Pipe f) (Pipe g) = Pipe (f >=> g)

idP :: Monad m => Pipe i i r m r
idP = Pipe return

With the PolyKinds extension we can make a variant of Category that works for tuples of types as well as for normal types. This class looks exactly the same as the normal one:

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

But because of PolyKinds it magically becomes more general. You can see this by comparing their kinds

λ> :kind Category
Category :: (AnyK -> AnyK -> *) -> Constraint
λ> :kind Control.Category.Category
Control.Category.Category :: (* -> * -> *) -> Constraint

With DataKinds it becomes possible to have tuples of types, which are written as '(Type1,Type2). Unfortunately we can not (yet?) pattern match on these directly in data declarations. So we need type families to unwrap them:

type family Fst (xy :: (*,*)) :: *
type family Snd (xy :: (*,*)) :: *
type instance Fst '(x,y) = x
type instance Snd '(x,y) = y

Note that the kind signatures are necessary. Without them Ghc will give errors like

Couldn't match kind `BOX' against `*'

With these type functions in hand we can write

newtype WrapPipe m iu or = WrapPipe
     { unWrapPipe :: Pipe (Fst iu) (Fst or) (Snd iu) m (Snd or) }

instance Monad m => Category (WrapPipe m) where
    id = WrapPipe idP
    x . y = WrapPipe (unWrapPipe y >+> unWrapPipe x)

And that's it. We now have a category whose objects are not Haskell types, but rather pairs of Haskell types. In Ghc's terms, an instance of Category (*,*) instead of Category *. The kind parameter is why we need MultiParamTypeClasses.

With this same trick we can also define Category instances for product categories and lens families. Or going the other way, you can wrap Monoids as a Category over objects of kind (). You could even go one step further and have a category for lists of functions of different types.

There is a big downside, however. And that is that the type inference engine is not able to see past the type families. You need to give an explicit type annotation on the wrapped pipe. Compare

λ> type MyWPipe = WrapPipe IO '(Int,String) '(Int,String)
λ> runPipe (unWrapPipe (id . id :: MyWPipe)) $ Right "done"
Right "done"

with

λ> type MyPipe = Pipe Int Int String IO String
λ> runPipe (unWrapPipe (id . id) :: MyPipe) $ Right "done"
<interactive>:2:10:
   Couldn't match type `Fst or0' with `Int'
   blah, blah, blah, etc.

This makes sense, since Ghc doesn't know that there are no other instances of Fst and Snd. Ideally we would like to write

newtype WrapPipe m '(i,u) '(o,r) = WrapPipe { unWrapPipe :: Pipe i o u m r }

Comments

Jake McArthurDate: 2012-07-28T15:02Zx

You could write WrapPipe with a GADT to express that "pattern matching" on data declarations:

data WrapPipe :: (* -> *) -> (*,*) -> (*,*) -> * where WrapPipe :: Pipe i o u m r -> WrapPipe m '(i,u) '(o,r)

However, I can't seem to be able to define the Category instance from this. GHC gets hung up on the definition for id. Not sure why, yet. Sorry, but I threw away my GHCi session before deciding to leave a comment, so I can't reproduce the error without some work, now.

Sjoerd VisscherDate: 2012-07-28T17:16Zx

For categories that do not have the same objects as Hask, what seems to work best is to replace id with methods that return the source and target identity arrows for a given arrow. That's what I do in my data-cagetory package. Here's the product category.

Jake McArthurDate: 2012-07-28T17:50Zx

I decided to recreate my code. Here it is in its entirety:

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeFamilies #-}
module CategoryPair where

import Prelude hiding (id, (.))
import Control.Monad

data Pipe i o u m r = Pipe { runPipe :: Either i u -> m (Either o r) }

(>+>) :: Monad m
      => Pipe io1 io2 ur1 m ur2
      -> Pipe io2 io3 ur2 m ur3
      -> Pipe io1 io3 ur1 m ur3
(>+>) (Pipe f) (Pipe g) = Pipe (f >=> g)

idP :: Monad m => Pipe i i r m r
idP = Pipe return

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

data WrapPipe :: (* -> *) -> (*,*) -> (*,*) -> * where
  WrapPipe :: Pipe i o u m r -> WrapPipe m '(i,u) '(o,r)

instance Monad m => Category (WrapPipe m) where
  id = WrapPipe idP
  WrapPipe x . WrapPipe y = WrapPipe (y >+> x)

And here is the unfortunate error I get:

    Could not deduce (a ~ (,) * * o0 r0)
    from the context (Monad m)
      bound by the instance declaration
      at /home/jake/src/experiments/CategoryPair.hs:30:10-41
      `a' is a rigid type variable bound by
          the type signature for id :: WrapPipe m a a
          at /home/jake/src/experiments/CategoryPair.hs:31:3
    Expected type: WrapPipe m a a
      Actual type: WrapPipe m ((,) * * o0 r0) ((,) * * o0 r0)
    In the return type of a call of `WrapPipe'
    In the expression: WrapPipe idP

Reply