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
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.
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.
I decided to recreate my code. Here it is in its entirety:
And here is the unfortunate error I get:
Reply