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 , 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³:

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, ⁴.

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⁵ mapping, except instead of mapping between categories, it maps between functors.

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

1. For all , there exists a morphism, , where ⁶

2. 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⁷ 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⁸.

-- 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 equipped with natural transformations and , obeying the obvious¹⁰ 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¹¹ 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¹². 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.