Kleisli Categories

Last time, we discussed one of the standard categories associated with a monad, the Eilenberg-Moore category. This time, we discuss the other, the Kleisli category, and its significance.

For a monad $\mathbb{T}$ on $\mathcal{C}$ , the Kleisli category, denoted $\mathcal{C}_{\mathbb{T}}$ , has:

Objects: The objects of $\mathcal{C}$ .
Morphisms: A morphism of type $A \rightarrow B$ is a $\mathcal{C}$ -morphism of type $A \rightarrow \mathbb{T}(B)$ .

Unlike many simple categorical constructions, the composition and identities are not inherited from the base category. Instead, the identity at $A$ is given by the component of the unit at $A$ , $\eta_A$ . For two Kleisli morphisms $f : A \rightarrow B$ , and $g : B \rightarrow C$ , we shall write their composite as $g \bullet f$ . This is given by the following composite of their underlying $\mathcal{C}$ -morphisms:

$A \xrightarrow{f} \mathbb{T}(B) \xrightarrow{\mathbb{T}} \mathbb{T}^2(C) \xrightarrow{\mu_C} \mathbb{T}(C)$

A Computational Perspective

The popular intuition in computer science is that the Kleisli category of appropriately chosen monads can give a compositional model for various forms of effectful computation.

Example: For the list monad $\mathbb{L}$ , we can think of a Kleisli morphism $f : A \rightarrow B$ as producing a list of possible outputs. This can be seen as a crude form of non-deterministic computation. The identity $\mathsf{id}_A$ is the function of type $A \rightarrow \mathbb{L}(A)$ acting as:

$a \mapsto [a]$ .

So the identity “deterministically” returns its input as its output. Now if we consider two Kleisli maps $f : A \rightarrow B, g : B \rightarrow C$ , their composite acts as follows:

Input $a$ is mapped by $f$ to some list of possible outputs, say $[a_1,\ldots,a_n]$ .
The output of $f$ is transformed by applying $g$ element-wise to produce a list-of-lists $[g(a_1),\ldots,g(a_n)]$ .
The multiplication concatenates the results together into a single output list.

Encoding non-determinism via lists is favoured in many software programming contexts as they have an efficient representation as a datatype. A perhaps more satisfactory mathematical representation of (unbounded) non-determinism is the following.

Example: The Kleisli category of the powerset monad is equivalent to the category of sets and relations between them.

Example: Recall the state monad for a set $S$ , constructed from the Cartesian closure of $\mathsf{Set}$ . A Kleisli map $A \rightarrow B$ for this monad is a function of type $A \rightarrow S \Rightarrow (B \times S)$ . For $a \in A$ , $f(a)$ is a function taking a state value, and producing an element of $B$ and a new state value. The Kleisli composition of such maps does exactly what a programmer might hope, threading state and computation values through a composite of two such stateful computations.

An Algebraic Perspective

As well as this computational perspective, as has been the case for other aspects of monads, it is instructive to consider an algebraic point of view as well.

Consider an equational presentation $(\Sigma,E)$ , and the monad $\mathbb{T}$ it induces, as discussed in earlier posts. A Kleisli morphism $f : A \rightarrow B$ is a function $f : A \rightarrow \mathbb{T}(B)$ . We can think of this as an $A$ -indexed family of equivalence classes of terms with variables in $B$ , which we might write as $([t_a])_{a \in A}$ (Recall $[t]$ denotes an equivalence class with representative $t$ ). If we have a second morphism $g : B \rightarrow C$ , this is a function $g : B \rightarrow \mathbb{T}(C)$ , that is a $B$ -indexed family of terms with variables ranging over $C$ . Denote this family $([t'_b])_{b \in B}$ . The composite $g \bullet f$ will encode an $A$ -indexed family of terms with variables in $C$ . Formally, this family is:

$([t_a[t'_b / b \mid b \in B]])_{a \in A}$

Here the notation $t[t'_b / b \mid b \in B]$ denotes substituting each occurrence of variable $b$ appearing in term $t$ with $t_b$ .

So algebraically, the Kleisli category has morphisms families of (equivalence classes of) terms, and composition is substitution. From this point of view, the identity morphism at $A$ is $\eta_A$ , which corresponds to the trivial family:

$([a])_{a \in A}$