The Kleisli Category and Monads in Programming

The Eilenberg–Moore category resolves a monad into an adjunction by building the category of all its algebras. Kleisli's construction, a decade older, resolves the same monad with far less structure: keep the objects of the base category, and redefine what an arrow is.¹ The resulting category is the category of free algebras. Read through computer science, it is the category of effectful programs, with the monad's multiplication as the sequencing operation.

The construction

To follow $f$ with $g$: run $f$, landing in $TB$; the next step $g$ expects a bare $B$, so apply $T$ to it, giving $Tg:TB\to T^{2}C$; the result is doubly wrapped, so flatten with ${\mu }_C$. Each piece of the monad has a role. $T$ lifts the second program over the first one's effect, $\mu$ merges the two layers of effect, and $\eta$ provides the do-nothing program.

The verification uses each monad law once. Associativity of $\bullet$ follows from the associativity law of the monad plus naturality of $\mu$; the unit laws of the monad make $\eta$ a two-sided identity.²

The Kleisli adjunction

$\mathcal{K}(\mathbb{T})$ resolves the monad. Define

• $F:\mathcal{C}\to \mathcal{K}(\mathbb{T})$ by $FA=A$ and, for $g:A\to B$, $Fg={\eta }_B\circ g$ (a pure program, run through the unit);
• $U:\mathcal{K}(\mathbb{T})\to \mathcal{C}$ by $UA=TA$ and, for a Kleisli arrow $f:A\to TB$, $Uf={\mu }_B\circ Tf:TA\to TB$.

Then $F⊣U$, and $UF=T$ with the induced multiplication equal to $\mu$.³ The monad we started from is recovered, so every monad arises from an adjunction by this construction alone — the Eilenberg–Moore route is a second, independent proof of the same fact.

Kleisli arrows as effectful programs

Barr & Wells model a functional programming language as a category: types are objects, programs are arrows, and composition is running one program after another.⁴ That model handles pure programs. A program with an effect — one that may fail, log output, consult state, or return several results — does not fit the shape $A\to B$; it fits $A\to TB$ for the monad $T$ encoding the effect. The Kleisli category is then the category whose arrows are effectful programs, and Kleisli composition runs them in sequence.

For the maybe monad, take partial programs $f:A\to B+1$ and $g:B\to C+1$. Then $Tg:B+1\to (C+1)+1$ sends the failure point to the outer failure point, and ${\mu }_C$ merges the two failure points into one. The composite $g\bullet f$ fails when either stage fails and returns $g(f(a))$ otherwise, the propagation a programmer would otherwise write by hand as a case analysis.

The same element-chase works for the state monad. Take $TB=(B\times S{)}^S$ and Kleisli arrows $f:A\to (B\times S{)}^S$ and $g:B\to (C\times S{)}^S$: each is a program that, given a start state, returns a result and an end state. Starting from $a\in A$ and $s_0\in S$:

• $f(a)(s_0)=(b,s_1)$: the first program runs, producing $b$ and an updated state $s_1$;
• $Tg(f(a))$ is the function $s\mapsto (g(b),s_1)$-shaped element of $T^{2}C$ — a stateful computation returning another stateful computation;
• ${\mu }_C$ runs the outer computation and feeds its end state to the inner one, giving $(g\bullet f)(a)(s_0)=g(b)(s_1)$.

The composite threads the state from left to right; the multiplication carries the state-passing. Sequential, stateful execution order is part of $\mu$ for this particular $T$, not a convention added to the notation.

Bind

Functional languages present Kleisli composition through the operator bind, written >>=. Bind takes an effectful value and a Kleisli arrow and applies the arrow under the effect:

Bind and Kleisli composition are interdefinable: $g\bullet f=\lambda a.f(a)>>=g$, and conversely bind is composition with a constant first program. In this notation the monad laws become the three program equivalences

which say that pure steps can be inlined and that sequencing is associative — a block of effectful code means the same thing however it is parenthesized. do-notation is the direct syntax for iterated bind: each line $x\leftarrow f(\dots )$ binds the result of a Kleisli arrow and passes it on, and the desugaring is a right-nested chain of >>=. The associativity law is what makes the flat, line-by-line reading legitimate.

Substitution and evaluation

Barr & Wells give a reading of Kleisli arrows that predates the effects vocabulary: substitution.⁵ Take the list monad and a Kleisli arrow $f:A\to B^{\ast }$ on alphabets $A=\{a,b\}$, $B=\{c,d,e\}$ with $f(a)=cddc$ and $f(b)=ec$. Applying $Tf$ to the string $abba\in A^{\ast }$ substitutes a string for each letter:

and $\mu$ concatenates the result to $cddcececcddc\in B^{\ast }$. The multiplication carries out a computation: it evaluates a formal expression using the algebra structure — here the monoid operation, since the algebras of the list monad are monoids. For a monad built from ring-like structure the free algebra consists of polynomial expressions and $\mu$ evaluates the polynomial. Kleisli arrows are substitutions; $\mu$ is evaluation. This viewpoint, developed through the notion of strong monad, is the root of the monads-as-computation literature.⁶

The Kleisli category as free algebras

The two resolutions of a monad are related concretely: the Kleisli category is the full subcategory of the Eilenberg–Moore category on the free algebras.

The equivalence sends the Kleisli object $A$ to the free algebra on $A$; a Kleisli arrow $A\to TB$ corresponds, by freeness, to a unique algebra morphism $(TA,{\mu }_A)\to (TB,{\mu }_B)$. Under this identification $U$ becomes the restriction of the Eilenberg–Moore forgetful functor.

The resolution spectrum

Fix a monad $\mathbb{T}$ on $\mathcal{C}$ and consider all adjunctions $F^{\prime }⊣G^{\prime }$ inducing it. These form a category (arrows are functors between the codomains commuting with both sides), and the two constructions of this module are its endpoints:

• Kleisli is initial. For any inducing adjunction with codomain $\mathcal{B}$ there is a unique functor $\mathcal{K}(\mathbb{T})\to \mathcal{B}$ commuting with the adjunctions — it sends $A$ to $F^{\prime }A$, and exists because every Kleisli object is free.
• Eilenberg–Moore is terminal. The comparison functor$\mathcal{B}\to {\mathcal{C}}^{\mathbb{T}}$ is the unique functor the other way.

Any category of things the monad acts on therefore contains the free algebras and embeds in the full category of algebras. For the list monad the spectrum runs from the category of free monoids to the category of all monoids, with every variety of monoid-like structure inducing the same monad falling in between.

Two factorizations, two disciplines

The contrast between the endpoints organizes how the two fields use monads.

Mathematics centers on the whole category of algebras (monadicity, transfer of limits, algebraic theories), so Eilenberg–Moore dominates. Computer science centers on sequencing effectful computations over base types, which never leaves the free algebras, so Kleisli dominates.⁸ Both categories induce the monad exactly.

Dropping the unit and multiplication and keeping only the endofunctor gives the theory of algebras for an endofunctor, where initiality replaces freeness and inductive datatypes appear as least fixed points.