Monads from Adjunctions

An adjunction $F⊣G$ between categories $\mathcal{A}$ and $\mathcal{B}$ induces structure on the domain side. The round trip $A\mapsto GFA$ is an endofunctor $T=GF:\mathcal{A}\to \mathcal{A}$; the unit $\eta :\mathrm{id}\to GF$ is a natural transformation into it; and the counit $\epsilon :FG\to \mathrm{id}$, inserted in the middle, produces a natural transformation $GFGF\to GF$ collapsing two applications of $T$ into one. That triple of data (an endofunctor, a unit into it, and a flattening map) is a monad, and it satisfies laws that make it a monoid.

Barr and Wells call the structure a triple, and the two words name the same thing.¹ The monad records what an adjunction does to its domain without reference to the codomain $\mathcal{B}$ or the functor $F$ that reached it. Two different adjunctions can induce the same monad, and every monad can be resolved back into an adjunction, generally into many.

The definition

Here $T\mu$ and $\mu T$ are the two whiskerings of $\mu$ by $T$: $T\mu$ has component $T({\mu }_A):T^{3}A\to T^{2}A$, while $(\mu T{)}_A={\mu }_{TA}:T^{3}A\to T^{2}A$. The associativity law states that the two ways of contracting a triple stack $T^{3}A$ down to $TA$ agree. The unit law states that inserting a fresh $T$-layer by $\eta$ (either underneath, as $\eta T$, or on top, as $T\eta$) and then multiplying returns the identity.

The diagonal maps in the second figure are identity arrows $TA\to TA$; the triangles assert that the two composites down through $T^{2}A$ equal them.

The monoid analogy

The laws reproduce the axioms of a monoid, transcribed one level up. A monoid $(M,e,m)$ in $\mathbf{Set}$ has a multiplication $m:M\times M\to M$ and a unit $e:1\to M$ satisfying associativity and the unit laws. Replace the set $M$ by an endofunctor $T$, the cartesian product $\times$ by composition of endofunctors, the one-point set $1$ by the identity functor, and the axioms become the monad laws.²

The category of endofunctors $[\mathcal{A},\mathcal{A}]$ carries a composition $\circ$ that plays the role of a product (a monoidal structure, with the identity functor as its unit). A monad is a monoid object in that monoidal category. Reading the table line by line gives the standard formulation: a monad is a monoid in the category of endofunctors.

Adjunctions induce monads

Write $T=GF$. The unit of the monad is the unit of the adjunction. The multiplication $\mu =G\epsilon F$ has component $G({\epsilon }_{FA}):GFGFA\to GFA$: it applies the counit in the middle, at the object $FA$, and transports the result back through $G$. The associativity and unit laws of the monad follow from the two triangle identities of the adjunction, applied under $G$ and over $F$.

Every adjunction gives a monad by this proposition, and conversely every monad arises from some adjunction, generally from many. The Kleisli and Eilenberg–Moore constructions produce two canonical adjunctions resolving a given monad; they sit at the two extremes of a poset of such resolutions.

The free monoid, as a monad

The free–forgetful adjunction between $\mathbf{Set}$ and $\mathbf{Mon}$ produces the first computational example. The free monoid on a set $A$ is $A^{\ast }$, the set of finite strings (lists) over $A$; forgetting the monoid structure returns the underlying set. Composing free after forgetful gives the endofunctor

with $Tf:A^{\ast }\to B^{\ast }$ mapping $f$ over each list. This is the list monad.⁴ Its unit and multiplication read off directly:

• Unit ${\eta }_A:A\to A^{\ast }$ sends an element $a$ to the singleton list $[a]$.
• Multiplication ${\mu }_A:(A^{\ast }{)}^{\ast }\to A^{\ast }$ takes a list of lists and concatenates it, erasing the inner brackets. For example $[[a,b],[c,d,e],[],[a,a]]$ flattens to $[a,b,c,d,e,a,a]$.

Associativity of the monad is associativity of concatenation: flattening a triply-nested list of lists gives the same result whether the inner brackets or the outer brackets go first. The unit laws say that wrapping every element as a singleton and then flattening, or wrapping the whole list once and then flattening, both leave the list unchanged.

Monoids and the writer monad

Barr and Wells give a second construction from a fixed monoid $M$, the representation triple.⁵ Define

where $1_M$ is the identity of $M$ and $m_1{m}_2$ is its product. The unit and multiplication of the monad are the unit and multiplication of $M$, threaded past the carried element $s$. In programming this is the writer monad: a value paired with an accumulated $M$-labelled output (a log, a running cost, a count), and $\mu$ combines two accumulations with the monoid operation. The monad laws reduce directly to the monoid laws of $M$.

This monad arises from the underlying-set / free adjunction on the category of $M$-sets, exactly as the list monad arises from $\mathbf{Set}$ and $\mathbf{Mon}$.

Monads as computational effects

A monad on $\mathbf{Set}$ packages a notion of computation producing an $A$ into the type $TA$. The unit injects a pure value as a trivial computation, and the multiplication collapses a computation-of-a-computation into a single one. The recurring examples of effectful programming are all monads.

The maybe monad $TA=A+1$ adds a distinguished no result point; $\mu :(A+1)+1\to A+1$ merges the two failure points into one, so a failure anywhere in a chain propagates. The state monad $TA=(S\to A\times S)$ makes a computation a function that consumes an initial state and returns a value together with a new state; $\mu$ threads the state through two such steps in order. Each entry is a monad on $\mathbf{Set}$ arising from an adjunction.

The algebras of these monads recover the corresponding categories of structured sets, and the multiplication becomes the sequencing operation of effectful programs in the Kleisli category.

Comonads

Dualizing the definition — reversing every arrow in the two coherence diagrams — gives a comonad, which Barr and Wells call a cotriple.⁶

An adjunction $F⊣G$ induces a comonad $(FG,\epsilon ,F\eta G)$ on $\mathcal{B}$, the codomain side, at the same time as it induces the monad $GF$ on $\mathcal{A}$. Where a monad models building up a structure and collapsing nested layers, a comonad models a context that can be observed ($\epsilon$) and duplicated ($\delta$): infinite streams, labelled trees, and stores of values are comonads. The Kleisli construction of a comonad — the co-Kleisli category — reappears in the theory of cartesian closed categories built from a comonad, a route into models of linear logic.⁷

Algebras, sequencing, and the bare endofunctor

Three constructions build on a monad:

• Algebras. Its algebras are objects carrying a $T$-structure map compatible with $\eta$ and $\mu$; they form the Eilenberg–Moore category.
• Sequencing. Its Kleisli category has as arrows $A\to TB$ the effectful programs, composed by $\mu$.
• The bare endofunctor. Dropping $\eta$ and $\mu$ leaves an endofunctor and its algebras, whose initial object is the least fixed point that models inductive datatypes.