Free monads and their algebras

Today we are interested in the following theorem: The category of algebras of an endofunctor is isomorphic to the category of algebras of its free monad. It sounds complicated (and is rather not precise), so let me explain:

Free monads (arising from algebras). Let \mathcal{C} be a category, \Sigma be an endofunctor on \mathcal C, and \mathsf{Alg}(\Sigma) be the category of \Sigma-algebras. We can define a forgetful functor U : \mathsf{Alg}(\Sigma) \rightarrow \mathcal C as U (X, f) = X on objects, and U \beta = \beta on morphisms. Assume that U has a left adjoint, which we call F. As always in case of adjunctins, a monad arises. We call this monad the free monad generated by \Sigma, and denote it by \Sigma^*.

Free monads are initial algebras. If \mathcal{C} has finite products, we can prove that \Sigma^*X is equal to the initial algebra (if it exists) of the endofunctor \Sigma(-) + X. We name the action of this initial algebra \xi. So, the situation is:

\Sigma(\mu Y. \Sigma Y + X) + X \stackrel{\xi}{\rightarrow} \mu Y. \Sigma Y + X.

We split \xi into two components:

\eta : X \rightarrow \Sigma^*X
\eta = \xi \cdot inr

\alpha : \Sigma\Sigma^*X \rightarrow \Sigma^*X
\alpha = \xi \cdot inl

One can prove that \xi (and so \eta and \alpha) is natural in X.

We can provide another natural transformation, which, intuitively, transforms a \Sigma into its free monad:

\psi : \Sigma X \rightarrow \Sigma^*X
\psi = \alpha \cdot \Sigma \eta

Moreover, \eta is the unit of the monad \Sigma^*, and \mu = ( \hspace{-0.8mm} [ \alpha , id ] \hspace{-0.8mm} ) : \Sigma^*\Sigma^* \stackrel{\bullet}{\rightarrow} \Sigma^* is the multiplication of the monad.

Eilenberg-Moore algebras. Let (T, \mu^T, \eta^T) be a monad on \mathcal C. We define an (Eilenberg-Moore) T-algebra (aka “for T qua monad”) as an algebra (X \in \mathsf{Obj}(\mathcal C), f : TX \rightarrow X), where

(1) TTX \stackrel{\mu^T_X}{\longrightarrow} TX \stackrel{f}{\longrightarrow} X = TTX \stackrel{Tf}{\longrightarrow} TX \stackrel{f}{\longrightarrow} X

(2) X \stackrel{\eta^T_X}{\longrightarrow} TX \stackrel{f}{\longrightarrow} X = X \stackrel{\mathit{id}_X}{\longrightarrow} X

By \mathsf{EM}(T) we denote the category of Eilenberg-Moore T-algebras.

The theorem can now be stated as:

\mathsf{Alg}(\Sigma) is isomorphic to \mathsf{EM}(\Sigma^*).

Is there any use of such a theorem? It allows us to automatically transfer some properties from the simpler level of \Sigma-algebras to the world of free monads and initial algebras. This theorem will appear at least once more in this blog, so don’t forget about it too soon.

How to prove it? One way is to use Beck’s monadicity theorem (the “evil” version from Mac Lane’s book). It exactly fits the conditions about existence of adjoints, and the unintuitive condition about \Sigma creating coequalizers has a lot to do with (1). But we are (or at least I am) interested in something that can be encoded in Haskell more directly. So, let’s build an explicit isomorphism.

We define two functors (we should actually prove that they are really functors, but you know…):

J : \mathsf{EM}(\Sigma^*) \rightarrow \mathsf{Alg}(\Sigma)
J (X, f : \Sigma^*X \rightarrow X) = (X, f \cdot \psi)
J g = g

J^{-1} : \mathsf{Alg}(\Sigma) \rightarrow \mathsf{EM}(\Sigma^*)
J^{-1} (X, f : \Sigma X \rightarrow X) = (X, ( \hspace{-0.8mm} [ f, id ] \hspace{-0.8mm} ) )
J^{-1} g = g

To prove the theorem, we show that (A) J \cdot J^{-1} = Id_{\mathsf{Alg}(\Sigma)} and (B) J^{-1} \cdot J = Id_{\mathsf{EM}(\Sigma^*)}. We concentrate on objects, arrows are easy.


(J \cdot J^{-1}) (X, f) = (X, ( \hspace{-0.8mm} [ f, id ] \hspace{-0.8mm} ) \cdot \psi)

Since the functors do not alter the carrier of the algebra, we focus on the action:

( \hspace{-0.8mm} [ f, id ] \hspace{-0.8mm} ) \cdot \psi

= (def. of \psi)

( \hspace{-0.8mm} [ f, id ] \hspace{-0.8mm} ) \cdot \alpha \cdot \Sigma \eta

= (def. of \alpha, \eta)

( \hspace{-0.8mm} [ f, id ] \hspace{-0.8mm} ) \cdot \xi \cdot inl \cdot \Sigma \xi \cdot \Sigma inr

= (computation law)

[f, id] \cdot (\Sigma ( \hspace{-0.8mm} [ f, id ] \hspace{-0.8mm} ) + id) \cdot inl \cdot \Sigma \xi \cdot \Sigma inr

= (sum)

[f \cdot \Sigma ( \hspace{-0.8mm} [ f, id ] \hspace{-0.8mm} ) , id \cdot id] \cdot inl \cdot \Sigma \xi \cdot \Sigma inr

= (inl)

f \cdot \Sigma ( \hspace{-0.8mm} [ f, id ] \hspace{-0.8mm} ) \cdot \Sigma \xi \cdot \Sigma inr

= (comp. law)

f \cdot \Sigma [ f, id ] \cdot \Sigma(\Sigma ( \hspace{-0.8mm} [ f, id ] \hspace{-0.8mm} ) + id) \cdot \Sigma inr

= (sum + inr)

f \cdot \Sigma id

= (functor)




We first calculate:

f \cdot \psi \cdot \Sigma f

= (def. of \psi)

f \cdot \alpha \cdot \Sigma \eta \cdot \Sigma f

= (naturality of \eta)

f \cdot \alpha \cdot \Sigma \Sigma^* f \cdot \Sigma \eta

= (naturality of \alpha)

f \cdot \Sigma^* f \cdot \alpha \cdot \Sigma\eta

= (1)

f \cdot \mu \cdot \alpha \cdot \Sigma\eta

= (def. of \mu)

f \cdot ( \hspace{-0.8mm} [ \alpha, id ] \hspace{-0.8mm} ) \cdot \alpha \cdot \Sigma\eta

= (def. of \psi)

f \cdot ( \hspace{-0.8mm} [ \alpha, id ] \hspace{-0.8mm} ) \cdot \psi

= (similarly to A)

f \cdot \alpha


We use this result in the following calculation:

[f \cdot \psi, id] \cdot (\Sigma f + id)

= (sum)

[f \cdot \psi \cdot \Sigma f, id \cdot id]

= (prev. calculation)

[f \cdot \alpha, id \cdot id]

= (2)

[f \cdot \alpha, f \cdot \eta]

= (sum)

f \cdot [\alpha, \eta]

= (def. of \alpha, \eta)

f \cdot \xi


We use this result as a premise in the fusion law, hence:

( \hspace{-0.8mm} [ f \cdot \psi, id ] \hspace{-0.8mm} )

= (fusion)

f \cdot ( \hspace{-0.8mm} [ \xi ] \hspace{-0.8mm} )

= (reflection law)



We conclude:

(J^{-1} \cdot J) (X, f) = (X, ( \hspace{-0.8mm} [ f \cdot \psi, id ] \hspace{-0.8mm} )) = (X, f)


About Maciej Piróg

I am a functional programmer. I believe in large cardinals, axiom of choice, and that "P=NP" will not be solved in my lifetime. I think that category theory is abstract nonsense, and that is why it gives me this Monty-Python-style feeling of amusement.

3 responses to “Free monads and their algebras

  1. Znawca

    W jakiej kategorii?

Leave a Reply

Fill in your details below or click an icon to log in: Logo

You are commenting using your account. Log Out /  Change )

Google+ photo

You are commenting using your Google+ account. Log Out /  Change )

Twitter picture

You are commenting using your Twitter account. Log Out /  Change )

Facebook photo

You are commenting using your Facebook account. Log Out /  Change )


Connecting to %s

%d bloggers like this: