The ins and outs of monads

In previous posts we have seen a lot of the basic mathematical infrastructure of monads. The aim of this post is to adopt a computational view on monads, viewing $\mathbb{T}(X)$ as effectful computations over an object $X$ . From this perspective, we shall consider two natural questions:

How can we build such computations? In other words, how do we get things into $\mathbb{T}(X)$ ?
What can we do with computations once have have built them? In other words, how to we get things back out of $\mathbb{T}(X)$ ?

There is a lot of discussion of these topics in the literature. As usual, we will try and keep things simple, restricting attention to simple monads on $\mathsf{Set}$ , and concentrating on the key ideas.

Building computations

So far, the only way have have seen to build elements of $\mathbb{T}(X)$ is to apply the monad unit $\eta_X$ .

Example: For the exception monad, for set of exceptions $E$ , the value $\eta(x) = (1,x) \in X + E$ is a trivial computation that returns the value $x$ , and doesn’t throw an exception.

Example: The finite powerset monad $\mathbb{P}$ can be seen as a form of bounded non-determinism. $\eta(x) = \{ x \} \in \mathbb{P}(X)$ is a trivially non-deterministic computation that always results in the value $x$ .

Example: The list monad $\mathbb{L}$ can be seen as a form of non-determinism which can be easier to implement in a programming language. It is unusual as there is an order on computations, and repeated values are allowed. Obviously another perspective is to see such computations as living in a list data structure. Again $\eta(x) = [x]$ is the trivial singleton list containing only the value $x$ .

The intuition we derive from these examples is that $\eta(x)$ yields a trivially effectful computation in some suitable sense. To get any real use out of these computational effects, we need to be able to build less boring examples as well. To solve this problem, as usual we shall adopt an algebraic perspective. Assume we have an equational presentation $(\Sigma, E)$ . An $n$ -ary operation $o \in \Sigma$ induces a function $\mathbb{T}^n(X) \mapsto \mathbb{T}(X)$ as follows:

$([t_1],\ldots,[t_n]) \mapsto [o(t_1,\ldots,t_n)]$

Continuing the examples above:

Example: The exception monad has a presentation consisting of a constant $e$ for each exception in $E$ . These induce functions $\mathsf{raise}_e : 1 \rightarrow \mathbb{X}$ with action $\star \mapsto e$ , which we can think of as raising the exception $e$ .

You may wonder where the notion of catching or handling an exception appears. This is a good question, and will be addressed in the next section.

Example: The finite powerset monad has a presentation with a binary operation $\vee$ and a constant element $\bot$ . The constant induces a function $\bot : 1 \rightarrow \mathbb{P}(X)$ with action $\star \mapsto \emptyset$ , which we can think of as picking out a diverging computation.

The binary operation induces an operation $\vee : \mathbb{T}(X)^2 \rightarrow \mathbb{X}$ with action $(U,V) \mapsto U \cup V$ , which takes two non-deterministic computations, and combines their possible behaviours. For example $\eta(x_1) \vee \eta(x_2)$ is a computation yielding either $x_1$ or $x_2$ .

Example: Similarly to the previous example, the list monad has a presentation with binary operation $\times$ , and a constant element $1$ . The constant induces a function $1 \rightarrow \mathbb{T}(X)$ with action $\star \mapsto []$ .

The binary operation induces a function $\mathbb{T}(X)^2 \rightarrow \mathbb{T}(X)$ with action $([x_1,\ldots,x_m],[x_{m + 1}, \ldots, x_{n}]) \mapsto [x_1,\ldots,x_n]$ concatentating two lists. We can interpret these operations as simply manipulating data structures, or more subtly as a form of non-determinism in which the operations respect the order on choices.

Rather than describe these operations directly in terms of substitutions, it would be better to phrase things in terms of the available monad structure. To do so, we abuse notation and let $m$ denote the set $\{1,\ldots,m \}$ . A family of $m$ equivalence classes of terms over $X$ , $([t_i])_{1 \leq i \leq m}$ , can be identified with a morphism $t: m \rightarrow \mathbb{T}(X)$ , and a single $m$ -ary term with a map $o : 1 \rightarrow \mathbb{T}(m)$ . The composite $t^* \circ o : 1 \mapsto \mathbb{T}(X)$ , where $t^*$ denotes the Kleisli extension of $t$ , corresponds to the substitution we are interested in:

$([t_1],\ldots,[t_n]) \mapsto [o(t_1,\ldots,t_n)]$

In fact, we have generalised slightly, as $o$ is now an arbitrary term, not just an operation appearing in the signature.

Of course, we expect these mapping $\mathbb{T}(X)^n \rightarrow \mathbb{T}(X)$ induced by Kleisli morphism to behave in a suitably uniform way. That is, they should be natural in some sense. This actually requires a modicum of care to get right. We should really consider our mapping as being of type $U_{\mathbb{T}}(X)^n \rightarrow U_{\mathbb{T}}(X)$ . Here, $U_{\mathbb{T}} : \mathsf{Set}_{\mathbb{T}} \rightarrow \mathsf{Set}$ is the forgetful functor from the Kleisli category. This has action on objects $X \mapsto \mathbb{T}(X)$ , so this rephrasing makes sense. We then note that the induced maps:

$U_{\mathbb{T}}^n(X) \rightarrow U_{\mathbb{T}}(X)$

are natural. This is sometimes phrased as being natural with respect to Kleisli morphisms. They also trivially interact well with the strength morphisms in $\mathsf{Set}$ . In more general categories, there is a bijection between:

Families of morphisms $U_{\mathbb{T}}^n(X) \rightarrow U_{\mathbb{T}}(X)$ Kleisli natural in $X$ , and interacting well with monad strength. These are referred to as algebraic operations.
Morphisms $1 \rightarrow \mathbb{T}(m)$ , referred to as generic effects.

To give a denotational semantics for a serious programming language, a lot more details need filling in. The category $\mathsf{Set}$ is not suitable for realistic work, but is certainly a helpful way to build up the basic intuitions.

Evaluating computations

Now we have some tools for building up elements of $\mathbb{T}(X)$ , what can we do with them? The unit and multiplication of a monad have types $\mathsf{Id} \Rightarrow \mathbb{T}$ and $\mathbb{T}^2 \Rightarrow \mathbb{T}$ , so so they give us no way “out of the monad”.

What we are looking for is a systematic way of building well-behaved maps of type $\mathbb{T}(X) \rightarrow Y$ for some $Y$ . The key idea is to recall the Eilenberg-Moore adjunction. For a set $X$ , the free algebra over $X$ is:

$F^{\mathbb{T}}(X) = (\mathbb{T}(X), \mu_X)$

The universal property of this adjunction means that if we can identity another Eilenberg-Moore algebra $(Y,\xi)$ , and a homomorphism

$h : X \rightarrow Y$

these bijectively corresponds to algebra homomorphisms:

$F^{\mathbb{T}}(X) \xrightarrow{\hat{h}} (Y,\xi)$

That is, morphisms

$\mathbb{T}(X) \rightarrow Y$

respecting the algebraic structure. It is worth considering the roles of these components:

The homomorphism $h : X \rightarrow Y$ specifies how values should be interpreted.
The algebra $(Y, \xi)$ specifies how the structure used to build up an effectful computation should be evaluated, in a manner respecting the structure encoded by the monad.

As usual, this is probably best understood by considering some examples.

Example: For the exception monad over $E$ , an Eilenberg-Moore algebra $(Y, \xi : Y + E \rightarrow Y)$ must act as the identity on the left component of the coproduct, and send each element of the right component to any value of its choosing in $Y$ . In other words, we specify a default value to take for each of the exceptions that might be raised. Given a function $h : X \rightarrow Y$ , the induced algebra morphism will map values according to $h$ , and otherwise chose the value specified by $\xi$ when it encounters a raised exception.

Example: For the finite powerset monad $\mathbb{P}$ , giving an Eilenberg-Moore algebra is equivalent to specifying a join semilattice structure. For example, we can consider the Eilenberg-Moore algebra on the natural numbers $\mathbb{N}$ specified by taking the maximum of pairs of elements, and bottom value $0$ . The resulting homomorphism $\mathbb{P}(\mathbb{N}) \rightarrow \mathbb{N}$ induced by the identity will map a finite set to its maximum value (inevitably defaulting to $0$ if the set is empty).

Example: The pattern for the list monad is similar. An Eilenberg-Moore algebra is a monoid, so we must specify a multiplication and unit element. For example if $X$ is the set of two by two matrices over the natural numbers, this carries a monoid structure under matrix multiplication. The identity on $X$ then induces a map $\mathbb{L}(X) \rightarrow X$ that multiplies a list of matrices together from left to right. Note that this example fundamentally exploits the fact that the multiplication operation is not forced to be commutative.

The ideas in this section are the basics of what are known as effect handlers. As with algebraic operations, to produce a denotational semantics for a realistic programming language, and more complex handlers, there are many details to take care of, and we must move beyond $\mathsf{Set}$ . However, this simplified setting is sufficient to illustrate the key ideas, without dealing with distracting technical details.

Summary

We have have seen the basic mathematical machinery to build effectful computations within a monad, and also how to evaluate these computation to values. The main points are:

The morphisms that allow us to build elements of $\mathbb{T}(X)$ arise naturally from an algebraic presentation of the monad.
The morphisms that allow us to evaluate computations in $\mathbb{T}(X)$ require us to make choices as to how that evaluation should proceed, specifically a suitable Eilenberg-Moore algebra, and then exploit the universal property of free algebras.

The literature in this area contains many nice examples, and is enjoyable to read. For algebraic operations and generic effects, search for work of Plotkin and Power, and for effect handlers, the work of Pretnar, Plotkin and Bauer are good places to start reading. There is a lot more to these topics than the details we have sketched here, so it is well worth exploring further.

We have also been limited in our example by the relatively simple monads we have introduced so far. We will see more interesting monads from a computational perspective in later posts.

Building computations

Evaluating computations

Summary

Share this:

Like this:

Related

Leave a Reply Cancel reply