# Free monads in category theory (part 1)

## Introduction

Free monads can be used in Haskell for modelling a number of different concepts: trees with arbitrary branching, terms with free variables, or program fragments of an EDSL.

This series of posts is *not* an introduction to free monads in Haskell, but to the underlying theory. In the following, we will work in the category \(\mathsf{Set}\) of sets and functions. However, most of what we say can be trivially generalised to an arbitrary category.

## Algebras of a functor

If \(F\) is an endofunctor on \(\mathsf{Set}\), an **algebra** of \(F\) is a set \(X\) (called its *carrier*), together with a morphism \(FX → X\). Algebras of \(F\) form a category, where morphisms are functions of their respective carriers that make the obvious square commute.

Bartosz Milewski wrote a nice introductory post on functor algebras from the point of view of functional programming, which I strongly recommend reading to get a feel for why it is useful to consider such objects.

More abstractly, a functor \(F : \mathsf{Set}→ \mathsf{Set}\) generalises the notion of a *signature* of an algebraic theory. For a signature with \(a_i\) operators of arity \(i\), for \(i = 0, \ldots, n\), the corresponding functor is the polynomial: \[
F X = a₀ + a₁ × X + ⋯ + a_n × X^n,
\] where the natural number \(a_i\) denotes a finite set of cardinality \(a_i\).

For example, the theory of monoids has 1 nullary operation, and 1 binary operation. That results in the functor: \[ F X = 1 + X^2 \]

Suppose that \((X, θ)\) is an algebra for this particular functor. That is, \(X\) is a set, and \(θ\) is a function \(1 + X² → X\). We can split \(θ\) into its two components: \[ θ_e : 1 → X, \] which we can simply think of as an element of \(X\), and \[ θ_m : X × X → X. \]

So we see that an algebra for \(F\) is exactly a set, together with the operations of a monoid. However, there is nothing that tells us that \(X\) is indeed a monoid with those operations!

In fact, for \(X\) to be a monoid, the operations above need to satisfy the following laws: \[ \begin{aligned} & θ_m (θ_e(∗), x) = x \\ & θ_m (x, θ_e(∗)) = x \\ & θ_m (θ_m (x, y), z) = θ_m (x, θ_m (y, z)). \end{aligned} \]

However, any two operations \(θ_e\) and \(θ_m\) with the above types can be assembled into an \(F\)-algebra, regardless of whether they do satisfy the monoid laws or not.

## “Lawful” algebras

The above example shows that functor algebras don’t quite capture the general notion of “algebraic structure” in the usual sense. They can express the idea of a set equipped with operations complying to a given signature, but we cannot enforce any sort of *laws* on those operations.

For the monoid example above, we noticed that we can realise any actual monoid as an \(F\)-algebra (for \(FX = 1 + X²\)), but that not every such algebra is a monoid. This means that monoids can be regarded as the objects of the subcategory of \(\mathsf{Alg}_F\) consisting of the “lawful” algebras (exercise: make this statement precise and prove it).

Therefore, we have the following commutative diagram of functors:

and it is easy to see that \(U\) (which is just the restriction of the obvious forgetful functor \(\mathsf{Alg}_F → \mathsf{Set}\) on the right side of the diagram) has a left adjoint \(L\), the functor that returns the free monoid on a set.

Explicitly, \(LX\) has \(X^*\) as carrier (i.e. the set of *lists* of elements of \(X\)), and the algebra is given by the coproduct of the function \(1 → X^*\) that selects the empty list, and the list concatenation function \(X^* × X^* → X^*\).

In Haskell, this algebra looks like:

alg :: Either () ([x], [x]) → [x] alg (Left _) = [] alg (Right (xs, ys)) = xs ++ ys

The endofunctor \(UL\), obtained by taking the carrier of the free monoid, is a monad, namely the *list monad*.

## Algebras of a monad

Given a monad \((T, η, μ)\) on \(\mathsf{Set}\), a monad algebra of \(T\) is an algebra \((X, θ)\) of the underlying functor of \(T\), such that the following two diagrams commute:

In Haskell notation, this means that the following two equations are satisfied:

θ (return x) = x θ (fmap θ m) = θ (join m)

In the case where the monad \(T\) returns the set of “terms” of some language for a given set of free variables, a monad algebra can be thought of as an evaluation function.

The first law says that a variable is evaluated to itself, while the second law expresses the fact that when you have a “term of subterms”, you can either evaluate every subterm and then evaluate the resulting term, or regard it as a single term and evaluate it directly, and these two procedures should give the same result.

Naturally, monad algebras of \(T\) form a full subcategory of \(\mathsf{Alg}_T\) which we denote by \(\mathsf{mAlg}_T\).

We can now go back to our previous example, and look at what the monad algebras for the list monad are. Suppose we have a set \(X\) and a function \(θ : X^* → X\) satisfying the two laws stated above.

We can now define a monoid instance for \(X\). In Haskell, it looks like this:

instance Monoid X where empty = θ [] mappend x y = θ [x, y]

The monoid laws follow easily from the monad algebra laws. Verifying them explicitly is a useful (and fun!) exercise. Vice versa, any monoid can be given a structure of a \(T\)-algebra, simply by taking `mconcat`

as \(θ\).

Therefore, we can extend the previous diagram of functors with an equivalence of categories:

where the top-left equivalence (which is actually an isomorphism) is determined by the `Monoid`

instance that we defined above, while its inverse is given by `mconcat`

.

Let’s step back at this whole derivation, and reflect on what it is exactly that we have proved. We started with some category of “lawful” algebras, a subcategory of \(\mathsf{Alg}_F\) for some endofunctor \(F\). We then observed that the forgetful functor from this category to \(\mathsf{Set}\) admits a left adjoint \(L\). We then considered monad algebras of the monad \(UL\), and we finally observed that these are exactly those “lawful” algebras that we started with!

## Monadic functors

We will now generalise the previous example to an arbitrary category of algebra-like objects.

Suppose \(\mathsf{D}\) is a category equipped with a functor \(G : \mathsf{D} → \mathsf{Set}\). We want to think of \(G\) as some sort of “forgetful” functor, stripping away all the structure on the objects of \(\mathsf{D}\), and returning just their carrier.

To make this intuition precise, we say that \(G\) is *monadic* if:

- \(G\) has a left adjoint \(L\)
- The
*comparison functor*\(\mathsf{D} → \mathsf{mAlg}_T\) is an equivalence of categories, where \(T = GL\).

The comparison functor is something that we can define for any adjunction \(L ⊢ G\), and it works as follows. For any object \(A : \mathsf{D}\), it returns the monad algebra structure on \(G A\) given by \(G \epsilon\), where \(\epsilon\) is the counit of the adjunction (exercise: check all the details).

So, what this definition is saying is that a functor is monadic if it really is the forgetful functor for the category of monad algebras for some monad. Sometimes, we say that a *category* is monadic, when the functor \(G\) is clear.

The monoid example above can then be summarised by saying that the category of monoids is monadic.

## Conclusion

I’ll stop here for now. In the next post we will look at algebraically free monads and how they relate to the corresponding Haskell definition.

## Comments