The Interchange Law
I find it amazing the way you can take a bunch of abstract nonsense and turn it into concrete Haskell code for doing something mundane. Having down-to-earth examples really does help with getting your head around the abstractions.
Anyway, on page 43 of Categories for the Working Mathematician (2nd Ed.) is the 'interchange law' for horizontal and vertical composition of natural transformations. Not only can we find a nice mundane example to help thinking about it, we can even test it using Quickcheck.
For convenience we can define a natural transformation type:
Where f and g are intended to be instances of Functor.
If we have a natural transformation from f to g, and another from g to h, then we can compose them using the ordinary Haskell composition operator (.). In Haskell, functors are frequently containers, so we can use containers as a guiding example. If we know how to map a bag of stuff to a sack of stuff, and we know how to map a sack of stuff to a box of stuff, then we just perform the two operations in sequence and we can map a bag of stuff to a box of stuff. This is known as vertical composition.
But there is also another way to compose natural transformations known as horizontal composition. Again we can think about containers. Suppose we know how to map a bag of stuff to a sack of stuff, and we know how to map a box of stuff to a crate of stuff, then we also know how to map a bag of boxes of stuff to a sack of crates of stuff. There are two obvious ways to do this: we could convert the bag of boxes of stuff to a sack of boxes, and then convert each box to a crate. Or we could convert the boxes to crates first, and then map the resulting bag of crates to a sack of crates. We can define two binary operators `o` and `o'` to perform each of these tasks:
Intuitively we'd expect these things to be equal, and in fact they always are. (Exercise: write a quickcheck for this based on the code below.)
Now we need some functorial containers to play with:
Now we can define a bunch of natural transformations mapping between these containers and some others:
On page 43 is the interchange law. Superficially it looks a lot like abiding. For any α, β, α' and β' with compatible types, we have
This is the identity I want to check for the special case of the types I've chosen above. So we can define the left and right hand sides:
And here we go:
Just type test1 in ghci to hear the sweet sound of 100 tests passing.
Anyway, we're just a hair's breadth away from defining 2-categories now. But I'll leave that for another day.
Thinking about it, I gave slogans for the previous theorems so why don't I give one for the interchange law. Take a deep breath. If you know how to convert a bowl of stuff into a box of stuff, and a box into a bag, and an urn into a crate, and a crate into a sack, then there are two equivalent ways to convert a bowl of urns into a bag of sacks: we can either construct methods going from bowl to bag and from urn to sack and combine them to go from bowl of urns to a bag of sacks, OR, we can go from a bowl of urns to a box of crates to a bag of sacks. I'm sure it's all a lot clearer now. ;-)
Well that's enough abstract nonsense. Time to get away from it all and watch some youtube videos. Eh? Oh well. Just wish me luck for tomorrow when I try to beat my fastest time in Bay to Breakers. Maybe some other bayfpers will be there too.
Anyway, on page 43 of Categories for the Working Mathematician (2nd Ed.) is the 'interchange law' for horizontal and vertical composition of natural transformations. Not only can we find a nice mundane example to help thinking about it, we can even test it using Quickcheck.
For convenience we can define a natural transformation type:
> {-# OPTIONS -fglasgow-exts -fno-warn-missing-methods #-}
> import Test.QuickCheck
> import Control.Monad.Writer
> type Natural f g = forall a.f a -> g a
Where f and g are intended to be instances of Functor.
If we have a natural transformation from f to g, and another from g to h, then we can compose them using the ordinary Haskell composition operator (.). In Haskell, functors are frequently containers, so we can use containers as a guiding example. If we know how to map a bag of stuff to a sack of stuff, and we know how to map a sack of stuff to a box of stuff, then we just perform the two operations in sequence and we can map a bag of stuff to a box of stuff. This is known as vertical composition.
But there is also another way to compose natural transformations known as horizontal composition. Again we can think about containers. Suppose we know how to map a bag of stuff to a sack of stuff, and we know how to map a box of stuff to a crate of stuff, then we also know how to map a bag of boxes of stuff to a sack of crates of stuff. There are two obvious ways to do this: we could convert the bag of boxes of stuff to a sack of boxes, and then convert each box to a crate. Or we could convert the boxes to crates first, and then map the resulting bag of crates to a sack of crates. We can define two binary operators `o` and `o'` to perform each of these tasks:
> o,o' :: (Functor f,Functor f',Functor g,Functor g') => Natural f' g' ->
> Natural f g -> (forall c.f' (f c) -> g' (g c))
> o s t x = s (fmap t x)
> o' s t x = fmap t (s x)
Intuitively we'd expect these things to be equal, and in fact they always are. (Exercise: write a quickcheck for this based on the code below.)
Now we need some functorial containers to play with:
> data Pair x = Pair x x deriving (Eq,Show)
> instance Functor Pair where
> fmap f (Pair a b) = Pair (f a) (f b)
> newtype Id x = Id x deriving (Eq,Show)
> instance Functor Id where
> fmap f (Id x) = Id (f x)
Now we can define a bunch of natural transformations mapping between these containers and some others:
> alpha :: Natural Pair []
> alpha (Pair x y) = [x,y]
> beta :: Natural [] Maybe
> beta [] = Nothing
> beta (x:xs) = Just x
> alpha' :: Natural ((,) a) Id
> alpha' (a,x) = Id x
> beta' :: Natural Id (Either b)
> beta' (Id x) = Right x
On page 43 is the interchange law. Superficially it looks a lot like abiding. For any α, β, α' and β' with compatible types, we have
(β . α) o (β' . α') = (β o β') . (α o α')
This is the identity I want to check for the special case of the types I've chosen above. So we can define the left and right hand sides:
> lhs = (beta . alpha) `o` (beta' . alpha')
> rhs = (beta `o` beta') . (alpha `o` alpha')
> type From = Pair (Float,Integer)
> type To = Maybe (Either String Integer)
And here we go:
> test1 = quickCheck (\x -> lhs (x :: From) == (rhs x :: To))
Just type test1 in ghci to hear the sweet sound of 100 tests passing.
Anyway, we're just a hair's breadth away from defining 2-categories now. But I'll leave that for another day.
Thinking about it, I gave slogans for the previous theorems so why don't I give one for the interchange law. Take a deep breath. If you know how to convert a bowl of stuff into a box of stuff, and a box into a bag, and an urn into a crate, and a crate into a sack, then there are two equivalent ways to convert a bowl of urns into a bag of sacks: we can either construct methods going from bowl to bag and from urn to sack and combine them to go from bowl of urns to a bag of sacks, OR, we can go from a bowl of urns to a box of crates to a bag of sacks. I'm sure it's all a lot clearer now. ;-)
Well that's enough abstract nonsense. Time to get away from it all and watch some youtube videos. Eh? Oh well. Just wish me luck for tomorrow when I try to beat my fastest time in Bay to Breakers. Maybe some other bayfpers will be there too.
> instance Arbitrary a => Arbitrary (Id a) where
> arbitrary = liftM Id arbitrary
> instance Arbitrary a => Arbitrary (Pair a) where
> arbitrary = liftM2 Pair arbitrary arbitrary
posted by sigfpe at Saturday, May 17, 2008
3 Comments:
I guess this is something you get asked a lot...but I'll add my voice to the throng anyway. Are you going to write a book on categories and functional programming? Thanks to your blog it will enjoy the unusual status of being a classic before even having been written.
I'm not convinced I know the subject well enough. And anyway, I never manage to complete papers, let alone an entire book! Not without giving up my day job anyway.
Whether you think you know the subject well enough or not, I'd like to second the idea of a book. There's been a furor of late over on Reddit about the impenetrability of most books on category theory (due mostly to the jargon and lack of examples). And here at Indiana Uni some folks are working on teaching undergrads about monads without using the scary M word. So there's definitely an audience out there for CT in English.
As someone who knows a fair deal of CT, I've always found your posts a delight to read and the concrete examples really help for making the higher concepts make sense in the world of day-to-day programming. And after trying to teach friends CT by examples rather than by definitions for the past couple years, it'd be nice to have a book to direct folks to. Heck, I'd even be willing to help write such a thing if need be.
Post a Comment
<< Home