Free monads in category theory

Forgetting how to multiply

It’s probably easiest to understand what a free monad is if we first understand forgetful functors¹.

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

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 $(R,+,\cdot ,0,1)$, where $R$ is a set, and $(+,\cdot )$ are binary operations with identity elements $(0,1)$ respectively.

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

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

Forgetting monoids

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

The forgetful functor $M:Ring\to Mon$ maps from the category of rings to the category of monoids, $Mon$, 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 $X$, a monoid defined by $(X,\ast ,e)$, and $Y$, a monoid defined by $(Y,{\ast }^{\prime },f)$, a function $\varphi :X\to Y$ from $X$ to $Y$ is a monoid homomorphism iff:

it preserves compositionality³:

$$\varphi (a\ast b)=\varphi \left(a\right){\ast }^{\prime }\varphi \left(b\right),\forall ab\in X$$

and maps the identity element: $$\varphi \left(e\right)=f$$

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, $U:Mon\to Set$⁴.

$Set$ is a category where the objects are sets, and the arrows are just plain functions. So $U$ will map every monoid in $Mon$ 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 $F:C\to D$ must take all objects $X\in C$ to $F\left(X\right)\in D$, and all morphisms $f:X\to Y\in C$ to $F\left(f\right):F\left(X\right)\to F\left(Y\right)\in D$, such that the following diagram commutes:

$$\begin{array}{cccc}X& \stackrel{f}{\to }& Y& \\ F\downarrow & & \downarrow F& \\ F\left(X\right)& \stackrel{F\left(f\right)}{\to }& F\left(Y\right)& \end{array}$$

This diagram says that it doesn’t matter if we start with $X$, apply $F$ and then $F\left(f\right)$, or start with $X$ and instead apply $f$ and then $F$- we always end up with $F\left(Y\right)$. 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⁵ mapping, except instead of mapping between categories, it maps between functors.

Given functors $F,G:C\to D$, a natural transformation $\eta$ is a morphism between functors such that:

1. For all $X\in C$, there exists a morphism, ${\eta }_X:F\left(X\right)\to G\left(X\right)$, where $F\left(X\right),F\left(G\right)\in D$⁶

2. For every morphism $f:X\to Y\in C$, the following diagram- a naturality square- commutes:

$$\begin{array}{cccc}F\left(X\right)& \stackrel{F\left(f\right)}{\to }& F\left(Y\right)& \\ {\eta }_X\downarrow & & \downarrow {\eta }_Y& \\ G\left(X\right)& \stackrel{G\left(f\right)}{\to }& G\left(Y\right)& \end{array}$$

This means we’re making a rather strong claim about the properties of $\eta$: $G\left(f\right)\circ \eta$ is the same as $\eta \circ F\left(f\right)$!

Adjunctions

Let’s consider two functors going in opposite directions, $F:C\to D$ and $G:D\to C$.

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

$$\alpha :D\text{(}FX,Y\text{)}\cong C\text{(}X,GY\text{)}$$

where the isomorphism is natural in $X$ and $Y$.

Simply saying these hom-sets are naturally isomorphic is rather imprecise. We can pin down the naturality of $\alpha$ 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 $X\in C$ to $Y\in D$, fixing $Y$:

$$D\text{(}F\_,Y\text{)}$$

$$D\text{(}\_,GY\text{)}$$

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

$$X\mapsto \text{hom}(FX,Y):C^{op}\to Set$$

$$X\mapsto \text{hom}(X,GY):C^{op}\to Set$$

These functors take every object $X\in C^{op}$ to a hom-set of morphisms in $D$, so it’s perfectly valid to ask for a natural transformation between them:

$$\begin{array}{cccc}D\text{(}F{X}^{\prime },Y\text{)}& \stackrel{\alpha }{\to }& C\text{(}{X}^{\prime },GY\text{)}& \\ \_\circ Ff\downarrow & & \downarrow \_\circ f& \\ D\text{(}FX,Y\text{)}& \stackrel{\alpha }{\to }& C\text{(}X,GY\text{)}& \end{array}$$

So for every morphism $f:X^{\prime }\to X\in C$, applying $\alpha$ and then precomposing with $f$ is the same as precomposing with $Ff$ and then applying $\alpha$. That’s naturality in $X$. Naturality in $Y$ is much the same, except we fix $X$, and get functors from $D\to Set$:

$$\begin{array}{cccc}D\text{(}FX,Y\text{)}& \stackrel{\alpha }{\to }& C\text{(}X,GY\text{)}& \\ g\circ \_\downarrow & & \downarrow Gg\circ \_& \\ D\text{(}FX,Y^{\prime }\text{)}& \stackrel{\alpha }{\to }& C\text{(}X,G{Y}^{\prime }\text{)}& \end{array}$$

for all mophisms $g:Y\to Y^{\prime }\in D$.

We can think of $\alpha$ as a pair of hom-functors⁷ that take $C^{op}\to Set$, and a pair of functors that take $D\to Set$, 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 $F$ is left adjoint to $G$, or $F⊣G$.

Free monoids

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

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

Returning to our monoid example, if we take $U$ to be $U:Mon\to Set$, the left adjoint to $U$ is the free functor $F:Set\to Mon$.

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

$$\alpha :Mon\text{(}Fa\to b)\cong Set\text{(}a\to Ub\text{)}$$

and vice-versa.

How could we construct $F$ so that the above conditions are met? Spoiler alert: we can just use List! Let’s try to translate $\alpha$, and its inverse, into pseudo-Haskell⁸.

-- 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⁹. 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 $T:C\to C$ equipped with natural transformations $\eta :1_C\Rightarrow T$ and $\mu :T^2\Rightarrow T$, obeying the obvious¹⁰ axioms of identity and associativity. The $Monad$ category has monads as objects, and monad homomorphisms as arrows.

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

• For every monad $T$, $U$ will forget $\eta$ and $\mu$, and just give us the underlying endofunctor $T$.
• For every monad homomorphism $\varphi$, $U$ will give us a natural transformation in $End$.

Now we can see what behaviour $F$ should have, when $F⊢U$:

• For every endofunctor $A$, $FA$ should be a monad.
• For every natural transformation $\eta :A\Rightarrow B$, $F\eta$ should be a monad homomorphism.
• The isomorphism $FA\Rightarrow B\cong A\Rightarrow UB$ should be natural in $A$ and $B$.

Again, this makes very strong claims about the behaviour of $F$. It turns out that the following construction¹¹ 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 $\mu :T^2\Rightarrow T$ (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 $\mu :T^2\Rightarrow T$ for free by by sticking another layer of Free on top. It’s a lossless process; everything you’ve joined is retained¹². 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.