Friday, November 15, 2013

Applicative Functors

Well, perhaps it's time to resurrect this blog from benign neglect. I must admit that I've been spending close to zero time thinking about comonads and coalgebras lately. This is partly a consequence of having a Real Job, and partly a consequence of the fact that the remainder of my time apart from this is devoted to homotopy type theory and whiskey.

Herein, I simply wish to share a picture of what applicative functors are in category theoretic language.

To this end, let $F: \mathcal{C} \rightarrow \mathcal{D}$ be a functor between cartesian closed categories. We shall call $F$ applicative if there exists a natural transformation of bifunctors $\alpha: F(-^{-}) \rightarrow F(-)^{F(-)}$ (the blanks are different here - is that confusing?). In other words, an applicative functor doesn't necessarily "preserve" exponentials, but there is a map.

In Haskell, $\alpha$ is typically denoted <*>

Also, recall that functor application is actually a function fmap :: Functor f => (a -> b) -> f a -> f b

(I don't want to terminate these sentences with periods because I don't want to gum up the syntax in some way. How do people usually deal with this?)

Now, as fmap can be rather cumbersome to write, I've seen <$> used instead. Well, that makes plenty of sense actually: the operator $ is a special case of this with respect to the identity functor.

Now, a common use of this is to deal with functions that take multiple arguments "inside" of functors. Remember that everything in Haskell is curried by default, so, for instance, addition has the following type:


(+) :: Num a => a -> a -> a

Therefore,

(<$>) (+) :: (Functor f, Num a) => f a -> f (a -> a)

So if we compose that with <*>, we get:

(<*>) . ((<$>) (+)) :: (Num a, Control.Applicative.Applicative f) => f a -> f a -> f a

So, we can now perform addition "inside" any applicative functor, so if you evaluate

(((<*>) . ((<$>) (+))) (Just 1)) (Just 2)

you get

Just 3

Of course, what I wrote above is really ugly, so in practice we would actually use the infix form:

(+) <$> Just 1 <*> Just 2

Now, if you were going to do something like this often, you might as well define a new operator:

let (<+>) x y = (+) <$> x <*> y

So that

Just 1 <+> Just 2

evaluates to

Just 3

Of course, the example functor I am using is rather special, as it creates an "extra value" for any given type. You might wonder what happens when I add nothing to just a number:

Just 1 <+> Nothing

Well, it evaluates to:

Nothing

Well, after all, Maybe is a functor from types to pointed types, so I think it makes perfect sense that our natural transformation preserves the new "basepoint" which we call Nothing.

Wednesday, February 20, 2013

Splay tree access is coalgebraic

Splay trees are balanced binary trees that keep the most recently accessed or inserted item at the top.  More information can be found at http://en.wikipedia.org/wiki/Splay_tree

We wish to define splay trees in Haskell and then make an observation about a certain coalgebraic behavior.

We begin with an import that will become relevant later and the type definition:

> import Control.Comonad
>
> data SplayTree a = Null | Node (SplayTree a) a (SplayTree a)
>   deriving (Eq)

We also want a way of seeing it.  We could have just derived Show, but I like this better:

> instance (Show a) => Show (SplayTree a) where
>   show (Node Null stuff Null) = "[" ++ (show stuff) ++ "]"
>   show (Node left stuff Null) = "(" ++ (show left) ++ "<--[" ++ (show stuff) ++ "])"
>   show (Node Null stuff right) = "([" ++ (show stuff) ++ "]-->" ++ (show right) ++ ")"
>   show (Node left stuff right) =
>       "(" ++ (show left) ++ "<--[" ++ (show stuff) ++ "]-->" ++ (show right) ++ ")"
>   show Null = ""


The functionality of a splay tree derives from classic binary tree operations, together with a "splay" function.  The splay function takes care of the rebalancing.  We begin by defining a textbook binary search tree insert function.

> binsert :: Ord a => a -> SplayTree a -> SplayTree a
> binsert x (Node left stuff right)
>          | x <= stuff = Node (insert x left) stuff right
>          | x > stuff  = Node left stuff (insert x right)
> binsert x Null = Node Null x Null

The actual splay tree insert will follow once we've defined splay:

> insert x t = splay x (binsert x t)

The splay function is a series of rotations that depends upon where the recently used item, below denoted as x, lies in relation to the root.  In fact, we are interested in various configurations where x is the child or grandchild of the current node.  If it is not, we just recursively go down a level.  This function assumes that x is a member of the tree already.  The possibilities are in correspondence with the nice pictures in the above wikipedia page.

We might be already balanced:

> splay x (Node left y right) | x == y = (Node left x right)

What if x is the child of the current node ("zig" or "zag")?  A simple rotation will do:

> splay x (Node (Node l1 y l2) p right)
>             | x == y = Node l1 x (Node l2 p right)
> splay x (Node left p (Node r1 y r2))
>             | x == y = Node (Node left p r1) x r2

Or, x is the left child of the left child (zig-zig) or the right child of the right child (zag-zag):

> splay x (Node (Node (Node ll1 y ll2) p lr) g right)
>           | x == y = Node ll1 x (Node ll2 p (Node lr g right))
> splay x (Node left g (Node rl p (Node rr1 y rr2)))
>           | x == y = Node (Node (Node left g rl) p rr1) x rr2

The other possibilities are a "zigzag" or "zagzig":

> splay x (Node (Node ll p (Node lr1 y lr2)) g right)
>           | x == y = Node (Node ll p lr1) x (Node lr2 g right)
> splay x (Node left g (Node (Node rl1 y rl2) p rr))
>           | x == y = Node (Node left g rl1) x (Node rl2 p rr)

These cases cover when we do not see x as a child or grandchild:

> splay x Null = Null
> splay x (Node left stuff right)
>       | x <= stuff = splay x (Node (splay x left) stuff right)
>       | x > stuff = splay x (Node left stuff (splay x right))

And there you have it!  Let's give it a try:

*Main> insert 3 (insert 4 (insert 2 (insert 0 Null)))
(([0]<--[2])<--[3]-->[4])

Notice that 3 is on the top since it was last accessed.  Neat!

Membership testing is somewhat interesting.  We wish to determine if x is in the tree and splay the tree if this is the case.  As such, membership will have an interesting type.

We start off with plain binary tree membership:

> bmember :: Ord a => a -> SplayTree a -> Bool
> bmember x Null = False
> bmember x (Node left y right) | x == y = True
>                               | x < y  = bmember x left
>                               | x > y  = bmember x right

And now we do the required splaying if we find x:

> member :: Ord a => a -> SplayTree a -> (Bool, SplayTree a)
> member x t | (x `bmember` t)     = (True, splay x t)
>            | not (x `bmember` t) = (False, t)

Note the type signature of member.  The part SplayTree a -> (Bool, SplayTree a) looks coalgebraic.  Let's see if we can more formally clarify that.

Consider the functor $Bool \times -$.  Mathematically, we can identify this with $\mathbb{Z}/{2} \times -$, which has two different monad structures corresponding to the addition and multiplication in $\mathbb{Z}/{2}$.  In terms of boolean algebra, these are or and and, respectively.

However, there is also a comonadic structure on $Bool \times -$.  Let's see if we can define it:

> newtype BoolFunct a = BoolFunct (Bool, a)
>
> instance Functor BoolFunct where
>   fmap f (BoolFunct (b, x)) = BoolFunct (b, f x)

Due to reasons that I do not fully understand, Haskell does not let me declare that (Bool,a) is a functor for any type a.  This is why I need the silly type constructor 'BoolFunct'.

The comonadic structure is induced by the diagonal:

> instance Comonad BoolFunct where
>  extract (BoolFunct (b, x)) = x
>  duplicate (BoolFunct (b, x)) = BoolFunct (b, BoolFunct (b, x))

Of course, one should also check the comonadic laws, namely that duplicate is coassociative and that extract is a counit.  This is left as an exercise for the reader.

By the way, I'm a bit bothered that these things are called 'laws' in the community.  Physics has 'laws'.  Mathematics has axioms.  We are really just verifying that an object satisfies the axioms.  But I digress...

Let's make an observation:

*Main> :type member 3
member 3 :: (Num a, Ord a) => SplayTree a -> (Bool, SplayTree a)

That's interesting.  Detecting whether or not the number 3 is a member seems to give a coalgebra SplayTree Integer -> BoolFunct SplayTree Integer.  Of course, one should be dutiful and verify that this is indeed a coalgebraic structure.  In fact, this is trivial as soon as you write down the commutative diagram.  Here is an example demonstrating coassociativity:

*Main> let t = insert 4 (insert 5 (insert 2 (insert 3 Null)))
*Main> ((fmap (member 3)) . (member 3)) t
(True,(True,([2]<--[3]-->([4]-->[5]))))
*Main> (duplicate . (member 3)) t
(True,(True,([2]<--[3]-->([4]-->[5]))))

There you have it!  Accessing a splay tree is a coalgraic operation.  I'm not sure if this is a useful observation or not, but part of the mission of this blog is to collect interesting comonads and coalgebras in the Haskell world to understand them better.


Addendum: What I've posted above is correct in spirit but not in letter.  If I really want to make member a coalgebra over the comonad BoolFunct, then I need to use the type constructor:

> cmember :: Ord a => a -> SplayTree a -> BoolFunct (SplayTree a)
> cmember x t = BoolFunct (member x t)

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.