Saturday, December 22, 2012

The stream of Fibonacci numbers is an instance of a comonadic type.


The object of this post is to provide a simple example of the use of comonads in Haskell.  Much of this post is a rehash of this awesome paper by Richard B. Kieburtz.

It just so happens that the definition of Comonad is available from hackage.  Simply do 'cabal install comonad'.  I must admit that typing this command feels kind of funny.

Now we can

> import Control.Comonad

Okay, let's define what a stream is:

> data Stream a = forall b. S b (b -> a) (b -> b)
> current (S x f g) = f x
> rest (S x f g) = S (g x) f g

A stream of a's consists of a current position x, a function f to get some value from the current position, and a function g to transition from the current position to the rest of the stream.

Note, to make this definition, -XExistentialQuantification must be passed to ghci or ghc.  Why?  Because of the forall b part of the definition of Stream.  This allows us to use any type b as a "carrier" or "container" for the underlying implementation of a stream.

Here is the stream of integers corresponding to the Fibonacci sequence:

> fibstream = S (1,1) fst (\(j,k) -> (k, j + k))

In this case, our "carrier" is an iterated 2-tuple.  But we don't really need to know that.  I shall now pause to ask ghci for some Fibonacci numbers:

*Main> current fibstream
1
*Main> current (rest fibstream)
1
*Main> current (rest (rest fibstream))
2
*Main> current (rest (rest (rest fibstream)))
3
*Main> current (rest (rest (rest (rest fibstream))))
5
*Main> current (rest (rest (rest (rest (rest fibstream)))))
8

Hooray!

Of course, the astute category theorist should recognize that Stream is a functor on the category of Haskell types.

> instance Functor Stream where
>   fmap f = \s -> S s (f . current) rest

That is, given an f that goes from a's to b's, we can make (fmap f) that goes from a Stream of a's to a Stream of b's.

Note that in category theory, if $F$ is a functor from a category $\mathcal{C}$ to another category $\mathcal{D}$, then we use $F$ to refer to both the object and morphism mappings of $F$.  For instance, we blithely refer to $F(X)$ and $F(f)$ where $X$ is an object and $f$ is a morphism.

For our Stream functor in Haskell, the type constructor Stream refers to the object component of the functor and fmap refers to the morphism component.

How about an example of this functor in action?

> square x = x * x
> fibsquares = (fmap square) fibstream

fibsquares ought to be a stream consisting of the squares of the Fibonacci numbers.  Let's ask ghci:

*Main> current fibsquares
1
*Main> current (rest fibsquares)
1
*Main> current (rest (rest fibsquares))
4
*Main> current (rest (rest (rest fibsquares)))
9
*Main> current (rest (rest (rest (rest fibsquares))))
25
*Main> current (rest (rest (rest (rest (rest  fibsquares)))))
64

We now have a functor called Stream, a member fibstream of the type Stream Integer, and a function (fmap square) from Stream Integer to Stream Integer, which is the image of the function square from Integer to Integer.

What about this comonad business?

Recall that a comonad $G$ on a category $\mathcal{C}$ consists of a functor $G : \mathcal{C} \rightarrow \mathcal{C}$ together with natural transformations $\Delta: G \rightarrow G^2$ and $\epsilon : G \rightarrow 1$ satisying "the appropriate diagrams", namely, that $\Delta$ is coassociative and $\epsilon$ is a counit for $\Delta$.

Well, as you might have predicted, I claim that the functor Stream, as defined above, is a comonad.  The counit is already defined above as current.  I'm going to call $\Delta$ something more descriptive:

> dupstream s = S s id rest

(id is the identity function)

This turns (Stream a) into (Stream (Stream a)).  By construction, this is a natural transformation (always be suspicious when you read something like this).  Shall we verify coassociativity?

> f1 = dupstream (dupstream fibstream)
> f2 = (fmap dupstream) (dupstream fibstream)

In f1, we duplicate the duplicated stream.  In f2, we duplicate the stream "encapsulated" by the duplicated stream.  I hope that makes sense.  Both are of type (Stream (Stream (Stream Integer))).  If Stream is really a comonad, f1 ought to be equal to f2.

Well, ghci?

*Main> current (current (current f1))
1
*Main> current (current (current f2))
1

That's not a proof, but rather encouraging.

> instance Comonad Stream where
>    extract = current
>    duplicate = dupstream

In the Comonad specification, the counit is denoted by "extract" and the comultiplication is denoted by "duplicate".  These names are more descriptive than $\epsilon$ or $\Delta$.

Now that we have a comonad, the natural question that a mathematician would ask is, "What are the coalgebras over this comonad?".  Recall that given a comonad $G$, a coalgebra over $G$ consists of an object $X$ together with a morphism $\psi: X \rightarrow G(X)$ such that $\Delta_{X} \circ \psi = G(\psi) \circ \psi$.  That is, an object $X$ equipped with a comultiplication that is compatible with the comultiplication on $G$.  A morphism of coalgebras is a map $f: X \rightarrow Y$ in $\mathcal{C}$ such that $G(f) \circ \psi_{X} = \psi_{Y} \circ f$ (here, I use a subscript to denote respective coalgebra structures).

Given a comonad $G$, we get an entire category of coalgrbas for free.  This is the Kleisli category $\mathcal{C}^G$, which consists of all cofree coalgebras.

A cofree coalgebra over $G$ is of the form $\Delta_{X} : G(X) \rightarrow G(G(X))$.  It follows that a morphism between cofree coalgebras is a map $f: G(X) \rightarrow G(Y)$ compatible with $\Delta$.  Recall that there is a counit $\epsilon_{Y} : G(Y) \rightarrow Y$.  Hence, given such an $f$, there is $\epsilon_{Y} \circ f : G(X) \rightarrow Y$.

In fact, all maps in to a cofree coalgebra are lifts of maps to the underlying object.  Let's illustrate this with an example.

> smudge s = (current s) + (current (rest s)) + (current (rest (rest s)))

smudge takes a Stream s and adds the first three elements.  As we've defined it, is a map from (Stream a) to a, where a is a type that + works on, namely of the type class Num.

Observe:

*Main> smudge fibstream
4

For the sake of simplicity, let's consider smudge a morphism from (Stream Integer) to Integer.  It ought to life to a morphism from (Stream Integer) to (Stream Integer) that is compatible with the cofree coalgebra structure on (Stream Integer), namely, duplicate.

How do we lift smudge?  Applying fmap to smudge will produce a morphism from (Stream (Stream Integer)) to (Stream Integer).  We can then precompose this with duplicate to obtain a map (Stream Integer) to (Stream Integer).

> streamsmudge = (fmap smudge) . duplicate

*Main> :type streamsmudge fibstream
streamsmudge fibstream :: Stream Integer
*Main> current (streamsmudge fibstream)
4
*Main> current (rest (streamsmudge fibstream))
6


In fact, the above lift can be done with any morphism like smudge.  Control.Comonad defines

> extend f = (fmap f) . duplicate

and in this context, streamsmudge is just (extend smudge).


What we've done is somewhat trivial.  Given a way to smudge the first few elements of a stream, we can create a stream of these smudges.  That's what cofree-ness means in this context.

I personally think that this is neat, because concepts like coalgebras and cofreeness can be tricky to understand.  Algebras and free things usually easier to grasp in mathematics.  The co prefix makes the brain twist around.

Prelude

This is a blog that I will use to learn more about functional programming.  Specifically, I'm going to see how various category theoretic concepts are mapped into the Haskell programming language (and possibly others).

Mathematician friends who are not "in the loop" can follow along by first installing Haskell.  It will help to have some programming experience or possibly read a few of the basic tutorials.  One neat thing about this language is that you can open up the interpreter by typing ghci in your terminal and play around.

Computer science and programmers might profit from this blog as well.  Though my posts will assume some mathematical background, I will pause to make appropriate definitions from time to time.  However, the interested reader should at least know about categories and functors.