Archive for the ‘Category Theory’ Category

Everything’s a Function.

January 18, 2013

In Haskell, ignoring certain annoyances like bottom, we have a Cartesian closed category, or CCC, of types and functions. In CCCs, there are function types and Cartesian product types and they are related by the curry and uncurry isomorphisms (named after Haskell Curry).

curry :: ((a , b) -> c) -> (a -> b -> c)
uncurry :: (a -> b -> c) -> ((a , b) -> c)

But CCCs have another important property, they are endowed with a “terminal object”, that is an object t such that there is a unique function f :: a -> t for any a. In Haskell, the terminal object is (), called unit, and it has only one value, also (), and hence only one (polymorphic) function to it, the constant function \ x -> (). If you think about Cartesian products with any number n of factors (a1 , a2 , .. , an), you can think of () as the special case with 0 factors. And just like we can generalize currying to functions with any number n > 2 of arguments, we can think about “zurrying” functions with 0 arguments.

zurry :: (() -> a) -> a
unzurry :: a -> (() -> a)
zurry f = f ()
unzurry x = \ () -> x

What does that give us? Well, nothing, but it lets us recognize that function evaluation is really just a zurried form of function composition.

unzurry (f x) = f . (unzurry x)

So function evaluation isn’t really first class, and since this is Functional Programming, maybe we should think of everything as a function, by unzurrying if necessary!

P.S. When working with a monad, you work in its Kleisli category which is another example of a CCC. The above discussion relating function evaluation to function composition, would then relate Kleisli evaluation (>>=) to Kleisli composition (>=>).

Zipper comonad

January 18, 2013

Here’s something cool I realized while thinking about Haskell lenses (getters and setters) being coalgebras of the costate comonad. Another example of a comonad is the zipper.

data Zipper a = Zipper [a] a [a]

(List) zippers are a way of looking at lists with a focus at a particular element. It should be obvious that we might want to get or set that focus, so that zippers come naturally adorned with lenses.

get :: Zipper a -> a
set :: Zipper a -> a -> Zipper a
lens :: Zipper a -> (a , a -> Zipper a)
get Zipper ls x rs = x
set (Zipper ls x rs) y = Zipper ls y rs
lens z = (get z , set z)

The other natural operations on zippers is list traversal. The zipper had three parts, the part of list to the left, the focus, and the part of the list to the right. (Clowns to the left of me, jokers to the right.) The left part is assumed to be in reverse order, so that its head is next to the focus.

toList :: Zipper a -> [a]
goLeft :: Zipper a -> Zipper a
goRight :: Zipper a -> Zipper a
toList Zipper ls x rs = (reverse ls) ++ (x:rs)
goLeft Zipper ls x rs = Zipper (tail ls) (head ls) (x:rs)
goRight Zipper ls x rs = Zipper (x:ls) (head rs) (tail rs)

So, how are zippers an example of a comonad? Define extract (coreturn) and duplicate (cojoin) like so.

extract :: Zipper a -> a
duplicate :: Zipper a -> Zipper Zipper a
extract = get
duplicate z = Zipper (tail $ iterate goLeft z) z (tail $ iterate goRight z)

What is duplicate of a zipper? Its focus is the zipper itself, but its other parts are all the other possible zippers for the underlying list, with their foci shifted according to their distance from the focus zipper. Maybe a better word for “duplicate” would be “diagonal”, since you can visualize it by putting copies of the list next to each other, then drawing a diagonal line through their foci. Indeed, this is closely related to various morphisms in topology and algebra that all go by the name “diagonal map”.

Nota bene: Zippers only really make sense for infinite lists, because in a finite list you can’t go left or right indefinitely, so for finite lists you have to work around with Maybes or special cases. I’m sure this has something to do with the distinction between data and codata. Finite lists are data and form a monad (the familiar one) while infinite lists (streams) are codata and form a comonad.