Probably Random

A blog by Paul Siegel

Monads

September 13, 2017

Monads and comonads were invented in the 1950’s to solve the descent problem in geometry and topology: how, in general, can local constructions be glued together to form a global geometric object? But since their initial success (particularly in the work of Grothendieck) they have been recognized much more broadly in mathematics. This post is part of a series aimed at understanding the importance of category theory in modern computer science, and monads play a particularly prominent role in that overlap.

More specifically, monads are a popular design pattern in functional programming. They allow programmers to enrich complex data processing pipelines with additionl structure to help manage side effects or replicate familiar data structures from object-oriented programming. A full discussion of monads in functional programming will have to wait for a future post, but the reader who already has some familiarity with the functional style may recognize hints of what is to come.

Examples of (co)monads

Recall that an adjunction between categories $\C$ and $\D$ consists of a pair of functors $F \colon \D \to \C$ and $G \colon \C \to \D$ together with unit/counit natural transformations

\[u \colon 1_\D \to GF \quad \text{and} \quad v \colon FG \to 1_\C\]

which satisfy two adjunction identities.

One can think of $F$ and $G$ as being “almost inverses”, with the unit/counit pair measuring how far they are from being actual inverses. Given this setup, the functor $GF$ is an example of a monad, and $FG$ is an example of a comonad. (Of course a (co)monad is not just a bare functor - one considers the unit and counit to be part of the structure.)

In fact, this is the only source of examples of monads and comonads. We will provide axiomatic definitions later on, but it is a theorem that every (co)monad satisfying those axioms is inducd by an adjunction (in fact many adjunctions in general) as described above.

Example: the product monad

Let us begin by examining the monad and comonad associated to the product / diagonal adjunction constructed in my post on adjunctions. This adjunction consisted of the product functor $P \colon \Set^2 \to \Set$ which sends a pair of sets to their product together with its left adjoint, the diagonal functor $\Delta \colon \Set \to \Set^2$.

The monad associated to this adjunction is the functor

\[P \Delta \colon \Set \to \Set\]

which sends an object $X$ to $X \times X$ and a morphism $f$ to the morphism $f \times f$.

The comonad associated to this adjunction is the functor

\[\Delta P \colon \Set^2 \to \Set^2\]

which sends a pair of sets $(X, Y)$ to $(X \times Y, X \times Y)$ and a pair of functions $(f, g)$ to the $(f \times g, f \times g)$.

We will discuss the role that the counit and unit natural transformations play in these constructions later on.

Example: Galois connections

Recall that a Galois connection is an adjunction between two posets (equipped with their natural category structures). In my post on the subject, I went through the proof that a Galois connection between $(A, \leq_A)$ and $(B, \leq_B)$ is the same thing as a pair of increasing functions $F \colon B \to A$ and $G \colon A \to B$ with the property that

\[\begin{equation} \label{gal_connection} F(b) \leq_A a \iff b \leq_B G(a) \end{equation}\]

for every $a \in A$, $b \in B$.

What is a monad in this language? Let us show that the functor $M = GF$ satisfies three axioms:

This follows from the fact that $F$ and $G$ are increasing (which in turn follows from the fact that $F$ and $G$ are functors).

Indeed, we have $F(b) \leq_A F(b)$ by reflexivity, and thus $b \leq_B GF(b)$ by \eqref{gal_connection}.

To prove this, note that $M^2(b) \leq_B M(b)$ since $M$ is extensive. Moreover $F(b) \leq_A FGF(b)$ by \eqref{gal_connection} applied to the reflexive inequality $GF(b) \leq_B GF(b)$, and thus $GF(b) \leq_B GFGF(b)$ since $G$ is increasing. This is equivalent to $M(b) \leq_B M^2(B)$, so we conclude that $M(b) = M^2(B)$ by antisymmetry of $\leq_B$.

A function $M$ which satisfies the three axioms above is traditionally called a closure operator, so we have shown that for any Galois connection $(F, G)$ the corresponding monad $M = GF$ is a closure operator. It will follow from more general considerations involving the relationship between adjunctions and monads that every closure operator comes from a Galois connection as above, so in fact the monads on a poset are precisely the closure operators on that poset.

Show that the comonad $FG$ is a closure operator on the poset obtained by reversing the partial ordering $\leq_A$ on $A$.

The monad axioms

It is entirely possible to develop the theory of monads from the point of view that a monad is the composition of the right adjoint functor with the left adjoint functor coming from an adjunction between two categories. But this definition is unsatisfactory since many different adjunctions can give rise to the same monad and thus it is difficult to see what the monad itself actually is. In this section we will define monads axiomatically and then show that the construction via adjunctions satisfies the axioms. In a future post we will show that every monad in the sense of the axioms comes from an adjunction, so that the two possible definitions are equivalent.

Let $\D$ be a category. A monad on $\D$ is a functor $M \colon \D \to \D$ equipped with a pair of natural transformations $u \colon 1_\D \to M$ and $j \colon M^2 \to M$ called the unit and join transformations, respectively, which satisfy the following coherence conditions:

\[j \circ Mj = j \circ jM\]

as natural transformations $M^3 \to M$ and:

\[j \circ Mu = j \circ uM = 1_M\]

as natural transformations $M \to M$.

Let $F \colon \D \to \C$ be a functor which is left adjoint to $G \colon \C \to \D$ via the unit $u \colon 1_\D \to GF$ and counit $v \colon FG \to 1_\C$. Then $M = GF$ equipped with the unit $u$ and join $j = GvF$ is a monad in the sense of the definition above.

Note that $j$ is the natural transformation $GFGF \to GF$ whose component at an object $D$ of $\D$ is the morphism $G(v_{F(D)})$. So $j$ is indeed a natural transformation $M^2 \to M$, and we must show that $M$, $u$, and $j$ satisfy the coherence conditions.

Let us begin with the identity $j \circ Mj = j \circ jM$. We have:

\[j \circ Mj = GvF \circ GFGvF = G(v \circ FGv)F\]

Let us pause to review what it means for $v$ to be a natural transformation $FG \to 1_\C$. For any morphism $f \colon C_1 \to C_2$ in $\C$ we have:

\[v_{C_2} \circ FG(f) = 1_\C(f) \circ v_{C_1} = f \circ v_{C_1}\]

Applying this to the morphism $v_C \colon FG(C) \to C$ where $C$ is any object of $\C$, we get:

\[v_C \circ FG(v_C) = v_C \circ v_{FG(C)}\]

But the left-hand side of this equation is the component of $v \circ FGv$ and the right-hand side is the component of $v \circ vFG$ at $C$, so these two natural transformations are equal. This gives:

\[j \circ Mj = G(v \circ FGv)F = G(v \circ vFG)F = GvF \circ GvFGF = j \circ jM\]

as desired.

It remains only to prove that $j \circ Mu = j \circ uM = 1_M$. We shall prove that $j \circ Mu = 1_M$ and leave the other identity to the reader. We have:

\[j \circ Mu = GvF \circ GFu = G(vF \circ Fu)\]

But $vF \circ Fu = 1_F$ according to the definition of adjunction, so $j \circ Mu = G 1_F$. The component of $1_F$ at an object $D$ of $D$ is just the identity morphism $F(D) \to F(D)$, so the component of $G 1_F$ at $D$ is the identity morphism $GF(D) \to GF(D)$ since $G$ is a functor. Since $M = GF$ we conclude:

\[j \circ Mu = G 1_F = 1_M\]

as desired. The identity $j \circ uM = 1_M$ follows similarly using the adjunction identity $Gv \circ uG = 1_G$.

Formulate a similar set of axioms for comonads, and prove that if $F$ is left adjoint to $G$ then $FG$ (equipped with the appropriate extra structure) is a comonad.

Examples revisited

With the proper definition of a monad in hand, let us revisit the examples from the first section of this post, placing emphasis on the role of the unit and join transformations. We’ll also throw in some examples from the category of graphs.

Example: the product monad

We saw before that the functor $M \colon \Set \to \Set$ which sends a set $X$ to $X \times X$ and a function $f$ to $f \times f$ is a monad in the sense that it is the composition of the product functor with its left adjoint. Let us now give $M$ the structure of a monad in the sense of the monad axioms.

Define the unit $u \colon 1_{\Set} \to M$ component-wise to be the family of functions $u_X \colon X \to X \times X$ given by $u_X(x) = (x,x)$. Similarly define the join $j \colon M^2 \to M$ component-wise to be the family of functions

\[j_X \colon X \times X \times X \times X \to X \times X\]

given by $j(x_1, x_2, x_3, x_4) = (x_1, x_4)$. Let us check that the triple $M$, $u$, $j$ is a monad.

We begin with the coherence condition $j \circ Mj = j \circ jM$. The component of each side at a set $X$ is a morphism $M^3(X) \to M(X)$ which corresponds to a function $X^8 \to X^2$. We have:

\[\begin{align*} (j \circ Mj)_X(x_1, \ldots, x_8) &= (j_X \circ M(j_X))(x_1, \ldots, x_8) \\ &= (j_X \circ j_X \times j_X)(x_1, \ldots, x_8) \\ &= j_X((j_X(x_1, \ldots, x_4), j_X(x_5, \ldots, x_8))) \\ &= j_X(x_1, x_4, x_5, x_8) \\ &= (x_1, x_8) \end{align*}\]

On the other hand,

\[\begin{align*} (j \circ jM)_X(x_1, \ldots, x_8) &= (j_X \circ j_{M(X)})(x_1, \ldots, x_8) \\ &= (j_X \circ j_{X \times X})(x_1, \ldots, x_8) \\ &= j_X(j_{X \times X}((x_1, x_2), (x_3, x_4), (x_5, x_6), (x_7, x_8))) \\ &= j_X((x_1, x_2), (x_7, x_8)) \\ &= (x_1, x_8) \end{align*}\]

Thus $j \circ Mj = j \circ jM$, as desired.

We will conclude by verifying the identity $j \circ uM = 1_M$, leaving the final coherence condition $j \circ Mu = 1_M$ to the reader. Both sides are natural transformations $M \to M$, so the component of each side at a set $X$ is a morphism $M(X) \to M(X)$, i.e. a function $X \times X \to X \times X$. Evaluating at a point $(x_1, x_2) \in X \times X$ gives:

\[\begin{align*} (j \circ uM)_X(x_1, x_2) &= (j_X \circ u_{M(X)})(x_1, x_2) \\ &= (j_X \circ u_{X \times X})(x_1, x_2) \\ &= j_X(u_{X \times X}(x_1, x_2)) \\ &= j_X(x_1, x_2, x_1, x_2) \\ &= (x_1, x_2) \end{align*}\]

But of course $(1_M)_X(x_1, x_2) = (x_1, x_2)$ as well, so indeed $j \circ uM = 1_M$ as desired.

Example: monads over posets

We saw in the example involving Galois connections that a monad induced by an adjunction between two posets is a closure operator. Here we will prove the (nearly trivial) result that the monads over a poset in the sense of the axiomatic definition of the previous section are precisely the closure operators.

Let $(A, \leq_A)$ be a poset and let $M \colon A \to A$ be a function. Then $M$ has the structure of a monad if and only if $M$ is a closure operator.

Suppose $M$ is a monad, meaning it is a functor and it comes equipped with a unit $u \colon 1_A \to M$ and a join transformation $j \colon M^2 \to M$ which satisfy the coherence conditions. We must show that $M$ is increasing, extensive, and idempotent.

$M$ is increasing because the functors on a poset are precisely the increasing functions.

$M$ is extensive because the component of $u$ at an object $a \in A$ is a morphism $u_a \colon a \to M(a)$, and the existence of such a morphism is equivalent to the statement that $a \leq_A M(a)$.

To prove that $M$ is idempotent, note that $M(a) \leq_A M^2(A)$ since $M$ is extensive and increasing. Moreover the component of $j$ at an object $a \in A$ is a morphism $j_a \colon M^2(a) \to M(a)$, and the existence of such a morphism is equivalent to the statement that $M^2(a) \leq_A M(a)$. Thus $M(a) = M^2(a)$ by antisymmetry of $\leq_A$.

Conversely, suppose $M$ is a closure operator.

$M$ is a functor because, as above, a functor on a poset is the same thing as an increasing function.

Since $M$ is extensive we have $a \leq_A M(a)$ for all $a \in A$ and thus there is a unique morphism from $a$ to $M(a)$; call this morphism $u_a$. It is straightforward to check that the $u_a$’s assemble to form a natural transformation $u \colon 1_A \to M$.

The rest of the conditions in the definition of a monad a trivial: the join transformation and the natural transformations appearing in the coherence conditions are all natural transformations $M \to M$ since $M$ is idempotent, and the only such natural transformation is $1_M$ since its component at any $a \in A$ must be the unique morphism from $M(a)$ to itself.

Show that every monad on a poset is induced by a Galois connection. (Hint: given a closure operator $M$ on a poset $(A, \leq_A)$, consider the poset $(M(A), \leq_A)$.)

Monads and graphs

We conclude this post with some exercises involving monads on the category $\tbf{Gph}_0$ of graphs with loops allowed.

Define a functor $U \colon \tbf{Gph}_0 \to \tbf{Gph}_0$ which sends a graph $G$ to the graph obtained by adjoining a single vertex to $G$ and no additional edges. Construct a unit and a join transformation which gives $U$ the structure of a monad.

Define a functor $C \colon \tbf{Gph}_0 \to \tbf{Gph}_0$ which sends a graph $G$ to the graph with the same vertex set $V$ as $G$ and edge set $V \times V$. Construct a unit and a join transformation which gives $C$ the structure of a monad.

Given $G \in \tbf{Gph}_0$, define $\pi_0(G)$ to be the graph with one vertex for each connected component of $G$ and one loop based at each vertex. Show that $G \mapsto \pi_0(G)$ defines a functor $\tbf{Gph}_0 \to \tbf{Gph}_0$, and construct a unit and a join transformation which gives $\pi_0$ the structure of a monad.