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:

1. \(G\) has a left adjoint \(L\)
2. 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.