# Free monads in category theory

*Free monads*.

*August 2, 2016*

## Forgetting how to multiply

It’s probably easiest to understand what a free monad is if we first understand forgetful functors^{1}.

In category theory, a functor maps between categories, mapping objects to objects and morphisms to morphisms in a way that preserves compositionality^{2}.

A *forgetful functor* is just a functor that discards some of the structure or properties of the input category.

For example, unital rings have objects , where is a set, and are binary operations with identity elements respectively.

Let’s denote the category of all unital rings and their homomorphisms by , and the category of all non-unital rings and their homomorphisms with . We can now define a forgetful functor: , which just drops the multiplicative identity.

Similarly, we can define another forgetful functor , which maps from the category of rngs to the category of abelian groups. discards the multiplicative binary operation, simply mapping all morphisms of multiplication to morphisms of addition.

## Forgetting monoids

The forgetful functor forgets ring multiplication. What happens if instead you forget addition? You get monoids! We can define monoids as the triple , where is a set, is an associative binary operation, and is the neutral element of that operation.

The forgetful functor maps from the category of rings to the category of monoids, , in which the objects are monoids, and the morphisms are monoid homomorphisms.

Monoid homomorphisms map between monoids in a way that preserves their monoidal properties. Given , a monoid defined by , and , a monoid defined by , a function from to is a monoid homomorphism iff:

it preserves compositionality^{3}:

and maps the identity element:

Translating into Haskell, if `phi`

is a monoid homomorphism between monoid `X`

to monoid `Y`

, then:

```
phi (mappend a b) == mappend (phi a) (phi b) -- (1)
phi (mempty :: X) == mempty :: Y -- (2)
```

For example, we can define a monoid homomorphism that maps from the list monoid to the `Sum`

monoid, the monoid formed from the natural numbers under addition:

```
import Data.Monoid
listToSum :: [a] -> Sum Int
listToSum = Sum . length
```

If it’s too difficult (or we can’t be bothered) to derive a formal proof, we can use QuickCheck to test properties of functions. Let’s quickly check if `listToSum`

is actually a monoid homomorphism:

```
import Test.QuickCheck
-- (1)
homomorphism :: [()] -> [()] -> Bool
homomorphism a b =
phi (mappend a b) == mappend (phi a) (phi b)
where phi = listToSum
```

```
ghci> quickCheck homomorphism -- (1)
OK, passed 100 tests.
ghci> listToSum (mempty :: [a]) == mempty :: Sum Int -- (2)
True
```

Let’s forget some more things with yet another forgetful functor, ^{4}.

is a category where the objects are sets, and the arrows are just plain functions. So will map every monoid in to its underlying set, and every monoid homomorphism to a plain function.

`Sum Int`

would just become `Int`

, `listToSum`

would just become `length`

, `mappend :: Sum a`

would map to `(+)`

, and so on. We forget that any of these things formed a monoid.

## Natural Transformations

Moving our discussion from forgetful functors to free constructions requires the concept of natural transformations. Recall that a functor must take all objects to , and all morphisms to , such that the following diagram commutes:

This diagram says that it doesn’t matter if we start with , apply and then , or start with and instead apply and then - we always end up with . The functor has mapped between categories in a way that preserves the internal structure of the original category.

A *natural transformation* is a similar sort of structure-preserving^{5} mapping, except instead of mapping between categories, it maps between functors.

Given functors , a natural transformation is a morphism between functors such that:

For all , there exists a morphism, , where

^{6}For every morphism , the following diagram- a

*naturality square*- commutes:

This means we’re making a rather strong claim about the properties of : is the same as !

## Adjunctions

Let’s consider two functors going in opposite directions, and .

and aren’t just any old functors though- they’re equipped with a *natural isomorphism*:

where the isomorphism is natural in and .

Simply saying these hom-sets are naturally isomorphic is rather imprecise. We can pin down the naturality of by saying that certain natural transformations hold. But to define a natural transformation we need to define some functors!

We can define a natural transformation between these hom-functors from to , fixing :

We can use another notation to make their functorish nature more apparent:

These functors take every object to a hom-set of morphisms in , so it’s perfectly valid to ask for a natural transformation between them:

So for every morphism , applying and then precomposing with is the same as precomposing with and then applying . That’s naturality in . Naturality in is much the same, except we fix , and get functors from :

for all mophisms .

We can think of as a pair of hom-functors^{7} that take , and a pair of functors that take , such that each pair of functors creates a bijection between their corresponding sets, satisfying the above naturality conditions.

We describe this functorial relationship by saying that is *left adjoint* to , or .

## Free monoids

Armed with the ability to talk about the “adjointness” of functors, we can now examine what happens when we take to be a forgetful functor, when .

If is a forgetful functor that discards some information about its domain, must be able to “reconstruct” enough to go from to . The left adjoint to a forgetful functor is always a free functor!

Returning to our monoid example, if we take to be , the left adjoint to is the free functor .

This means there must be a natural isomorphism, , that creates a bijection between hom-sets of and , such that all functions to an underlying set of uniquely determines a monoid homomorphism that’s natural in and :

and vice-versa.

How could we construct so that the above conditions are met? Spoiler alert: we can just use List! Let’s try to translate , and its inverse, into pseudo-Haskell^{8}.

```
-- Just delete the monoid constraint
u :: Monoid m = m
alpha :: (List a -> Monoid m) = (a -> u (Monoid m))
alpha' :: (a -> u (Monoid m)) -> (List a -> Monoid m)
```

Now we can translate this into actual Haskell^{9}. Since `u`

just removes the monoid constraint, we can substitute all instances of `u (Monoid m)`

with simply `m`

, and we can use the real list constructor and type constraint syntax:

```
import Data.Monoid
alpha :: Monoid m => (a -> m) -> ([a] -> m)
alpha g xs = mconcat $ map g xs
alpha' :: Monoid m => ([a] -> m) -> (a -> m)
alpha' h x = h [x]
```

To prove that `alpha`

actually forms a natural isomorphism, we need to show that `alpha . alpha' = id`

:

```
-- Proof that alpha . alpha' = id
alpha . alpha'
-- eta expand
= \h x -> alpha (alpha' h) x
-- substitute definition of alpha'
= \h x -> alpha h [x]
-- substitute definition of alpha
= \h x -> mconcat (map h [x])
-- map f [x] = [f x]
= \h x -> mconcat ([h x])
-- mconcat [x] = x
= \h x -> h x
-- eta-reduce
= \h = h
-- definition of id
= id
```

and in the other direction, that `alpha' . alpha = id`

:

```
-- Proof that alpha' . alpha = id
alpha' . alpha
-- eta-expand
= \g xs -> alpha' (alpha g) xs
-- substitute definition of alpha
= \g xs -> mconcat (map (alpha g) xs)
-- eta-expand
= \g xs -> mconcat (map (\x -> alpha g x) xs)
-- substitute definition of alpha'
= \g xs -> mconcat (map (\x -> g [x]) xs)
-- map (f . g) = map f . map g
= \g xs -> mconcat (map g (map (\x -> [x]) xs))
-- free theorem
= \g xs -> g (mconcat (map (\x -> [x]) xs))
-- mconcat [[a],[b],[c]] = [a,b,c]
= \g xs -> g xs
-- eta-reduce
= \g -> g
-- definition of id
= id
```

So it follows that the list does indeed form a free monoid! Interestingly, what we’ve already defined as `alpha`

is just `foldMap`

:

```
alpha :: Monoid m => (a -> m) -> ([a] -> m)
foldMap :: Monoid m => (a -> m) -> [a] -> m
```

So in more Haskellish terms, we map each element of a list to a monoid, and then combine the results using the structure of that monoid.

```
ghci> foldMap Product [2,4,6]
Sum {getSum = 12}
ghci> foldMap Product [2,4,6]
Product {getProduct = 48}
```

Of course, `foldMap`

is really defining a monoid homomorphism, which means it should map the identity element:

```
ghci> foldMap Product []
Product {getProduct = 1}
ghci> foldMap Sum []
Product {getSum = 0}
```

…and preserve compositionality:

```
homomorphism :: [Int] -> [Int] -> Bool
homomorphism a b = phi (a ++ b) == phi a `mappend` phi b
where phi = foldMap Sum
```

```
ghci> quickCheck homomorphism
OK, passed 100 tests.
```

## Free Monads

Now let’s take a look at free monads. Of course, monads are just monoids in the category of endofunctors, so we can apply what we’ve already learned! A monad is an endofunctor equipped with natural transformations and , obeying the obvious^{10} axioms of identity and associativity. The category has monads as objects, and monad homomorphisms as arrows.

We can define a forgetful functor, , that maps from the category of monads to the category of endofunctors. The category of endofunctors, , has endofunctors as objects and natural transformations as arrows, so should be a forgetful functor such that:

- For every monad , will forget and , and just give us the underlying endofunctor .
- For every monad homomorphism , will give us a natural transformation in .

Now we can see what behaviour should have, when :

- For every endofunctor , should be a monad.
- For every natural transformation , should be a monad homomorphism.
- The isomorphism should be natural in and .

Again, this makes very strong claims about the behaviour of . It turns out that the following construction^{11} satisfies all these criteria:

We’re effectively asking for the existence of

```
data Free f a = Pure a | Free (f (Free f a))
instance Functor f => Monad (Free f) where
return a = Pure a
Pure a >>= f = f a
Free m >>= f = Free (fmap (>>= f) m)
```

The monadic bind operation `(>>=)`

can be defined in terms of “substitution followed by renormalization”:

```
Monad m => m a -> (a -> m b) -> m b
m >>= f = join (fmap f m)
```

In conventional monads, we substitute the `a`

in our monad `m a`

with `m b`

, to get `m m b`

, and then we renormalize with (which we call `join`

in Haskell) to get `m b`

. Free monads still perform the substitution of the underlying functor, but because `Free`

type is defined recursively as `Free (f (Free f a))`

, we effectively get for free by by sticking another layer of `Free`

on top. It’s a lossless process; everything you’ve joined is retained^{12}. In fact, `Free`

looks suspiciously like `List`

:

```
data List a = Nil | Cons (List a)
data Free f a = Pure a | Free (f (Free f a))
```

So `Free`

is basically just a list of functors! When we defined the free monoid, the natural isomorphism constraint basically forced us into defining `foldMap`

, which mapped each element of the list to a monoid, and then used the structure of that monoid to join the resulting elements:

```
foldMap :: Monoid m => (a -> m) -> [a] -> m
foldMap f xs = mconcat $ map f xs
```

Now we’re going to do the same for the free monad, by defining the natural transformation `foldFree`

, and its inverse, `foldFree'`

:

```
foldFree :: (Functor f, Monad m) =>
(forall a . f a -> m a) -> Free f a -> m a
foldFree' :: (Functor f, Monad m) =>
(forall a . Free f a -> m a) -> f a -> m a
```

Doing that is as simple as following the types:

```
foldFree _ (Pure x) = return x
foldFree phi (Free xs) = join $ phi $ fmap (foldFree phi) xs
foldFree' psi = psi . Free . (fmap Return)
```

Proving that `foldFree . foldFree' = id`

is left as an exercise for the reader.

As far as I understand, there’s no formal way of describing the “forgetfulness” of a functor.↩

A functor “preserves compositionality” if two morphisms of the input category compose to form a third morphism, such that the image of those two morphisms under the functor also compose to form the image of the third morphism.↩

All homomorphisms have one constraint in common: they must preserve compositionality. We can be generalise the homomorphism constraint for any -ary operation; a function is a homomorphism between two algebraic structures of the same type if: for all ↩

Technically, in Haskell we’d be mapping to the category , the category of Haskell types.↩

It’s actually exactly the same kind of structure preservation, because functors form a category where the objects are functors and the morphisms are natural transformations.↩

We call “the component of at ”↩

Category theory brings a great richness of perspectives, allowing us to think about relationships in whatever way that happen to suit whatever we’re trying to talk about.↩

I’m not sure of a way to write a polymorphic function that “forgets” a monoid constraint, so we’ll just wave our hands a bit until we get to Real Haskell.↩

This might look a bit strange- even though we’ve supposedly “forgotten” that

`m`

is a monoid in`alpha'`

, the type variable`m`

is still bound by the monoid type constraint. We can cheat, though, and explicitly parameterize a forgetful function`Monoid m => m -> b`

:↩`alpha Monoid m=>(b->m)->(a->b)->([a]->m) alpha m g xs = mconcat $ map (m . g) xs alpha' Monoid m=>(m->b)->([a]->m)->(a->b) alpha' m h x = m . h $ [x]`

Obvious to experienced category theorists, at least.↩

The way this construction defines the bind operator results in a quadratic asymtotic complexity. Janis Voigtlander describes an approach for reducing the asymtotic complexity to linear in his paper

*Asymtotic Improvement of Computations over Free Monads*.↩This gives an intuition for why any natural transformation between endofunctors, , can be fed to the free functor to form a monad homomorphism, . Just like the free monoid, we don’t “throw away” any information about the free construction beyond what’s defined by the underlying category.↩