Thu 23 Jun 2011

## Free Monads for Less (Part 1 of 3): Codensity

Posted by Edward Kmett under Algorithms , Category Theory , Data Structures , Haskell , Kan Extensions , Monads[8] Comments

A couple of years back Janis VoigtlĂ¤nder wrote a nice paper on how one can use the codensity monad to improve the asymptotic complexity of algorithms using the free monads. He didn't use the name Codensity in the paper, but this is essentially the meaning of his type `C`

.

I just returned from running a workshop on domain-specific languages at McMaster University with the more than able assistance of Wren Ng Thornton. Among the many topics covered, I spent a lot of time talking about how to use free monads to build up term languages for various DSLs with simple evaluators, and then made them efficient by using `Codensity`

.

This has been shown to be a sufficient tool for this task, but is it necessary?

First, some context:

**Monads for Free**

Given that *f* is a `Functor`

, we get that

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

is a `Monad`

for free:

instance Functor f => Functor (Free f) where fmap f (Pure a) = Pure (f a) fmap f (Free as) = Free (fmap (fmap f) as) instance Functor f => Monad (Free f) where return = Pure Pure a >>= f = f a -- the first monad law! Free as >>= f = Free (fmap (>>= f) as)

The definition is also free in a particular categorical sense, that if *f* is a monad, then, and you have a forgetful functor that forgets that it is a monad and just yields the functor, then the the free construction above is left adjoint to it.

This type and much of the code below is actually provided by Control.Monad.Trans.Free in the comonad-transformers package on hackage.

For a while, Free lived in a separate, now defunct, package named `free`

with its dual Cofree, but it was merged into comonad-transformers due to complications involving comonads-fd, the comonadic equivalent of the mtl. Arguably, a better home would be transformers, to keep symmetry.

**Free is a Monad Transformer**

instance MonadTrans Free where lift = Free . liftM Pure

and there exists a retraction for lift

retract :: Monad f => Free f a -> f a retract (Pure a) = return a retract (Free as) = as >>= retract

such that `retract . lift = id`

. I've spoken about this on Stack Overflow, including the rather trivial proof, previously.

This lets us work in `Free m a`

, then flatten back down to a single layer of *m*.

This digression will be useful in a subsequent post.

**MonadFree**

What Janis encapsulated in his paper is the notion that we can abstract out the extra power granted by a free monad to add layers of *f* to some monad *m*, and then use a better representation to improve the asymptotic performance of the monad.

The names below have been changed slightly from his presentation.

class (Monad m, Functor f) => MonadFree f m | m -> f where wrap :: f (m a) -> m a instance Functor f => MonadFree f (Free f) where wrap = Free

instances can easily be supplied to lift `MonadFree`

over the common monad transformers. For instance:

instance (Functor f, MonadFree f m) => MonadFree f (ReaderT e m) where wrap fs = ReaderT $ \e -> wrap $ fmap (`runReaderT` e) fs

This functionality is provided by Control.Monad.Free.Class.

Janis then proceeded to define the aforementioned type `C`

, which is effectively identical to

newtype Codensity f a = Codensity (forall r. (a -> f r) -> f r)

This type is supplied by Control.Monad.Codensity from my kan-extensions package on hackage.

I have spoken about this type (and another that will arise in a subsequent post) on this blog previously, in a series of posts on Kan Extensions. [ 1, 2, 3]

`Codensity f`

is a `Monad`

, **regardless** of what *f* is!

In fact, you can quite literally cut and paste much of the definitions for `return`

, `fmap`

, and `(>>=)`

from the code for the `ContT`

monad transformer! Compare

instance Functor (Codensity k) where fmap f (Codensity m) = Codensity (\k -> m (k . f)) instance Monad (Codensity f) where return x = Codensity (\k -> k x) m >>= k = Codensity (\c -> runCodensity m (\a -> runCodensity (k a) c)) instance MonadTrans Codensity where lift m = Codensity (m >>=)

from Control.Monad.Codensity in kan-extensions with

instance Functor (ContT r m) where fmap f m = ContT $ \c -> runContT m (c . f) instance Monad (ContT r m) where return a = ContT ($ a) m >>= k = ContT $ \c -> runContT m (\a -> runContT (k a) c) instance MonadTrans (ContT r) where lift m = ContT (m >>=)

from the Control.Monad.Trans.Cont in transformers.

`Codensity m a`

is effectively `forall r. ContT r m a`

. This turns out to be just enough of a restriction to rule out the use of callCC, while leaving the very powerful fact that when you lower them back down using

lowerCodensity :: Monad m => Codensity m a -> m a lowerCodensity (Codensity m) = m return

or

runContT :: ContT r m a -> m r runContT (ContT m) = m return

`ContT`

and `Codensity`

both yield a result in which all of the uses of the underlying monad's `(>>=)`

are right associated.

This can be convenient for two reasons:

First, some almost-monads are not associative, and converting to ContT or Codensity can be used to fix this fact.

Second, in many monads, when you build a big structure using left associated binds, like:

(f >>= g) >>= h

rather than use right associated binds like

f >>= \x -> g x >>= h

then you wind up building a structure, then tearing it down and building up a whole new structure. This can compromise the productivity of the result, and it can also affect the asymptotic performance of your code.

Even though the monad laws say these two yield the same answer.

**The dual of substitution is redecoration**

To see that, first, it is worth noting that about ten years back, Tarmo Uustalu and Varmo Vene wrote "The dual of substitition is redecoration", which among other things quite eloquently described how monads are effectively about substituting new tree-like structures, and then renormalizing.

This can be seen in terms of the more categorical viewpoint, where we define a monad in terms of `return`

, `fmap`

and `join`

, rather than `return`

and `(>>=)`

. In that presentation:

m >>= f = join (fmap f m)

`fmap`

is performing substitution. and `join`

is dealing with any renormalization.

Done this way, `(m >>= f)`

on the `Maybe`

monad would first `fmap`

to obtain `Just (Just a)`

, `Just Nothing`

or `Nothing`

before flattening.

In the Maybe a case, the association of your binds is largely immaterial, the normalization pass fixes things up to basically the same size, but in the special case of a free monad the monad is **purely defined in terms of substitution**, since:

-- join :: Functor f => Free f (Free f a) -> Free f a -- join (Pure a) = a -- join (Free as) = Free (fmap join as)

This means that every time you `>>=`

a free monad you are accumulating structure -- structure that you have traverse past to deal with subsequent left-associated invocations of `>>=`

! Free monads never shrink after a bind and the main body of the tree never changes.

More concretely, you could build a binary tree with

```
-- data Tree a = Tip a | Bin (Tree a) (Tree a)
```

and make a monad out of it, writing out your `return`

and `(>>=)`

, etc. by hand

The same monad could be had 'for free' by taking the free monad of

data Bin a = Bin a a deriving (Functor, Foldable, Traversable) -- using LANGUAGE DeriveFunctor, DeriveFoldable, DeriveTraversable

yielding the admittedly slightly less convenient type signature

```
type Tree = Free Bin
```

Now you can use `return`

for `Tip`

, and

bin :: MonadFree Bin m => m a -> m a -> m a bin l r = wrap (Bin l r)

to construct a binary tree node, using any free monad representation.

Now, if that representation is `Free Bin`

(or the original more direct `Tree`

type above) then code that looks like `f >>= \x -> g x >>= h`

performs fine, but `(f >>= g) >>= h`

will retraverse the unchanging 'trunk' of the tree structure twice. That isn't so bad, but given n uses of >>= we'll traverse an ever-growing trunk over and over *n* times!

**Putting Codensity to Work**

But, we have a tool that can fix this, `Codensity`

!

instance MonadFree f m => MonadFree f (Codensity m) where wrap t = Codensity (\h -> wrap (fmap (\p -> runCodensity p h) t))

Janis packaged up the use of `Codensity`

into a nice combinator that you can sprinkle through your code, so that your users never need know it exists. Moreover, it prevents them from accidentally using any of the extra power of the intermediate representation. If your code typechecks before you use improve somewhere within it, and it type checks after, then it will yield the same answer.

improve :: Functor f => (forall m. MonadFree f m => m a) -> Free f a improve m = lowerCodensity m

By now, it should be clear that the power of `Codensity`

is sufficient to the task, but is it necessary?

More Soon.

[Edit; Fixed minor typographical errors pointed out by ShinNoNoir, ivanm, and Josef Svenningsson, including a whole bunch of them found by Noah Easterly]

June 23rd, 2011 at 11:49 pm

[...] Last time, I started exploring whether or not Codensity was necessary to improve the asymptotic performance of free monads. [...]

July 5th, 2012 at 6:52 am

Hi,

Thank you for this very informative post.

You’ve just forgotten to declare f to be a functor when defining MonadFree f (Codensity m) instance.

Regards

July 5th, 2012 at 11:41 am

Fixed. I updated it by constraining MonadFree instead. It works correctly in the library I referenced. =)

October 26th, 2012 at 6:59 pm

I’m really fascinated by the idea of correct-by-construction monads. One question, though. Control.Monad.Free seems very similar to the Control.Monad.Prompt module. What is the relationship between the two?

November 18th, 2012 at 12:21 pm

@Tac-Tics: They are more or less identical.

November 8th, 2013 at 1:45 pm

[...] seen the term Free Monad pop up every now and then for some time, but everyone just seems to use/discuss them without giving an explanation of what [...]

June 21st, 2014 at 10:06 am

Hi,

I was looking for the Free type on the package indicated in the post, but it seems that in the latest version there’s no Control.Monad.Trans.Free subpackage.

Was it moved somewhere else?

Thanks.

August 3rd, 2014 at 10:41 pm

gucci bags…Needless to say, the Short & High Ugg boot Video game titles will be well-liked, beautiful varieties….