Abstract Nonsense

Abstract Nonsense

Ramblings by Benjamin Kovach

Theme adapted from minimal by orderedlist.

Cofree Meets Free

Published by Ben Kovach on August 14, 2014

Tags: haskell, cofree, comonads

Notes on Cofree Meets Free

Goal: to point out a close relationship between cofree comonads and free monads.

Slides on BayHac ’14 Free Monads talk

Coalgebraic “things” ≈ machines. They have internal state and you can press buttons to change it.

class TwoButton a where
    press :: a -> (a, a)

Above, the state is given by some type a and you can press either the left or right button. press changes the whole state, then we can extract using pressLeft or pressRight:

pressLeft, pressRight :: TwoButton a => a -> a
pressLeft  = fst . press
pressRight = snd . press 
  • Monads ≈ generalized algebraic structures
  • Comonads ≈ generalized machines

Idea: We have a “functorful” of buttons, and we can only observe the machine.

class Comonad w where
    extract :: w a -> a
    duplicate :: w a -> w (w a)

extract lets us observe the state. duplicate gives the container of new states we could end up in when pressing a given button.

A bunch of zippers give rise to comonads, with the focus element being able to be extracted. There is one button at each position the focus might be; pressing the corresponding button moves the focus to that point. The Store comonad has one button for each value you can store in the field it represents.

Cofree coalgebras can be thought of as memoised forms of elements of coalgebras. Memoising in TwoButton means that we figure out everything that might happen if we presse the buttons so we no longer need press.

data CofreeTwoButton = Memo CofreeTwoButton CofreeTwoButton

Each CofreeTwoButton gives a result of pressing one of the two buttons. Any CofreeTwoButton element can be memoised:

memoiseTwoButton :: TwoButton m => m -> CofreeTwoButton
memoiseTwoButton m = Memo 
    (memoiseTwoButton (pressLeft m)) 
    (memoiseTwoButton (pressRight m))

However, we have no way of seeing what’s stored! So we continue…

data CofreeTwoButton a = Memo a (CofreeTwoButton a) (CofreeTwoButton a)

memoiseTwoButton :: TwoButton m => (m -> a) -> m -> CofreeTwoButton a
memoiseTwoButton f m = Memo 
    (f m) 
    (memoiseTwoButton f (pressLeft m))
    (memoiseTwoButton f (pressRight m))

The first argument to memoiseTwoButton says what we want to store in the table and then memoiseTwoButton goes ahead and stores it. We can use the identity function if we want to store the original elements.

NB. This “evolves” a value based on some function, stores it, then recursively does this by “pressing left” and “pressing right” on the new value, making a sort of “memoised binary tree”.

This is like foldMap :: Monoid m => (a -> m) -> t a -> m, if we replace t by [] and remember that [a] is a free monoid. foldMap takes an element of a free monoid and interprets it as an element of another monoid. memoiseTwoButton packs an element of TwoButton into a cofree structure. “interpretation” and “packing” are both homomorphisms. Any element of a free monoid can be “interpreted” by any other monoid (that’s how it was designed – to only satisfy the monoid laws and eqns that can be derived from them).

Every single element of every TwoButton can be packed into CofreeTwoButton, so every equation in the original structure will hold after packing (opposite direction, dualised version).

A cofree comonad is basically a memoised comonad.

data Cofree f a = Cofree a (f (Cofree f a))

At each point in the “table” we store some observable value of type a. We also have a “functorful” of buttons, so we have a “functorful” of new states we can transition to. To fmap over it, apply f to the observable value and fmap over the child nodes.

instance Functor f => Functor (Cofree f) where
    fmap f (Cofree a fs) = Cofree (f a) (fmap (fmap f) fs)

duplicate takes a memoised state and replaces the observed state with the memoised state that stores the observable.

instance Functor f => Comonad (Cofree f) where
    extract (Cofree a _) = a
    duplicate c@(Cofree _ fs) = Cofree c (fmap duplicate fs)

Now we can memoise comonads:

memoiseComonad :: (Comonad w, Functor f) =>
    (forall x. w x -> f x) -> (forall x. w x -> Cofree f x)
memoiseComonad f w = Cofree 
    (extract w) 
    (fmap (memoiseComonad f) (f (duplicate w)))

So a cofree comonad is a type that can be used to memoise all of the states that are accessible from a state in a comonad by pressing its buttons.

The “Free” part

There is a close relationship between free and cofree. The usual Free monad:

data Free f a = Id a | Free (f (Free f a))

join' :: Functor f => Free f (Free f a) -> Free f a
join' (Id x) = x
join' (Free fa) = Free (fmap join' fa)

instance Functor f => Functor (Free f) where
  fmap f (Id x) = Id (f x)
  fmap f (Free fa) = Free (fmap (fmap f) fa)

instance Functor f => Monad (Free f) where
  return = Id
  m >>= f = join' (fmap f m)

Pairings give a way to combine pairs of functors of elements:

class (Functor f, Functor g) => Pairing f g where
    pair :: (a -> b -> r) -> f a -> g b -> r

For instance:

instance Pairing Identity Identity where
    pair f (Identity a) (Identity b) = f a b

data (f :+: g) x = LeftF (f x) | RightF (g x) deriving Functor
data (f :*: g) x = f x :*: g x deriving Functor

instance (Pairing f f', Pairing g g') => 
    Pairing (f :+: g) (f' :*: g') where
    pair p (LeftF x) (a :*: _) = pair p x a
    pair p (RightF x) (_ :*: b) = pair p x b

instance (Pairing f f', Pairing g g') =>
    Pairing (f :*: g) (f' :+: g') where
    pair p (a :*: _) (LeftF x) = pair p a x
    pair p (_ :*: b) (RightF x) = pair p b x

instance Pairing ((->) a) ((,) a) where
    -- (a -> b -> r) -> (c -> a) -> (a, b) -> r 
    pair p f = uncurry (p . f)

given a pairing between f and g we get one between Cofree f and Free g:

instance Pairing f g => Pairing (Cofree f) (Free g) where
    pair p (Cofree a _) (Id x) = p a x
    pair p (Cofree _ fs) (Free gs) = pair (pair p) fs gs

Remember that elements of Free g can be thought of as DSL expressions. This pairing gives a way to apply a monadic expression to a memoised comonad. I.e. monads give a language that can be used to compute something on the output of a comonad (a machine).

data UpDown a = Up a | Down a deriving Functor
type CofreeComagma a = Cofree UpDown a

collatz :: Integer -> UpDown Integer
collatz n | even n -> Down (n `div` 2)
collatz n = Up (3*n + 1)

We can memoise this as a cofree comonad:

memoisedCollatz :: Integer -> CofreeComagma Integer
memoisedCollatz n = Cofree n (fmap memoisedCollatz (collatz n))

Here’s the dual functor:

data Two a = Two a a deriving Functor

…and a pairing (remember above, where if we have pairings for f, g, and Cofree f and Free g have a pairing):

instance Pairing UpDown Two where
    pair f (Up a) (Two b _)   = f a b
    pair f (Down a) (Two _ c) = f a c

execute :: Cofree UpDown x -> Free Two (x -> r) -> r
execute w m = pair (flip ($)) w m

NB. look at the types and remember what a pairing is; it’s just a way to merge together elements of two separate functors and produce a single value. Here, we fold all of those xs from the cofree comonad, feeding them into each of the x -> rs. We finally produce a value of type r.

Here’s a free monad this gives rise to:

data Direction = WentUp | WentDown deriving Show

choose :: Free Two Direction
choose = Free (Two (return WentUp) (return WentDown))

Some code written in the corresponding DSL:

ex1 :: Free Two (Integer -> String)
ex1 = do
    x <- choose
    y <- choose
    case (x, y) of
        (WentDown, WentDown) -> return (\x -> "Decreased twice " ++ show x)
        _ -> return show

Here’s what happen when they meet:

go1 :: String
go1 = execute (memoisedCollatz 12) ex1

NB. It’s funny because I think of Free monads as specifying a specific way to do something (in a DSL, for instance), and comonads as sort of “infinite containers” that hold every value of something at once. Here, it’s kind of flipped on it’s head: Cofree actually defines a specific path through a DSL, while Free holds every possible outcome. In the last diagram, coming into this I might have actually expected Cofree to be the red tree, and Free to be the Collatz chain.

comments powered by Disqus