# Free monads in category theory

Part II of the series Free monads.
March 23, 2016

## Forgetting how to multiply

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

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

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,+,,0,1), where R is a set, and (+,) 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:RingRng, which just drops the multiplicative identity.

Similarly, we can define another forgetful functor A:RngAb, 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,,e), where S is a set, is an associative binary operation, and e is the neutral element of that operation.

The forgetful functor M:RingMon 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,,e), and Y, a monoid defined by (Y,,f), a function ϕ:XY from X to Y is a monoid homomorphism iff:

it preserves compositionality3:

ϕ(ab)=ϕ(a)ϕ(b),abX

and maps the identity element: ϕ(e)=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:MonSet4.

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:CD must take all objects XC to F(X)D, and all morphisms f:XYC to F(f):F(X)F(Y)D, such that the following diagram commutes:

Xf−−−YFFF(X)F(f)−−−F(Y)

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

Given functors F,G:CD, a natural transformation η is a morphism between functors such that:

1. For all XC, there exists a morphism, ηX:F(X)G(X), where F(X),F(G)D6

2. For every morphism f:XYC, the following diagram- a naturality square- commutes:

F(X)F(f)−−−F(Y)ηXηYG(X)G(f)−−−G(Y)

This means we’re making a rather strong claim about the properties of η: G(f)η is the same as ηF(f)!

Let’s consider two functors going in opposite directions, F:CD and G:DC.

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

α:D(FX,Y)C(X,GY)

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 α 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 XC to YD, fixing Y:

D(F_,Y)

D(_,GY)

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

Xhom(FX,Y):CopSet

Xhom(X,GY):CopSet

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

D(FX,Y)α−−−C(X,GY)_Ff_fD(FX,Y)α−−−C(X,GY)

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

D(FX,Y)α−−−C(X,GY)g_Gg_D(FX,Y)α−−−C(X,GY)

for all mophisms g:YYD.

We can think of α as a pair of hom-functors7 that take CopSet, and a pair of functors that take DSet, 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 FG.

## 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 FU.

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:MonSet, the left adjoint to U is the free functor F:SetMon.

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

α:Mon(Fab)Set(aUb)

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 α, and its inverse, into pseudo-Haskell8.

-- 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 Haskell9. 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:CC equipped with natural transformations η:1CT and μ:T2T, obeying the obvious10 axioms of identity and associativity. The Monad category has monads as objects, and monad homomorphisms as arrows. We can define a forgetful functor, U:MonadEnd, 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 η and μ, and just give us the underlying endofunctor T. • For every monad homomorphism ϕ, U will give us a natural transformation in End. Now we can see what behaviour F should have, when FU: • For every endofunctor A, FA should be a monad. • For every natural transformation η:AB, Fη should be a monad homomorphism. • The isomorphism FABAUB should be natural in A and B. Again, this makes very strong claims about the behaviour of F. It turns out that the following construction11 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 μ:T2T (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 μ:T2T for free by by sticking another layer of Free on top. It’s a lossless process; everything you’ve joined is retained12. 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.

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

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

3. All homomorphisms have one constraint in common: they must preserve compositionality. We can be generalise the homomorphism constraint for any n-ary operation; a function f:AB is a homomorphism between two algebraic structures of the same type if: f(μA(a1,,an))=μB(f(a1),,f(an)) for all a1,,anA

5. 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.

6. We call ηX “the component of η at X

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

8. 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.

9. 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]
10. Obvious to experienced category theorists, at least.

11. 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.

12. This gives an intuition for why any natural transformation between endofunctors, f:AUB, can be fed to the free functor to form a monad homomorphism, Ff:FAB. Just like the free monoid, we don’t “throw away” any information about the free construction beyond what’s defined by the underlying category.