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 on , the Kleisli category, denoted , has:
- Objects: The objects of .
- Morphisms: A morphism of type is a -morphism of type .
Unlike many simple categorical constructions, the composition and identities are not inherited from the base category. Instead, the identity at is given by the component of the unit at , . For two Kleisli morphisms , and , we shall write their composite as . This is given by the following composite of their underlying -morphisms:
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 , we can think of a Kleisli morphism as producing a list of possible outputs. This can be seen as a crude form of non-deterministic computation. The identity is the function of type acting as:
So the identity “deterministically” returns its input as its output. Now if we consider two Kleisli maps , their composite acts as follows:
- Input is mapped by to some list of possible outputs, say .
- The output of is transformed by applying element-wise to produce a list-of-lists .
- 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 , constructed from the Cartesian closure of . A Kleisli map for this monad is a function of type . For , is a function taking a state value, and producing an element of 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 , and the monad it induces, as discussed in earlier posts. A Kleisli morphism is a function . We can think of this as an -indexed family of equivalence classes of terms with variables in , which we might write as (Recall denotes an equivalence class with representative ). If we have a second morphism , this is a function , that is a -indexed family of terms with variables ranging over . Denote this family . The composite will encode an -indexed family of terms with variables in . Formally, this family is:
Here the notation denotes substituting each occurrence of variable appearing in term with .
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 is , which corresponds to the trivial family:
This family acts as a two sided identity with respect to substitutions as required.