Introduction

In the previous post, I introduced the notion of monadic functor, exemplified by the forgetful functor from the category of monoids to \(\mathsf{Set}\). We saw that monoids form a subcategory of the category of algebras of the functor \(F\) defined by \(F X = 1 + X²\), and we observed that those are the same as the monad algebras of the list monad.

Algebraically free monads

More generally, we can try different subcategories of \(\mathsf{Alg}_F\) and check whether they are monadic as well. So let’s start with possibly the simplest one: the whole of \(\mathsf{Alg}_F\).

This leads us to the following definition: we say that an endofunctor \(F\) admits an algebraically free monad if \(\mathsf{Alg}_F\) is monadic. The corresponding monad is called the algebraically free monad over \(F\).

Informally, the algebraically free monad over \(F\) is a monad \(T\) such that monad algebras of \(T\) are the same as functor algebras of \(F\).

Unfortunately, not all functors admit an algebraically free monad. For example, it is easy to see that the powerset functor does not.

Free monads as initial algebras

The free package on Hackage defines something called “free monad” for every Haskell functor. What does this have to do with the notion of algebraically free monad defined above?

Here is the definition of Free from the above package:

data Free f a
  = Pure a
  | Free (f (Free f a))

Translating into categorical language, we can define, for an endofunctor \(F\), the functor \(F^*\), which returns, for a set \(X\), a fixpoint of the functor \[ G Y = X + F Y. \]

Let’s assume that the fixpoint is to be intended as inductive, i.e. as an initial algebra. Therefore, we get, for all objects \(X\), an initial algebra: \[ X + F (F^* X) → F^* X. \]

Of course, those initial algebras might not exist, but they do if we choose \(F\) carefully. For example, if \(F\) is polynomial, then all the functors \(G\) above are also polynomial, thus they have initial algebras.

In general, if we assume that those initial algebras all exist, then we can prove that the resulting functor \(F^*\) is a monad, and is indeed the algebraically free monad over \(F\).

We will first show that \(F^*\) allows us to define a left adjoint \(L\) for the forgetful functor \(U : \mathsf{Alg}_F → \mathsf{Set}\). In fact, for any set \(X\), let the carrier of \(L X\) be \(F^* X\), and define the algebra morphism by restriction from the initial algebra structure on \(F^* X\): \[ F (F^* X) → X + F (F^* X) → F^* X. \]

By definition, \(F^* X\) is the initial object in the category of algebras of the functor \(Y ↦ X + F Y\). Moreover, it is easy to see that the latter category is equivalent to the comma category \((X ↓ U)\), where the equivalence maps \(F^* X\) to the obvious morphism \(X → U L X\). By the characterisation of adjunctions in terms of universal arrows, it follows that \(L\) is left adjoint to \(U\). Clearly, \(U L = F^*\), therefore \(F^*\) is a monad.

To conclude the proof, we need to show that the adjunction \(L ⊣ U\) is monadic, i.e. that the comparison functor from \(F\)-algebras to \(F^*\)-algebras is an equivalence. One way to do that is to appeal to Beck’s monadicity theorem. Verifying the hypotheses is a simple exercise.

It is also instructive to look at the comparison functor as implemented in haskell:

iter :: Functor f => (f x → x) → (Free f x → x)
iter θ (Pure x) = x
iter θ (Free t) = θ (fmap (iter θ) t)

and its inverse

uniter : Functor f => (Free f x → x) → (f x → x)
uniter ψ = ψ . liftF
  where liftF = Free . fmap Pure

It is not hard to prove directly, using equational reasoning, that iter θ is a monad algebra, and that iter and uniter are inverses to each other.

Algebraically free monads are free

The documentation for Free says:

A Monad n is a free Monad for f if every monad homomorphism from n to another monad m is equivalent to a natural transformation from f to m

which doesn’t look at all like our definition of algebraically free monad. Rather, this says that \(N\) is defined to be the free monad over \(F\) if the canonical natural transformation \(F → N\) is a universal arrow from \(F\) to the forgetful functor \(\mathsf{Mon}(\mathsf{Set}) → \mathsf{Func}(\mathsf{Set}, \mathsf{Set})\).

If that forgetful functor had a left adjoint, then we could just say that the free monad is obtained by applying this left adjoint to any endofunctor. This is actually the case if we replace \(\mathsf{Set}\) with a so-called algebraically complete category, such as the ones modelled by Haskell, where the left adjoint is given by the (higher order) functor Free.

In \(\mathsf{Set}\), however, we need to stick to the more awkward definition in terms of universal arrows, as not all functors are going to admit free monads. In any case, the relationship with the previously defined notion of algebraically free monad is not immediately clear.

Fortunately, we can prove that a monad is algebraically free if and only if it is free! Proving that an algebraically free monad \(F^*\) on \(F\) is free amounts to proving that the following natural transformation (corresponding to liftF in the Haskell code above):

\[ F X \xrightarrow{F \eta} F (F^* X) \to F^* X \]

is universal, which is a simple exercise.

To prove the converse, we will be using Haskell notation. Suppose given a functor f, and a monad t that is free on f. Therefore, we have a natural transformation:

l :: f x → t x

and a function that implements the universal property for t:

hoist :: Monad m => (∀ x . f x → m x) → t x → m x

Now we define a functor \(\mathsf{Set}→ \mathsf{Alg}_f\) which is going to be the left adjoint of the forgetful functor. The carrier of this functor is given by t itself, so we only need to define the algebra morphism:

alg :: f (t x) → t x
alg u = join (l u)

To show that this functor is the sought left adjoint, we have to fix a type x and an f-algebra θ : f y → y, define functions:

φ :: (x → y) → (t x → y)
ψ :: (t x → y) → (x → y)

then prove that φ g is an f-algebra morphism for all g : x → y, and that φ and ψ are inverses to each other.

The function ψ is easy to implement:

ψ a h = h . return

Defining φ is a bit more involved. The only tool at our disposal to define functions out of t x is hoist. For that, we need a monad m, and a natural transformation f → m.

The trick is to consider the continuation monad Cont y. Using θ, we define a natural transformation

w :: f z → Cont y z
w u = Cont (\k -> θ (fmap k u))

on which we can apply the universal property of t to get φ:

φ g = (`runCont` id) . hoist w . fmap g

From here, the proof proceeds by straightforward equational reasoning, and is left as an exercise.

Conclusion

We looked at two definitions of “free monad”, proved that they are equivalent, and shown the relationship with the Haskell definition of Free. In the next post, we will resume our discussion of algebraic theories “with laws” and try to approach them from the point of view of free monads and monadic functors.