Ramblings by Benjamin Kovach
Theme adapted from minimal by orderedlist.
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
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 thenmemoiseTwoButton
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.
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 x
s from the cofree comonad, feeding them into each of the x -> r
s. 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.