Monads

(under construction)

Part 4 of a short course on monads.

We spent one lecture on the Eilenberg-Moore definition of monads. In a second lecture, we will look at the Kleisli definition.

For self study, I augmented the lecture notes with some videos. First, I made a video summarizing the previous lectures, retaining only the minimum needed to motiviate the mathematical definition of a monad. After that, one should study the definition of a monad and show that List is a monad. ^[1] Try yourself, but I also made a video.

(Programs: I should add some new ones …)

Example

Going back to the three notations for monoids we notice the following. In Notation 3, the operations and equations change with each signature. In Notation 1 a 2, the operations and equations are independent of any reference to monoids.

This opens up the possibility of treating all algebraic theories in a common abstract framework and has been equally important for mathematics and software engineering.'

Axioms

This section assumes that the reader remembers the section on the free monoid and/or its Haskell implementation monoid.hs.

Definition: A monad

$(M,\eta ,\mu )$ is a functor

$M:\mathcal{C}\to \mathcal{C}$ with two natural transformation

$\eta :Id\to M$ and

$\mu :MM\to M$ such that

Exercise: Instantiate the definition with the list/free monoid monad. In other words, verify that in (List, eta, mu) as defined in monoids is a monad.

Answer. ^[2]

Remark: The definition of a monad can be equivalently formulated by saying that a monad is a monoid in the category of endofunctors. To make this precise, we need to explain what a monoid in a monoidal category is. This is a bit of a detour, so I'll skip it for now. But if you squeeze your eyes, you will be able to see the two triangles as the left and right identity laws of a monoid and the square as the associativity law.

I advertised the notion of monad as an axiomatisation of the idea of algebraic structure. So far, we defined a monad

$(M,\eta ,\mu )$. We checked that the defining equations for

$\eta$ and

$\mu$ are satisfied in our leading example where

$MX$ is the free monoid over

$X$. In other words,

$MX$ is the set of all terms one can form from the signature of monoids and "variables" in

$X$, with equality between terms given by the monoid equations.

Optional maths exercise: Show that our observation above on monoids generalises to all algebras specified by operations and equations. To get started, define

$TX$ as the set of all terms generated by the operations and elements of

$X$, with equality between terms given by the equations. This refers back to the definition of termalgebra. To continue, define

${\eta }_X:X\to TX$ as "insertion of variables". In other words,

$\eta (x)$ just says that every element of

$X$ (every variable) is also a term. To define

${\mu }_X:TTX\to TX$, we use the recursion principle/universal property of the termalgebra and define

${\mu }_X=i{d}_{TX}^{\mathrm{♯}}$. Now, it remains to verify that this

$(T,\eta ,\mu )$ satisfies the equations of a monad.

Definition: A monad in Kleisli form

$(M,\eta ,(-{)}^{\mathrm{♯}})$ …

Exercise: Let

$\mathrm{\Sigma }$ be a signature. For which

$\eta$ and

$(-{)}^{\mathrm{♯}}$ is

$MX={\mathsf{T}\mathsf{e}\mathsf{r}\mathsf{m}}_{\mathrm{\Sigma },X}$ a monad?

Exercise: (For Haskell programmers). Explain in which sense a monad in Kleisli form and a monad in Haskell are the same concept.

More Examples

We can use this opportunity to illustrate that category theory is an abstrac theory of structure by instantiating the notion of a monad in different "base" categories.

Monads in

$Set$

In sets, a monad can be identified with class of algebras defined by operations and equations. ^[3]

It is quite interesting that many important functors on

$Set$ happen to carry a natural monad structure: We have seen

$X^{\ast }=\mathsf{L}\mathsf{i}\mathsf{s}\mathsf{t}(X)$ as our paradigmatic example.

Which structure turns

$X\mapsto \{\mathrm{\perp }\}+X$ into a monad?

We have seen previously that the operation

$\mathcal{P}$ mapping a set

$X$ to its powerset is a functor. Can you show that it is also monad?

This idea also extends to probability distributions (Giry monad).

But in general, to carry the structure of a monad is quite a special property for a functor. For example, functors do always compose, but monads do not. ^[4]

Monads in Haskell

Is Haskell a category? There is some debate on this. My take is that full Haskell is clearly not a category (as demonstrated in the blog linked above), but that there are various fragments of Haskell that come close enough. In any case, when implementing category theory in Haskell we need to keep an eye on possible mismatches. For example, Haskell is clearly not the category

$Set$. Nevertheless, many concepts and results transfer from the category

$Set$ to Haskell.

For example

$\mathsf{L}\mathsf{i}\mathsf{s}\mathsf{t}(X)=X^{\ast }$ is a functor on

$Set$ and List a is a functor in Haskell.

$\mathsf{L}\mathsf{i}\mathsf{s}\mathsf{t}(X)$ is also a monad in

$Set$ and List a is a monad in Haskell. Moreover, they are functors/monads in

$Set$ for the same reason they are functors/monads in Haskell. Similar statements are true for other functors/monads.

Conversely, many monads known in Haskell such as the error monad or the state monad also correspond to monads in

$Set$. But some Haskell monads such as Input/Output do not have an analogue in

$Set$. ^[5]

Monads on

$Ord$

Monads in

$Set$ are the most important example for us. But the reason why monads are important to category theorists and mathematics in the large is that the notion of a monad makes sense in any category. ^[6] The point of this example is to show just one case of this: In ordered sets, a monad is a class of ordered algebras defined by monotone operations and inequations. ^[7]

Monads in

$Rel$

Let

$Rel$ be the category of sets with relations as arrows. If we want relations to play the role of functors, we need to say what natural transformations should be. We simply choose the subset-relation. What, then, is a monad in

$Rel$?

• First, we have an arrow (hence relation)
  $M:A\to A$.
• Second, we have
  $Id\subseteq M$.
• Third, we have
  $M;M\subseteq M$.

Exercise: Show that such a relation

$M$ is reflexive and transitive. Conversely, every reflexive and transitive relation is a monad in

$Rel$.

Theory

There is a lot to choose from. We could prove the claims about the examples above. We could prove that the Eilenberg-Moore and the Kleisli definitions are equivalent. Maybe a sketch of this would be helpful. And explain why monads in mathematics and monads in programming look quite different.

… too many diagrams for markdown latex but I will draw them by hand in the lecture … trying to tie everything we learned together …

Algebras for a Functor

Definition: Let

$F:\mathcal{C}\to \mathcal{C}$ be a functor. An arrow

$FA\to A$ is called an

$F$-algebra.

$f:A\to B$ is an

$F$-algebra morphism if

…

The category of

$F$-algebras is denoted by

$\mathsf{A}\mathsf{l}\mathsf{g}(F)$.

Example: Let

$FX=1+A\times X$. The initial

$F$-algebra is

$List(A)=A^{\ast }$.

Example: Every

$\mathrm{\Sigma }$-algebra is also and

$F$ algebra. The details are as follows. Let

$\mathcal{C}=Set$ and

$\mathrm{\Sigma }$ be a signature. Define

$FX=\sum _{\sigma \in \mathrm{\Sigma }}{X}^{\mathsf{a}\mathsf{r}\mathsf{i}\mathsf{t}\mathsf{y}(\sigma )}$. Then

$\mathsf{A}\mathsf{l}\mathsf{g}(\mathrm{\Sigma })=\mathsf{A}\mathsf{l}\mathsf{g}(F)$.

Algebras for a Monad

Definition:

$\alpha :MA\to A$ is an algebra for the monad

$(M,\eta ,\mu )$ if the following diagrams commute

…

I denote category of Eilenberg-Moore algebars for the monad

$M$ by

$\mathsf{M}\mathsf{A}\mathsf{l}\mathsf{g}(M)$.

Example: We have seen that lists, errors and a certain kind of binary trees are monads. It may be a good exercise to write down the respective

$(M,\eta ,\mu )$ in mathematical notation.

The Kleisli Category of a Monad

Definition: Kleisli category …

Theorem: (Lawvere 1963, Linton 1969) Let

$\mathrm{\Sigma }$ be a signature and let

$\mathsf{A}\mathsf{l}\mathsf{g}(\mathrm{\Sigma },E)$ be category of

$\mathrm{\Sigma }$-algebras satisfying

$E$.

$\mathsf{A}\mathsf{l}\mathsf{g}(\mathrm{\Sigma },E)\cong \mathsf{M}\mathsf{A}\mathsf{l}\mathsf{g}(M)$. Conversely let

$M:\mathsf{S}\mathsf{e}\mathsf{t}\to \mathsf{S}\mathsf{e}\mathsf{t}$ be a monad. Then there is a signature ^[8] and equations such that

$\mathsf{M}\mathsf{A}\mathsf{l}\mathsf{g}(M)\cong \mathsf{A}\mathsf{l}\mathsf{g}(\mathrm{\Sigma },E)$.

The Free Monad over a Functor

The previous theorem suggests that algebras for a monad are more general than algebras for a functor. Intuitively, while the functor encodes a signature (=operations), a monad also allows us take into account equations. Given a functor

$F$, this raises the question for which monad

$M$ we have

$$\mathsf{A}\mathsf{l}\mathsf{g}(F)\cong \mathsf{M}\mathsf{A}\mathsf{l}\mathsf{g}(M).$$

The answer is that the equation holds if

$M$ is the free monad over

$F$. I don't want to define the notion of free monad here. Suffice it to say that, if

$M$ is the free monad over

$F$, then the equation above holds by definition. So just take "free monad over

$F$" as a name for the monad that makes

$\mathsf{A}\mathsf{l}\mathsf{g}(F)\cong \mathsf{M}\mathsf{A}\mathsf{l}\mathsf{g}(M)$ true.

In fact, in Haskell we can describe the free monad over a functor in more familiar terms. Let us first assume that we have defined

data functor x = ...

Then the free monad over functor is

data free_monad a = Var a | Node (functor (free_monad a)) 

In fact, we have already seen an example in the file magma.

The Comparison Theorem

Theorem: The embedding of

$\mathsf{K}\mathsf{l}(M)\to \mathsf{E}\mathsf{M}\mathsf{A}\mathsf{l}\mathsf{g}(M)$ …

Applications

We have seen that monads unify such different areas as universal algebra and effects in programming languages. While monads provide an important perspective, these areas can be studied without monads. The reason is that monads provide a common abstraction (a typeclass in Haskell), but as long as one is interested only in one particular instance, the more abstract perspective can always be "compiled away".

Thus, mondads are more likely to show their true power in situations where one wants to study several (or all) instances simultaneously.

One example is the study of the category of general effects in programming languages. From a theoretical point of view, monads allow us to define a category of effects and study it. From a software engineering perspective, monads provide a common interface for a wide range of different applications with all the common benefits such as code reuse, maintainability, etc.

Many examples in both mathematics and theoretical computer science arise from the study of algebras over different base categories. Monads over the category

$Set$ account for algebras in the ordinary sense we reviewed in the first lecture. Now imagine, whether for mathematics or programming, you want something like ordinary algebras but with additional features. One way to try to get this, is to use monads over a different base category.

In fact, some of the examples above are of this nature. I mention a few more.

• In algebraic topology one wants to compute so-called homology groups in order to classify different spaces according to the holes they have (make the donut/cup example). This requires counting how often one goes around a loop and thus requires some kind of group structure. So we end up with monads on categories enriched over abelian groups.

• In programming languages, we may be interested in replacing

  $Set$ by categories that allow us to accommodate features such as recursion, types, computability, etc.

In fact, these two applications are typical. Monads were invented for applications to homology and then later introduced to computer science for their use in denotational semantics of programming languages.

Outlook

What would come next?

If this was a

• category theory course we would do limits, colimits, adjoints, completion of categories.

• semantics of programming languages course, we would do typed lambda calculus, cartesian closed categories, PCF, domain theory.

• a mathematics course we would do abelian categories, 2-categories, enriched categories, higher categories.

• type theory course, we would do dependent types and some theorem proving in a language such as Lean, Idris, Agda, Coq, Isabelle.

• foundations of mathematics/categorical logic course, we would build up from equational logic to higher-order intuitionistic predicate calculus through a sequence of richer and richer categories, from Lawvere theories, essentially algebraic theories, geometric theories to toposes.

---

1. The definition of List is available in Haskell in any of the two files monoids and monoidshs. ↩︎

2. I made a video on why List is a monad. The main insight is condensed in the following picture (I write

   $M$ instead of
   $\mathsf{L}\mathsf{i}\mathsf{s}\mathsf{t}$ for typesetting reasons):

   

   Just think of

   $\mu$ as removing the second level of square brackets. ↩︎

3. This is a theorem due to Lawvere and then Linton. See below for more details. ↩︎

4. It is actually an interesting exercise to start out with two monads

   $(M,\eta ,\mu )$ and
   $(M^{\prime },{\eta }^{\prime },{\mu }^{\prime })$ and then to try to define a monad on the composition
   $M{M}^{\prime }$. Where do you get stuck? What extra structure is needed to make it work? There is a famous answer to this question … let me know if you are interested in this … ↩︎

5. The deeper point here is that monads abstract the structure that allows us to deal with "effects". This applies to all programming languages, it is just that haskellers found this perspective more useful than others. (It could be interesting to discuss: Why?) ↩︎

6. Actually, to be more precise, we need something like a 2-category or bicategory here, but that would lead us too far astray for now. ↩︎

7. This really needs a bit more explanation. I may put more details later. ↩︎

8. To make this statement precise we should ask the monad to be "finitary" or allow the signature to have a proper class of operations of infinitary arity. ↩︎