Monads, from motivic spectra to functional programming

Monads come from two completely different worlds depending on who you ask. Mathematicians get them from adjunctions. Functional programmers get them from a typeclass with pure and bind. The shared name is no accident, and the bridge between the two views is the Kleisli category. Once you see it, the translation between composing effects in code and composing adjoints feels obvious.

I spent my PhD doing motivic homotopy theory, where adjunctions are everywhere. Now I write Lean 4 most days (it's my favourite FP language, which is why every code snippet below is in Lean), and a do block reads to me as a chain of unit and counit calculations. This post is partly notes to myself about why those two pictures are the same picture.

The definition

A monad on a category $\mathcal{C}$ is an endofunctor $T : \mathcal{C} \to \mathcal{C}$ with two natural transformations, a unit and a multiplication,

satisfying associativity and unit laws. Nothing here forces you to think of $T$ as a computational effect. It is an endofunctor with monoid-like structure, full stop.

The main source of monads in math is adjunctions. Given $L \dashv R$ with $L : \mathcal{C} \to \mathcal{D}$ and $R : \mathcal{D} \to \mathcal{C}$, you get a monad $T = R \circ L$ on $\mathcal{C}$ for free. The unit $\eta$ is the unit of the adjunction. The multiplication is $\mu = R \varepsilon L$, where $\varepsilon : LR \Rightarrow \mathrm{Id}$ is the counit.

Where this lives in algebraic geometry

If you work in algebraic geometry or motivic homotopy theory, adjunctions are not exotic. They are how you compute.

Take an open inclusion $\iota : U \hookrightarrow X$ of schemes. On sheaves or spectra you have $\iota^* \dashv \iota_*$, and the induced monad on $\mathrm{Sh}(X)$ is $T = \iota_* \iota^*$. It sends a sheaf $F$ to the sheaf you get by restricting to $U$ and pushing back out, forgetting whatever $F$ did outside $U$. The unit $F \to \iota_* \iota^* F$ is the restriction map. Since $\iota$ is an open immersion, the counit $\iota^* \iota_* \Rightarrow \mathrm{Id}$ is an isomorphism, so $\mu$ is too. The monad is idempotent. Localizing twice at $U$ is the same as localizing once.

Things get more interesting in the six-functor formalism on $\infty$-categories of motivic spectra $\mathbf{SH}(-)$. For a structural morphism $f : X \to S$, the adjunction $f^* \dashv f_*$ gives a monad $T = f_* f^*$ on $\mathbf{SH}(S)$, and this monad encodes the cohomology of $X$. Evaluating on the motivic sphere spectrum $\mathbb{S}_S$ gives $f_* f^* \mathbb{S}_S \simeq f_* \mathbb{S}_X$, the spectrum representing cohomology of $X$ over $S$.

The piece I find most beautiful is what the multiplication does. The map $\mu$ is induced by the counit $\varepsilon : f^* f_* \Rightarrow \mathrm{Id}$, and when you apply it to these spectra, the map $f_* f^* f_* f^* \Rightarrow f_* f^*$ is the cup product in cohomology. The unit $\eta : \mathrm{Id} \Rightarrow f_* f^*$ is the inclusion of constants. None of this looks remotely like a programming construct, but the categorical pattern is identical to how software engineers thread state and I/O.

The Kleisli category

To get from one world to the other you need the Kleisli construction. For a monad $T$, the Kleisli category $\mathcal{C}_T$ has the same objects as $\mathcal{C}$. A morphism $A \to B$ in $\mathcal{C}_T$ is a morphism $A \to TB$ in $\mathcal{C}$.

The identity at $A$ in $\mathcal{C}_T$ is $\eta_A : A \to TA$. Composition of $f : A \to TB$ and $g : B \to TC$ goes through $T$ and collapses via $\mu$:

For the motivic cohomology monad above, Kleisli composition is pulling back, pushing forward, and gluing with the cup product. For a programmer, Kleisli composition is sequencing effectful operations. The morphisms are the same shape.

Lean 4

In Lean 4 a monad is a typeclass:

class Monad (m : Type u → Type v) where
  pure : α → m α
  bind : m α → (α → m β) → m β

The dictionary is direct.

• pure is $\eta$.
• bind, often written >>=, is Kleisli composition evaluated at a point.

When you write a do block,

do
  let x ← e1
  let y ← e2 x
  pure (x + y)

it desugars into a chain of continuations:

e1 >>= fun x =>
e2 x >>= fun y =>
pure (x + y)

Every line is a morphism $A \to TB$. The do notation is sugar over a long chain of Kleisli compositions. The associativity of bind is the associativity of the Kleisli category, restated as a monad law.

The state monad as an adjunction

The classic example. Fix a set $S$ of states. In $\mathbf{Set}$ you have the tensor-hom adjunction

with the right adjoint sending $A$ to $A^S = \mathrm{Hom}(S, A)$. The induced monad on $\mathbf{Set}$ is

the type of a stateful computation returning a value in $A$. The unit $\eta$ sends $a$ to the constant function $s \mapsto (a, s)$. The multiplication $\mu$ comes from the counit of the adjunction, the evaluation map $\mathrm{ev} : S \times A^S \to A$ given by $(s, f) \mapsto f(s)$.

In Lean 4:

def State (σ α : Type) := σ → α × σ

instance : Monad (State σ) where
  pure a := fun s => (a, s)
  bind x f := fun s =>
    let (a, s') := x s
    f a s'

The body of bind is $\mu$ working. You run the first computation to get an updated state, then feed the new state into the next. Threading state by hand is what $\mu$ does for you in the abstract.

Free monads and syntax

Most everyday FP monads come from less geometric, free-forgetful adjunctions. Option, the functor $A \mapsto A + 1$, comes from the free pointed set adjunction. List comes from the free monoid adjunction. In each case $T$ is the composite of free and forgetful functors.

A cleaner way to see the same thing is through polynomial functors. A polynomial functor $P(Z) = \sum_{b \in B} Z^{E_b}$ is a signature: operations $b \in B$ with input arities indexed by $E_b$. The free monad $T_P$ satisfies

so $T(A)$ is the set of finite formal syntax trees built from your operations, with leaves of type $A$.

For $P(Z) = Z^2$, terms are binary trees $b(x, b(y, z))$. The free magma. Quotient by associativity and you pass from the free monad to the category of Eilenberg-Moore algebras, getting semigroups.

In math, a free monad is pure formal syntax, and an algebra over it is evaluating the syntax subject to laws. In functional programming the same idea has a name, the Free Monad pattern. You define your program's effects as a polynomial functor, then write an interpreter (an Eilenberg-Moore algebra) to give those effects meaning.

Why both sides agree

So why does the same pattern govern side effects in Haskell and stable motivic homotopy theory? Because adjunctions are everywhere, and every adjunction comes with a monad for free.

The interesting asymmetry is which side you start from. In math, you reach for the adjunction first, pullback against pushforward, left adjoint against right adjoint, and the monad shows up as bookkeeping for operations like the cup product. In FP, you reach for the monad first, and the adjunction is hidden behind the typeclass.

A programmer threading state through a do block is doing the same categorical motion as a geometer pushing through a unit and a counit. Different vocabularies, same algebra.