The basic theory of monads and their connection to
universal algebra
Anthony Voutas
May 2012
Abstract
This paper gives the definition of monads and outlines the key properties and theorems
concerning how monads relate to adjunctions and universal algebra, giving the EilenbergMoore construction and showing that varieties can be studied with monads. It provides asummary of the key applications and potential of the monadic and comonadic view, including
representing and reasoning about data structures, examining an alternative perspective on
universal (co)algebra and exploring adjunctions in yet another different way. It also mentions
some historical facts about the subject.

1

Introduction

From a basic point of view, category theory is a formal abstract theory of functions. However,with a little theoretical development, it provides a framework for defining and exploring mathematical concepts in general. It facilitates reasoning about objects at the appropriate level ofabstraction by adding external constraints on the properties of objects instead of examining
overly specific, complicated (internal) constructions of objects.
Mathematicians are more often concerned with the properties of objects, rather than their internal structure. This is not to say that internal structure is completely ignored by category
theory. In fact, categorical concepts can help to reason about and elucidate the internal structure of many algebraic objects, the notion of category itself being a generalisation of monoids
and partial orders.
The usefulness of category theory lies in its departure from defining new objects constructively.
Instead, category theory defines objects by their unique behaviour (in the sense that all objects
behaving similarly will be isomorphic – and thus interchangeable). Thus, category theory allows
us to reason purely with properties, never having to examine the internals of objects. This is thesource of category theory’s power. Moreover, objects defined in this way don’t necessarily exist
in any given category. This allows category theory to operate at different levels of abstraction.
We can consider categories in which a particular type of object always exists, but then we canalways return to the more general case. This is not impossible to simulate in other languages ofmathematics, but the language of category theory can make these distinctions natural. This is
the source of category theory’s versatility.
Category theory also allows the realisation of certain mathematical concept which go largely
unnoticed by the rest of mathematics. Examples of adjunctions are ubiquitous in mathematics,

1

Monads

Anthony Voutas

but the general definition and exposition of adjunctions can only be seen through category theory. Even the existence of these relationships in particular circumstances usually remains unseen
until category theory is applied. Monads are just as ubiquitous as adjunctions, as will be seen
later, and similarly remain unseen until category theory is applied to the situations in question.
The first monad explicitly constructed was presented by Roger Godemont in 1958 [1]. Though,it should be clarified that at the time, instead of using the name monad, he used “Standard
Constructions”, which indicates that they already existed without being explicitly generalised.
This is true for much of basic category theory, and in fact at the time Godemont was writing
about algebraic topology and sheaf theory, not explicitly category theory. This shouldn’t be too
surprising, as much of the foundational work in category theory was done to provide tools for
either algebraic topologists or universal algebraists.
The concept of a monad has gone by a few other names over the years. Triple, triad, standard construction, fundamental construction and monad have all been used at one point or
another. Both the terms standard construction and fundamental construction are vague and notparticularly unique, the term triple is even less unique, triad means more or less the same as
triple, and monad is a pre-existing term in the English language meaning more or less “a single
unit”, and is used in philosophy to refer to an indivisible entity, among other things.
A monad is essentially a monoid in an endofunctor category, and because of this the namemonad is somewhat of a pun on the word monoid. However, ‘monad’ is highly misleading terminology as we will see that a monad can be ‘split’ by any of the adjunctions which can be usedgenerate it, and moreover a monad is constructed from three other objects. An entity built fromthree entities and able to split into four entities (an adjunction is made up from four objects) ishardly monadic in the philosophical sense.
There was a time when all the names were used, but the convention has been settled and thename monad now predominates the literature. The popularity of the term monad is probably
due to Saunders Mac Lane, via his prominent and influential book Category Theory for theWorking Mathematician [2]. While discussing monads in the book, he provides justification forabandoning the term triple.
On a more technical note, monads have been used to provide and explore a different view ofuniversal algebra. This approach is supported by the fact that varieties can be represented via
monads. This is a result of the following connections which will be explored more thoroughlylater in this report.
An adjunction between categories A and B gives rise to a monad T on A. The monad T can thenbe used to construct an adjunction between A and a generalised category of algebras AT (The
Eilenberg-Moore construction). There is then a comparison functor from the original category
B to AT , and this is an isomorphism if a particular property is satisfied (call it X for now).
Varieties admit free constructions (that is an adjunction between a free functor and a forgetful
functor). Starting with a the free-forgetful adjunction for a variety, one can form the monadand then the Eilenberg-Moore adjunction. Then the property X is satisfied. In this way we canconstruct an isomorphism between the category of the variety and the category of algebras forthe monad for that variety. The notion of an algebra of the variety can now be captured by thenotion of an algebra for the monad.

2

Monads

Anthony Voutas

Thus, because universal algebra is essentially the study of varieties, monads are capable ofrepresenting the objects of study of universal algebra. Moreover, it can be useful to look at monads in order to prove general theorems about universal algebra, because monads admit many
nice properties. For starters, the monads for varieties exist entirely in the category of sets andfunctions, which is a very well understood category, whereas arbitrary variety categories can be
unusual. Moreover, monads are defined in a categorical way, which allows many different things
to be considered which aren’t as obvious in the algebraic signature view, such as morphisms
between varieties.
Monads provide a general definition for free constructions which is both general and simple.
Meanwhile, a particular free construction can be very complicated and messy. These characteristics make monads good for use in general proofs about free constructions, which takes some of
the burden off those working with particularly complicated free constructions.
Monads are also very useful in the context of functional programming. They can be used toreason about and represent recursive data structures, and even provide a way of constructing
a notion of structural induction for the defined data structures (via the initial algebra for themonad). Being able to define structural induction on a data structure is key to proving thecorrectness of recursive functions operating on that data structure.
Monads are used in functional programming languages to provide a general interface for thecreation and use of data structures. Polymorphic functions can be written to be applied to any
monad. Since monads can be used to represent basically any recursive data structure, polymorphic functions are extremely general when applied to the type-class of monads.
The concept of monad has been generalised to that of an arrow [3] in functional programming
languages like Haskell, in order to provide more flexibility in the creation of data structures.
Such generalisations require detailed knowledge of the concept of a monad, its strengths andits weaknesses. Monads have a slew of applications in the functional programming language
Haskell [4], including simplifying program code [3] and formalising side-effect free parallelism [5].
Furthermore, in category theory, the existence of a concept automatically produces the existence of a dual concept. In the case of monads, that concept is a comonad. The properties of acomonad are directly dual to that of a mona. So, comonads are also generated by an adjunction
and are useful for examining coalgebra. It so happens that coalgebra is an extremely useful way
of examining state-transition systems [6], and there is a deep connection between coalgebra andmodal logic [7] which is analogous to the connection between algebra and equational logic.
This connection is already well established and explored in the literature, but as coalgebraic
modal logic is a relatively new subfield there are currently many opportunities for its application
to be extended and for the surrounding concepts to be further explored in general.
The concept of monad extends beyond algebra though, since it is directly connected to theconcept of adjunctions, which are ubiquitous in mathematics and theoretical computer science.
A monad can provide a different view of any adjunction, essentially the view of the adjunction
taken inside one of the categories (with a comonad being in the other). Examining these monads
could lead to new insights in many fields and could be easier to manage than the adjunctions
themselves.

3

Monads

Anthony Voutas

With regards to universal algebra, Lawvere theories [8] are similar to monads, in that they
are both categorical formalisms for reasoning about algebraic varieties. Monads can be criticisedfor obscuring the original equations of the varieties, while Lawvere theories present the equations
more prominently.
It so happens that every Lawvere theory has a corresponding monad on Set, the converse beingtrue only for a generalisation of Lawvere theories to arities of arbitrary size [9]. So, in addition todisplaying equations more prominently, Lawvere theories can make a clearer distinction between
finitary algebra and infinitary algebra, whereas monads rely on a more subtle notion of rank torepresent this fact.
With all this in mind, obfuscation of the equations might be useful or required in practice.
Certainly, in functional programming applications hiding the internal structure of the monadis intended and useful in practice [3]. In addition, the theory of monads has been thoroughly
developed so it still has useful applications in universal algebra, even if in principle the conceptof Lawvere theory might be more useful. Furthermore, the development of theory surrounding
monads might be evidence that it is an easier concept to work with in the abstract, and this is
supported when examining the development of Lawvere theories for arbitrary categories [9, §5].
All in all, this does not diminish the applicability of monads to functional programming or to
examining adjunctions in general.
The theory contained in this report is entirely standard, and there are no original results.
This is merely a restating of work that is widely available in standard textbooks on these issues [2] [10] [1], with the exception of the discussion in Section 5, which is no more original, butslightly less prominent. This report has the following structure. Section 1 has been the introduction, informally covering some of the theoretical notions, outlining applications, and reviewing
the history of the concept. In Section 2, some necessary (but slightly less than basic) category
theory notions are presented to fix notation and prepare the reader for the rest of the report.
Also in Section 2, two concepts of algebra are given, the standard universal algebra notion of avariety, and the notion of an algebra for a functor. Then in Section 3 the connection between
monads and adjunctions are explored, and we show that a monad can be built from an adjunction, and that a monad can be split into an adjunction. In Section 4 the connection between
monads and universal algebra (via free-faithful adjunctions) is explored, and we prove that all
varieties have a corresponding monad, and that the Eilenberg-Moore category for that monad isisomorphic to the variety (when taken as a category). In section 5 the dual notion of a comonadis stated and some applications of coalgebra are given. Finally, and briefly, some avenues for
future research are presented.

4

Monads2

Anthony Voutas

Preliminary Details

Before launching into the technical details of what monads are and how they relate to adjunctions
and algebra, it is necessary to establish a few definitions and facts from category theory anduniversal algebra.

2.1

Horizontal composition of natural transformations

Recall that natural transformations can be composed in two different ways. Firstly they can becomposed vertically by composing their components. A slightly less utilised composition is thehorizontal composition, defined as follows [2, §II.5]:
Suppose we have the following functors and natural transformations:
S
A

T
σ

B

τ

C

T0

S0

Then we can form the composite functors T S, T 0 S, T S 0 and T 0 S 0 all from A to C, and we canconstruct a diagram (for X ∈ A):
T S(X)τS(X)

T 0 S(X)T 0 (σX )T (σX )T S 0 (X)τS 0 (X)

T 0 S 0 (X)This diagram commutes because it is the naturality diagram for τ with σX substituted for thegeneral arrow. We can now define the diagonal of this square to be the horizontal composite
τ σ. Note that in this document the notation for vertical composition will be α ◦ β, while thenotation for horizontal composition will be αβ (obviously it is not possible to compose any twonatural transformations, and natural transformations that can be composed horizontally cannot
necessarily be composed vertically or vice versa. We will later be using natural transformations
between endofunctors, which can always be composed horizontally).
In summary:Definition 2.1.1. The natural transformation which is the horizontal composition of the twonatural transformations τ : T →˙ T 0 and σ : S →˙ S 0 is given by the components:(τ σ)X = T 0 (σX ) ◦ τS(X) = τS 0 (X) ◦ T (σX )(1)This is always well defined if the codomain of S and S 0 matches the domain of T and T 0 .

2.2

Triangle identities for an adjunction

The triangle identities for an adjunction is a convenient equivalent definition for adjunction which
doesn’t refer explicitly to universal arrows or bijection of homsets [2, §IV.1 Theorem 2].
5

Monads

Anthony Voutas

Definition 2.2.1. [Triangle identities for an adjunction] Given that A and B are categories, anadjunction is a tuple hF, G, η, i, where F and G are functors F : A → B, G : B → A, and η
and  are natural transformations η : 1A →GF
˙,  : F G→1
˙ B such that the following diagrams
commute:
ηG

Fη

G

GF G

F

F GF

G

F

G

2.3

F

An aside about whiskering

Before going on to define a monad, it may be helpful to reflect on some facts about naturaltransformations. We will restrict our interests to particular types of natural transformations, forreasons which will become clear in the next section.
Using horizontal composition of natural transformations we can create a new natural transformation by whiskering a natural transformation by a functor [11]. Whiskering a naturaltransformation α by a functor F is done by horizontally composing α and the natural transformation 1F .
In general, given the following diagram of functors F, G, H, K and natural transformation α:
G
A

F

α

B

C

K

D

H
We can form the following natural transformations: (1K α by horizontal composition)
Kα : KG →˙ KH(Kα)B : KG(B) → KH(B)(Kα)B = K(αB )and (α1F by horizontal composition)
αF : GF →˙ HF(αF )A : GF (A) → HF (A)(αF )A = αF (A)Note that for an endofunctor T , we will take T 2 := T ◦ T and T 3 := T ◦ T ◦ T . Now with T
being an endofunctor on C, 1T being the identity natural transformation on T and η : 1C →˙ Tand µ : T 2 →˙ T being natural transformations, we can make the following observations (from thedefinition of whiskering just given).

µ

1T C

C
T

T3

T2

T

C

composes to

T

C

µT
T2

6

C

Monads

Anthony Voutas

For µX : T 2 (X) → T (X) we have components (µT )X = µT (X) : T 3 (X) → T 2 (X)

T2
µ

C

T3

T
1T C

C

T

composes to

C

T

Tµ

C

T2

For µX : T 2 (X) → T (X) we have components (T µ)X = T (µX ) : T 3 (X) → T 2 (X)

η

1T C

C

T3

1C

T

T

C

composes to

C

T

ηT

C

T2

For ηX : X → T (X) we have components (ηT )X = ηT (X) : T (X) → T 2 (X)

1C
η

C
T

T3

T
1T C

C

composes to

C

T

Tη

C

T2

For ηX : X → T (X) we have components (T η)X = T (ηX ) : T (X) → T 2 (X)

2.4

Signatures and Ω-Algebras

Here we use the presentation and notations of [12, Example 1.1.7].
At this point we ask an important question. Precisely what is an Algebra? The universal
algebraist will give an answer defining the concepts of theory and variety below.
One example of an algebra is found in group theory. A group consists of a set S, operations(◦, (−)−1 , e) — a binary operation ◦, an unary operation (−)−1 and a constant e (nullary operation) — and a set of equations which identify terms built from variables and these operations.
Informally (for now) a group is an algebra for the theory for groups, which is the set of operation
symbols and equations making up the group axioms.
To formalise this in general, recognise that the group theory is composed of the group operations and the group equations. First we will consider the operations without added equations.
Let Ω be a set of operation symbols (a different symbol for each operation you intend to havein your algebra - groups have three, rings have five, etc). Now let ar : Ω → N, be a function
which assigns to ω ∈ Ω the arity of the operation which corresponds to ω (that is, the number ofarguments the operation takes - often two or less, but this generalises to any natural number).
7

Monads

Anthony Voutas

A signature is comprised of Ω and ar together, and is often just referred to as Ω.
With a signature Ω, we can form Ω-algebras.
Definition 2.4.1. An Ω-algebra A is comprised of a ‘carrier’ for the algebra and an ‘interpretation’ for every operation symbol. The carrier of A is a set (often written |A|). The interpretationof ω ∈ Ω is a function aω : |A|ar(w) → |A|.
Note that the interpretation maps ar(ω)-tuples of elements of the carrier, back into the carrier, as you would expect of an operation.
As with groups, we can define the notion of a Ω-homomorphism from Ω-algebra A to Ω-algebra
B.
Definition 2.4.2. A Ω-homomorphism is a function f : |A| → |B| with the following property:f (aω (x1 , x2 , ..., xar(ω) )) = bω (f (x1 ), f (x2 ), ..., f (xar(ω) ))For all ar(ω)-tuples of xi ∈ |A|.
In other words the Ω-homomorphisms preserve the actions of the operations in the algebra.
Note that this coincides with the definition of group homomorphism in that if f : G → H isa group homomorphism, then f (x ◦G y) = f (x) ◦H f (y) (with the operation written in infix
notation here), f (x−1 ) = (f (x))−1 and f (eG ) = eH . In fact this general definition corresponds
to many standard definitions of homomorphisms (such as for rings, monoids, lattices, etc).
This property is compositional and satisfied for identities, and so we have a category of Ωalgebras and Ω-homomorphisms, called Ω-Alg.
In order to consider the addition of equations, it is necessary to define Ω-terms. An Ω-term
is either a variable, a constant, or an operation applied to the correct number of terms. An Ωequation is a pair of Ω-terms. In order for a Ω-algebra A to satisfy an Ω-equation, the two termsof the Ω-equation must evaluate (via the application of the A-interpretations of the operation
symbols) to the same carrier value under any consistent substitution of carrier values for thevariables in the terms.
The signature can be augmented with a set of Ω-equations and the algebras cut down to only
those that satisfy those equations. The addition of this set of equations gets us to a formal notionof variety which matches a great many intuitively algebraic constructions. Thus,
Definition 2.4.3. An algebraic theory is a pair (Ω, E) where Ω is a signature and E is a set ofΩ-equations.
Thus the algebras for a theory (Ω, E) are a full subcategory of the original Ω-Alg. This
subcategory (Ω, E)-Alg is called the variety, since it is a particular ‘variety of algebras’. In
universal algebra it is not necessary to acknowledge that a variety has arrows, it is usually taken
to simply be the set/class of objects (that is, the set of algebras for the theory).
Leaving aside these added equations is convenient for now. Without equations, an Ω-Algebra isessentially a carrier |A| and a single function:Xa:(|A|ar(ω) ) → |A|
(2)
ω∈Ω

8

Monads

Anthony Voutas

In which Σ is the disjoint union operator. The domain is the set of terms which consist of asingle operation applied to elements of |A| and the function evaluates those terms in |A|.

2.5

Functors and F -Algebras

Here we use the presentation and notations of [12, §2.2].
We will now consider an even more general definition of algebra, that of the algebra for a functor.
This definition will help us to work with algebras using convenient categorical insights.
Take an endofunctor F : C → C.
Definition 2.5.1. An algebra for F (an F -algebra) is a pair (X, h) where X is an object of C
and h : F (X) → X is an arrow of C.
Definition 2.5.2. An F -homomorphism between an F -algebra (A, a) and an F -algebra (B, b)
is a C arrow f : A → B such that the following diagram commutes:
F (A)F (f )

F (B)

a
A

b
f

B

We will now show that this definition captures the original set-theoretic one. Given a signatureΩ we can define a functor F : Set → Set (for sets X)
X
F (X) =X ar(ω)ω∈Ω

That is, F (X) is the domain of the evaluation function given in equation (2).
Now for arrows g : X → X 0 and operations ω interpreted in F (X) as ωX and in F (X 0 ) as
ωX 0 , we have F (g) : F (X) → F (X 0 )(F (g))(ωX (x1 , x2 , ..., xar(ω) )) = (ωX 0 (g(x1 ), g(x2 ), ..., g(xar(ω)) ))Then it is clear that F is a functor. Using the above definition, an F -algebra is a set X and afunctionXh
X ar(ω) → Xω∈ΩWhich is what we concluded an Ω-algebra was.
This definition captures the original notion, but is more general. As it turns out, F -algebras areΩ-algebras for set based, polynomial functors F [10, Chpt 10], that is functors F : Set → Set
such that:
F (X) =NX

cn X nn=0

F (f )(x1 , x2 , ..., xn ) = (f (x1 ), f (x2 ), ..., f (xn ))9Monads3

Anthony Voutas

Monads and adjunctions

Some of the notation and technicalities are taken from [10, Chpt 10], and a full treatment of thissubject can be found in [2, §VI].

3.1

What is a Monad?

In generalising the definition of algebra, we have lost some of the useful structure on F (X) namely the intuitive connection with terms. It seems that we may have generalised too far.
Fortunately, there is a way to reintroduce this intuition categorically.
Definition 3.1.1 (Monad). A Monad is a triple T = hT, µ, ηi such that T : C → C is an
endofunctor, µ and η are natural transformationsµ : T2 →˙ T,

η : 1C →˙ Tand the following are commutative diagrams
T3

Tµ

T2

ηT

T2

µ

µT
T2

1C T

µ

Tη

T 1C

µ

T

(3)

T

That is, µ ◦ T µ = µ ◦ µT and µ ◦ T η = 1T = µ ◦ ηT .
If the functor T is to be interpreted as an algebra type (as we will in section 4), then µ isa transformation which encodes how terms of terms are collapsed down to terms. The square
property above says that terms of terms of terms can be collapsed to terms unambiguously.
Furthermore, η is a transformation which encodes how single elements of the carrier are turned
into terms.
Example 3.1.2. Perhaps the simplest example of a monad is the monad for lists.
The monad T = hT, µ, ηi is defined on Set as follows. The functor T takes a set X to theset of finite lists of elements of the set X, and for functions f and lists [x1 , x2 , ..., xn ] ∈ T X:
T (f )([x1 , x2 , ..., xn ]) = [f (x1 ), f (x2 ), ..., f (xn )]2µX : T (X) → T (X) is a flattening in which:hi[x1,1 , x1,2 , ..., x1,n ], [x2,1 , x2,2 , ..., x2,n ], ..., [xm,1 , xm,2 , ..., xm,n ]hi
7→ x1,1 , x1,2 , ..., x1,n , x2,1 , x2,2 , ..., x2,n , ..., xm,1 , xm,2 , ..., xm,nand ηX : X → T (X) is an injection x1 7→ [x1 ]In this case the monad rules correspond to the claims that:
1. There is an unambiguous way of flattening a list of list of lists into a list.
2. Injecting a list into a singleton list of that list and flattening will return the first list.
3. Injecting each element of a list into a singleton list and flattening will return the first list.
These facts should be clear on reflection of a few examples, though a general proof is tedious.

10

Monads

3.2

Anthony Voutas

Adjunctions give rise to Monads

Theorem 3.2.1. [Adjunctions to Monads] Given an Adjunction (F, G, η, ) with F a G, we canalways construct a monad in the category C = dom(F ) as follows.
T : C → C = GF : C → C
η : 1C →˙ T = η : 1C →˙ GF
µ : T2 →˙ T = GF : GF GF →˙ GF
Proof. Making the above substitutions, it remains to show the following diagrams commute:GF GF GF

GF GF

1C GF

GF GF

GF GF

ηGF

GF η
GF GF

GF

GF GF

GF

GF

GF

GF 1C

GF

The commutativity of square diagram can be shown by examining the following diagrams
F GF G

F G



F G
FG

FG



F GF G(X)F G(f )F GX

1C

F G(X)F G(X)
X

f

(4)

X

If the diagram on the left commutes, then it commutes for all C objects, including all F (X), andits commutativity is preserved by applying the functor G to all objects and arrows. Thus if it
commutes, the original square diagram above commutes.
The diagram on the right of (4) commutes by the fact that  is a natural transformation. It isclear that the components of the diagram on the left are actually special cases of the one on theright where f = X
It remains to show that the triangles GF ◦ GF η = 1GF = GF ◦ ηGF commute. As it turns
out, these are specific cases of the triangle identities for an adjunction (definition 2.2.1). First
take the identity F ◦ F η = 1F under the action of G, then take the identity G ◦ ηG = 1G for
all objects F (X).
Example 3.2.2. We will now show the free-forgetful adjunction for monoids giving rise to themonad for lists seen in example 3.1.2. First we must define this adjunction.
The free functor F : Set → Mon is defined as follows. For sets X, F (X) is the monoid of
strings of elements of X. The monoid multiplication is concatenation and the unit is the empty
string. Elements of F (X) will be represented [x1 , ..., xn ].
For functions f , the functor F acts as follows
F f ([x1 , ..., xn ]) = [f (x1 ), ..., f (xn )]11

Monads

Anthony Voutas

The forgetful functor U : Mon → Set is defined as follows. For monoids M , U M is the underlying set of M , and for monoid homomorphisms h : M → N , U h : U M → U N is just the function h.
The natural transformation η : 1Set →˙ U F is defined by the components ηX (x) = [x], whilethe  : F U →˙ 1Mon is defined by components M ([m1 , ..., mn ]) = m1 ◦M ... ◦M mn .
We will take for granted that this is an adjunction. Then the monad generated is hU F, η, U F i.
U F sends a set X to the set of lists of elements of X, the components ηX inject elements of X
into singleton lists, and the components U FX : U F U F (X) → U F (X) flatten lists of lists tolists. This is the monad from example 3.1.2.

3.3

Algebras for a Monad

Theorem 3.2.1 begs the question: given a monad, can one split it into two adjoint functors?
The answer is yes. In general there are many splittings for a monad. There are two important
splitting constructions: The Eilenberg-Moore construction [13], and the Kleisli construction [14].
In fact, it so happens that the collection of splittings for a monad form a category in which the
Eilenberg-Moore adjunction is terminal and the Kleisli adjunction is initial. The proof of this isbeyond the scope of this report, but can be found in [2, §VI]. What will be proved is that theEilenberg-Moore construction yields a splitting of any monad.
We must first define the Eilenberg-Moore category C T of a monad T = hT, µ, ηi. This category consists of T-algebras and T-morphisms (this is an extension of the concept of an F -algebra
for an endofunctor F ).
Definition 3.3.1. The Eilenberg-Moore category C T consists of:
Objects of C T (the T-algebras) will be the T -algebras (A, a) (see definition 2.5.1) such thata ◦ T a = a ◦ µA

a ◦ ηA = 1A

andThat is, the following diagrams commute:
T 2A

Ta

µA
TA

a

TA

A

ηA

TA

a

a

A

A

(5)

Informally, one can consider T A as an object of terms over values in A, and a as an evaluation
which picks out a value in A for each term in T A. Then the square above corresponds to thenotion that evaluating a term of terms by applying two evaluations is equivalent to collapsing theterm of terms into an term and then evaluating it. The triangle corresponds to the notion thatsingleton terms evaluate to the value the term is built from. That is, a T-algebra is a T -algebra
for which µ acts as a term flattener and η acts as an injection into a singleton term.
Definition 3.3.2. The morphisms of T-algebras f : (A, a) → (B, b) are arrows f : A → B such

12Monads

Anthony Voutas

that f ◦ a = b ◦ T (f ), that is:
T (f )

T (A)

T (B)

a

b

A

f

B

That is, the normal notion of T -homomorphisms. This makes C T a full subcategory of thecategory of T -Algebras.
Example 3.3.3. Formally, algebras for the list monad hT, η, µi (from example 3.1.2) are pairs(A, a : T A → A), such that the diagrams (5) are satisfied.
The informal discussion above can be instantiated precisely in this situation, in that the term
set T A is the set of lists of elements of A, and the evaluation a is a function which picks out avalue from A for any given list. The properties which this function must obey from (5) are:
1. Singleton lists must be evaluated as the value they contain.
2. The evaluation a is associative, in that we can evaluate a list by parts, forming a new list
which when evaluated yields the same value in A as if evaluating the list as a whole.
These are essentially the requirements of a monoid, as such an evaluation can be entirely captured by the evaluations on lists of length two. The evaluation of longer lists can be recoveredfrom repeated application of this binary evaluation. The evaluation is fixed on singletons. The
empty list must evaluate to an identity for the binary evaluation, because every list can be taken
to be the concatenation of itself with the empty list, and it is given that the evaluation of theparts matches the evaluation of the whole.
So, the collection of algebras for the list monad are the collection of all monoids.

3.4

Monads give rise to Adjunctions

Theorem 3.4.1. Given a monad T = hT, µ, ηi on C we can construct an adjunction between C
and C T .
The adjunction will be defined by functors U (forgetful)
U : CT → C
U (A, a) = A
U (f : (A, a) → (B, b)) = f : A → B
and F (free)
F : C → CT
F (A) = (T A, µA )F (f : A → B) = T (f ) : (T A, µA ) → (T B, µB )13

Monads

Anthony Voutas

Proof. U is clearly a functor, so we will first show that F is a functor, and then show that F a U .
Firstly, we should check that (T A, µA ) is a T-algebra, by examining the following diagrams:
T 2 (T A)

T (µA )

T (T A)µA

ηT A

T (T A)

µA

µA

(T A)

(T A)

µT A
T (T A)(T A)

These are cases of:
T3

Tµ

ηT

T2

T

T2

µ

µT
T2

µ

T

µ

T

Which are clearly commutative because T = hT, µ, ηi is a monad.
Now we check that T (f ) is a T-morphism by examining this diagram:2

T 2 (f )T (A)T 2 (B)

µA

µB

T (A)

T (f )T (B)This clearly commutes for any f because µ is a natural transformation, and this is exactly thenatural transformation diagram for µ.
So, we now know that F and U are functors it now remains to show that they are adjoint(specifically, F a U ).
Notice that T = U F .
U F (A) = U (T A, µA )= TA
U F (f : A → B) = U (T f : (T A, µA ) → (T B, µB ))= Tf : TA → TB
We will show F a U by the triangle identities for adjunctions. First we need to define both theunit η : 1C → U F and the counit  : F U → 1C T . The notation suggests that the unit η : 1C → U F
can be taken to be the η : 1C → T of the monad, and this matches the required form.

14

Monads

Anthony Voutas

To establish the counit  : F U → 1C T , we examine the action of the functor F U : C T → C T .
F U (A, a) = F (A)= (T A, µA )F U (f : (A, a) → (B, b)) = F (f : A → B)
= T f : (T A, µA ) → (T B, µB )Let the components of the counit be (A,a) = a as a T-morphism from (T A, µA ) to (A, a):T 2 (A)

T (a)

T (A)

µA

a

T (A)

a

A

To be a T-morphism, the above diagram must commute, which it does because (A, a) is a Talgebra. For  to be natural, we must show that f ◦(A,a) = (B,b) ◦T (f ) for all f : (A, a) → (B, b).
Since f is a T-morphism, f ◦ a = b ◦ T (f ), which is precisely the property we want.
Now, the triangle identities for the adjunction can be seen as follows:1

G(A, a)G(A, a)ηG(A,a)1A

becomesηA

G(A,a)a1

FA

becomesF (A)

F ηA

(6)

TA

GF G(A, a)
FA

A

1

TA

TA
µA

T ηA

(7)

T 2A

F GF A(6) commutes because (A, a) is a T-algebra (see triangle diagram in (5)), and (7) commutes
because T is a monad (see η diagram in (3)).
Example 3.4.2. We will now show the adjunction which arises from the list monad.
If the monad is T = hT, η, µi on Set, then the Eilenberg-Moore adjunction is given by thefunctors U (forgetful)
U : SetT → Set
U (A, a) = A
U (f : (A, a) → (B, b)) = f : A → B
and F (free)
F : Set → SetT
F (A) = (T A, µA )F (f : A → B) = T (f ) : (T A, µA ) → (T B, µB )15

Monads

Anthony Voutas

It can be seen from the previous examples that SetT is isomorphic to Mon, and the forgetful andfree functors are isomorphic to those given by the original free-forgetful adjunction for monoids
as follows, U (forgetful):
U : Mon → Set
U (M ) = |M |U (h : M → N ) = h : |M | → |N |and F (free)
F : Set → Mon
F (A) = (T A, µA )F (f )([x1 , ..., xn ]) = T (f )([x1 , ..., xn ])= [f (x1 ), ..., f (xn )]In the next section we will see that this fact generalises to all algebraic varieties.

16

Monads

4

Anthony Voutas

Monads and universal algebra

In this section we will show for any theory (signature with equations), the traditional categoryof algebras (the variety) is isomorphic to the Eilenberg-Moore category for the monad arisingfrom the free construction corresponding to that variety.

4.1

Comparison functor

Suppose we have an adjunction between categories X and A, then we construct the monad T
in X from that adjunction, then construct the category X T . We have already said that there ismore than one construction of an adjunction from a monad. So it is not always the case thatA∼
= X T . However, there is a relationship in general, which is given by the following theorem:
Theorem 4.1.1 (Comparison functor to the Eilenberg-Moore category). Let
hF : X → A, G : A → X , η : 1X →˙ GF,  : F G →˙ 1A ibe an adjunction and let T = hGF, η, GF i be the monad it defines in X . Then there is a uniquefunctor K : A → X T such that GT K = G and KF = F T . That is, the following diagrams
commute for unique K:
F

X
FT

A

G

X

K

A
K

GT

XT

XT

Note that hF T , GT , η T , T i is the Eilenberg-Moore adjunction between X and X T .
Proof. Define the comparison functor K : A → X T in the following way, for objects a and arrows
f of A.
KA = hGA, GA i(8)

Kf = Gf : hGA, GA i → hGA0 , GA0 i(9)We will now prove that K is a functor. First we will show that hGA, GA i is a T-algebra as (8)claims.
Consider the proposed structure map GA : GF GA → GA, and the proposed carrier GA. The
first of the T-algebra properties is then (from (5))
GF GF GAGF GA

GFGA
GF GA

GF GA
GA

GA

GA

Which is the definition of G by definition 2.1.1 (recall that the square commutes in general).

17

Monads

Anthony Voutas

The second T-algebra property is
GA

ηGA

GF GA
GA
GA

Which happens to be one of the triangle identities from definition 2.2.1. So, K maps objects of
A to objects of X T .
Now we must show that Kf = Gf is a T-morphism as per (9). It’s certainly a X arrow, so
we need the following diagram to commute:
GF Gf
GF GA
GA

GF GA0
GA0

GA

Gf

GA0

This is G applied to the natural transformation square for , and thus, it commutes. So, fromthe above, and the fact that G is a functor we get that K is a functor in the following way:K(f ◦ g) = G(f ◦ g) = G(f ) ◦ G(g) = K(f ) ◦ K(g)
K(1A ) = G(1A ) = 1GA = 1KA
The last step above being because the identity on KA = hGA, GA i is the identity on GA.
Now, given this definition of K, it should be apparent that
KF = F T ,GT K = G

The left because GF = T and F T f = T f , and the right because GT just forgets that Kf is a
T-morphism. It has been shown that a comparison functor K exists and satisfies the required
equations, and so it remains to show that this functor is unique to prove the above theorem.
The property GT K = G requires that Gf = GT Kf = Kf . A functor can be fully determined by its action on arrows, and so K is fully determined by this property, and is thus unique.

4.2

Beck’s Theorem

Now that we have the comparison functor, we can examine when it is an isomorphism. This
will later allow us to prove that the comparison functor is an isomorphism for the free-forgetfuladjunction of a variety. Beck’s theorem provides a suitable method of discerning whether thecomparison functor is an isomorphism.
In order to state Beck’s theorem, we must define the notions of split coequaliser and absolutecoequaliser [2].
18Monads

Anthony Voutas

Definition 4.2.1. An arrow e is called an absolute coequaliser of δ0 and δ1 in C if for any functor
T : C → X the resulting fork
T δ0

Te

T a ⇒ T b −−→ T c
T δ1

makes T e the coequaliser of T δ1 and T δ0 .
Note that taking T above to be the identity functor, one can observe that all absolute coequalisers are coequalisers.
Definition 4.2.2. An arrow e is called a split coequaliser of δ0 and δ1 in C if the following is a
split forkδ0ea ⇒ b−→cδ1

That is, s : c → b an t : b → a exist, such thate ◦ δ0 = e ◦ δ1 ,e ◦ s = 1,

δ0 ◦ t = 1,

δ1 ◦ t = s ◦ eThat is, the following diagrams commute:
a

δ0

c

b

δ1

s

b

e
b

e

c

b

t

a

b
δ0

e
c

b

t

a
δ1

e
c

s

(10)

b

Since the definition of split coequaliser is given equationally, (and not in terms of uniquearrows) application of a functor will again yield a split coequaliser. Thus, all split coequalisers
are absolute coequalisers, and are thus coequalisers.
Before we get to Beck’s Theorem, we must also define what it means for a functor to create
coequalisers. The general definition for creating (co)limits can be found at the end of [2, §V.1],
but here it is simpler to give the specific definition for coequalisers.
Definition 4.2.3. A functor G : A → X creates coequalisers if to every coequaliser fork in X
there is exactly one fork in A which maps to that coequaliser fork under G, and that fork is acoequaliser fork in A.
Theorem 4.2.4 (Beck’s Theorem). Let
hF : X → A, G : A → X , η : 1X →˙ GF,  : F G →˙ 1A ibe an adjunction, hT, µ, ηi be the monad it defines in X , X T be the Eilenberg-Moore category ofT-algebras, andhF T : X → X T , GT : X T → X , η : 1X →˙ GT F T ,  : F T GT →˙ 1TX ibe the corresponding adjunction. Then the following are equivalent:
1. The comparison functor K : A → X T is an isomorphism.
2. The functor G : A → X creates coequalizers for those parallel pairs f, g in A for which
Gf, Gg has an absolute coequalizer in X .
3. The functor G : A → X creates coequalizers for those parallel pairs f, g in A for which
Gf, Gg has a split coequalizer in X .

19Monads

Anthony Voutas

Proof. We will show that 1 implies 2, that 2 implies 3 and that 3 implies 1.
That 2 implies 3 is clear because all split coequalisers are absolute coequalisers.
That 1 implies 2 will now be shown. So, given a unique comparison functor, we need to consider
the parallel pairs of arrows in A which correspond via G to parallel pairs of arrows with anabsolute coequaliser in X . Then for those particular parallel pairs of arrows in A we must showthat the functor G creates coequalisers for them. For such absolute coequalisers the image underF T is a coequaliser in X T .
d0hx, hihy, kid1

of T-algebras for which the corresponding arrows in X have an absolute coequaliser.
d0
y

x

e

z

d1
To create a coequaliser for this parallel pair we must first find a unique T-algebra structurem : T z → z on z such that e becomes a map of T-algebras

4.3

Free constructions for varieties

The fact that varieties admit free constructions is a standard result in universal algebra and category theory. Despite this, I have been unable to locate a proof which is even vaguely satisfactory.
The two best I found were [15, Theorem 8.3.3], which didn’t include equations and didn’t provethat there was an adjunction, and a single sentence in [2, §V.6] claiming that the result is aneasy generalisation of the case for groups which is given in that section.
Theorem 4.3.1. Given a variety (Ω, E)-Alg, we can construct an adjunction (the free-forgetfuladjunction to be precise) between the categories Set and (Ω, E)-Alg.
Instead of proving this, I will give some intuitive sense of what the free and forgetful functors
should be. Firstly, the forgetful functor is fairly clear. On algebras it returns the carrier set andon morphisms it returns the underlying function, and this is clearly a functor because composition and identities are the same.
The free functor acts on sets X and takes them to algebras in which the carrier set is theset of ground terms of the theory taking constants from X (and obviously the nullary operationsin the theory). The operations are given the obvious interpretation, which is that applying themtakes a list of terms to a new term which is just the old terms encased with the operation symbol
being interpreted. Since there are equations, the actual terms of the algebra need to be theequivalence classes under the quotient by the theory’s equations, but this doesn’t really affect
how the operations work.
The free functor also acts on functions f : X → X 0 in that it distributes their effect over
all the operation symbols in the theory so that they are directly applied to the constants x ∈ X
and only those constants. These form acceptable homomorphisms because the equations of thetheory must remain satisfied when functions are applied in this way.
20

Monads

4.4

Anthony Voutas

Universal algebra

We will now show that the forgetful functor U above creates coequalisers for those parallelpairs f, g in (Ω, E)-Alg for which Gf ,Gg has an absolute/split coequaliser in Set. Thus, by
Beck’s Theorem, we will have shown that the comparison functor K : (Ω, E)-Alg → SetT is an
isomorphism.
Theorem 4.4.1. The comparison functor K : (Ω, E)-Alg → SetT is an isomorphism.
Proof. Consider an arbitrary parallel pair of arrows f, g : A ⇒ B in X T for which the underlying
functions have an absolute coequaliser e:
Gf
GA

e

GB

X

Gg
We will prove that G : (Ω, E)-Alg → Set creates coequalisers for these pairs. To do so, we mustshow that e lifts to a unique morphism of algebras and then that this map is a coequaliser of f
and g.
Thus, consider an arbitrary n-ary operator ω ∈ Ω. We can construct the following diagram:
fn
A

n

g

n

Bn

ωA

en

Xn

ωB

ωX

(11)

f
A

g

B

X

e

f and g are (Ω, E)-morphisms, so the left squares commute. The function e is an absolutecoequaliser in Set and therefore its n-th power is also a coequaliser (of f n and g n ). So sincee ◦ ωB ◦ f n = e ◦ f ◦ ωA = e ◦ g ◦ ωA = e ◦ ωB ◦ g n
the universal property of en will force e ◦ ωB to factor uniquely through the coequaliser viae ◦ ωB = ωX ◦ en . This unique factorisation uniquely defines all the operation ωX on X so thatthe square on the right of (11) commutes for all ω ∈ Ω.
It must now be shown that e is a coequaliser of f and g as (Ω, E)-morphisms. So, consider
another morphism h such that h ◦ f = h ◦ g. Then h ◦ f = h ◦ g in Set (by applying the forgetful
functor G), so in Set h = h0 e for unique function h0 . So we must show that
Xn

h0n

Cn

ωX

ωC
X

h0

C

commutes for every operation ω. Now, h is a morphism of algebras, so
h0 ◦ ωX ◦ en = h0 ◦ e ◦ ωB = h ◦ ωB = ωC ◦ hn = ωC ◦ h0n ◦ enand since en is a coequaliser, en is epi, so h0 ◦ ωX = ωC ◦ h0n , as required by (12).

21

(12)

Monads

5

Anthony Voutas

Comonads

The comonad is the dual concept of a monad. A formal definition is easily obtained by considering monads in C op . All the results pertaining to monads, including those above can be
dualised to the comonad case. Thus, this section will not be concerned as much with the theoryof comonads, but rather with examples of their applications.
Importantly the concept of algebra dualises to that of a coalgebra, for which there are both
functor and comonad versions. Coalgebra is useful for reasoning about state transition systems [6] and modal logic [7]. For algebra, equations were key, but for coalgebra, they must
be replaced with behaviours [16] or bisimulations [17]. While monads are useful for constructively defined (algebraic) data types, comonads can provide a formal model for unbounded datatypes [17].

5.1State transition systems

Where algebraic induction has a notion of recursive construction, coalgebraic coinduction has anotion of recursive observation. There is a conceptual connection between this kind of observation
and any kind of state transistion system. As such, we expect, and do find that coalgebra provides
a general and neat language to describe all manner of state transition systems. [6]5.2

Modal Logic

Modal logic is a large field unto itself, and coalgebraic methods have only been explored relatively
recently. Coalgebraic methods allow generic tools to be created, both for showing soundness andcompleteness results [7] and for generating automated theorem provers [18].

5.3

Behaviours and Bisimulations

Bisimulation is a concept which stems from concurrency. One wants to be able to formally specify
certain aspects of the behaviour of concurrent systems. Coalgebra shows promise of being able
to provide formalisms for providing enough freedom to concurrent systems to maintain the useof multicore and multiprocessor systems, while providing enough boundaries to ensure program
correctness. [17]5.4

Unbounded data types

Unbounded data types might initially seem like an odd thing to desire. The truth is that in any
real-time system, modelling data as a stream of input is much more natural than modelling itwith finite data structures. Coalgebra allows the formal specification of infinite data types withcoinduction [6].

22Monads

Anthony Voutas

References[1] Barr M. & Wells C. Toposes, Triples and Theories. A Series of Comprehensive Studies inMathematics. Springer, New York, first edition, 1985.
[2] Mac Lane S. Categories for the working mathematician. Graduate Texts in Mathematics.
Springer, New York, second edition, 1978.
[3] Hughes J. Generalising monads to arrows. Science of Computer Programming, 37:66–111,
2000.
[4] HaskellWiki. Applications of monads in Haskell. http://www.haskell.org/haskellwiki/
Research_papers/Monads_and_arrows. Website accessed: 1 June 2012.
[5] Marlow S. & Newton R. & Peyton-Jones S. A monad for deterministic parallelism. In
Proceedings of the 4th ACM symposium on Haskell, Haskell ’11, pages 71–82, New York,NY, USA, 2011. ACM.
[6] Jacobs B. & Rutten J. A tutorial on (co)algebras and (co)induction. European Association
for Theoretical Computer Science, 62:222–259, 1997.
[7] Pattinson D. Coalgebraic modal logic: soundness, completeness and decidability of local
consequence. Theoretical Computer Science, 309(1-3):177 – 193, 2003.
[8] Lawvere F. W. Functorial Semantics of Algebraic Theories. PhD thesis, Columbia University, 1963. (Available with commentary as TAC Reprint 5).
[9] Hyland M. & Power J. The category theoretic understanding of universal algebra: Lawvere
theories and monads. Electronic Notes in Theoretical Computer Science, 172:437–458, 2007.
[10] Awodey S. Category Theory. Oxford Logic Guides. Oxford Press, Oxford, second edition,
2010.
[11] Willerton S. String diagrams 2. http://www.youtube.com/watch?v=JeGhNhgOTuk#t=133,
2007. YouTube video.
[12] Pierce B.C. Basic Category Theory for Computer Scientists. Foundations of Computing.
MIT Press, Cambridge, Massachusetts, first edition, 1991.
[13] Eilenberg S. & Moore J.C. Adjoint functors and triples. Illinois J. Math., 9(3):381–398,
1965.
[14] Kliesli H. Every standard construction is induced by a pair of adjoint functors. In Proceedingsof the American Mathematical Society, volume 16, pages 544–546, June 1965.
[15] Bergman G.M. An Invitation to General Algebra and Universal Constructions. Henry
Helson, 15 the Crescent, Berkeley CA, second edition, 1998. An earlier edition appeared as
Berkeley Mathematics Lecture Notes 7.
[16] Gumm H.P. Elements of the general theory of coalgebras. Preprint, 1999.
[17] Rutten J. Universal coalgebra: a theory of systems. Theoretical Computer Science, 249:3–80,
2000.

23

Monads

Anthony Voutas[18] Gore R & Kupke C & Pattinson D. Optimal tableau algorithms for coalgebraic logics. In
Javier Esparza and Rupak Majumdar, editors, Tools and Algorithms for the Construction
and Analysis of Systems, volume 6015 of Lecture Notes in Computer Science, pages 114–128.
Springer Berlin / Heidelberg, 2010.

24