The Continuation Monad

In this post, we introduce the continuation monad. This monad is slightly less well-behaved that some of the previous examples we have encountered, and a source of counterexamples to naive conjectures. Along the way, we will touch on some previous topics, such as monad morphisms, Kleisli and Eilenberg-Moore categories, and commutative monads.

The Monad Construction

We begin by establishing a relatively simple, but important form of adjunction. We do this at a greater level of generality than some of our earlier posts, to highlight the fairly minimal requirements. This adjunction then yields our monad in the usual way.

For any symmetric monoidal category \mathcal{V}, the monoidal closure means that for every object A, there is an adjunction:

(-) \otimes A \dashv A \multimap (-)

For a fixed object R, the functor (-) \multimap R is contravariant. That is, we can view it as having type \mathcal{V}^{op} \rightarrow \mathcal{V} or \mathcal{V} \rightarrow \mathcal{V}^{op} as is convenient to us.

Using the definitions, closure adjunction and symmetry, we have a series of natural bijections between the following homsets, involving the contravariant functor (-) \multimap R:

  • Morphisms A \multimap R \rightarrow B in \mathcal{V}^{op}
  • Morphisms B \rightarrow A \multimap R in \mathcal{V}
  • Morphisms B \otimes A \rightarrow R in \mathcal{V}
  • Morphisms A \otimes B \rightarrow R in \mathcal{V}
  • Morphisms A \rightarrow B \multimap R

These natural bijections establish that there is an adjunction:

(-) \multimap R : \mathcal{V} \rightarrow \mathcal{V}^{op} \dashv (-) \multimap R : \mathcal{V}^{op} \rightarrow \mathcal{V}

and therefore a monad on \mathcal{V}:

(((-) \multimap R) \multimap R, \eta, ((-) \multimap R) \circ \epsilon (-)  \circ ((-) \multimap R)

where \eta and \epsilon are the unit and counit of the adjunction. This monad is known as the continuation monad.

The Continuation Monad on Sets

To get a handle on what is going on, lets consider the special case where \mathcal{V} is the Cartesian closed category of sets and functions. The unit of the adjunction is then:

\eta(a)(f) = f(a)

and the counit is the same map, but in \mathsf{Set}^{op}. The multiplication of the monad at A is:

\mu(f )(g : A \Rightarrow R)) = f (\lambda h : (A \Rightarrow R) \Rightarrow R. h(g))

In the above, we’ve used lambda notation for inline functions, and added selected type annotations to emphasise how the input data is being used. Notice no copying or reuse of arguments takes place. This specific example lives in a Cartesian closed category, but the construction is inherently symmetric monoidal in nature, and therefore linear in its use of its arguments.

Kleisli Structure

A Kleisli morphism of type A \rightarrow B is a morphism in the underlying category of type A \rightarrow (B \multimap R) \multimap R. In the case of \mathsf{Set}, this is a function:

f : A \rightarrow (B \Rightarrow R) \Rightarrow R

From a computer science perspective, we can think of an element k : B \Rightarrow R as a continuation. This is how a computation should continue once it has computed a value of type B, eventually yielding a result of type R. An element g \in (B \Rightarrow R) \Rightarrow R is a computation yielding a B, that requires a continuation as a parameter, telling it how to continue to yield final result of type R.

Eilenberg-Moore Algebras

The Eilenberg-Moore algebras can be difficult to describe in the general case. We focus attention on a particular result. Consider the two element set 2 = \{ 0, 1 \}. The functor (-) \Rightarrow 2 : \mathsf{Set}^{op} \Rightarrow \mathsf{Set} is the contravariant powerset functor. An element \xi \in X \Rightarrow 2 can be seen a characteristic function, mapping elements appearing in a subset to 1, and the others to 0. This means that it has a left adjoint, as we already know, and their is an equivalent between the category of Eilenberg-Moore algebras, and \mathsf{Set}^{op}. Therefore, in this case:

\mathsf{Set}^{((-) \Rightarrow 2) \Rightarrow 2} \simeq \mathsf{Set}^{op}

It is well known (in the right circles!) that \mathsf{Set}^{op} is equivalent to the category \mathsf{CABA} of complete atomic Boolean algebras and morphisms preserving their joins and meets.

Remark: Notice there is a pronounced different here to considering complete Boolean algebras and their usual morphisms preserving the algebraic structure. In this case it is well known the forgetful functor to \mathsf{Set} does not have a left adjoint, as the free complete Boolean algebra on three generators does not exist. This is an instructive counterexample to the naive intuition that these algebraic constructions always “just work out”. Once you move beyond collection of operations of a fixed cardinality bound, you need to be much more careful.

A topos is a category rather similar to the category of sets and function, and \mathsf{Set} is probably the simplest example. Toposes are Cartesian closed, and have an object \Omega known as a subobject classifier, which can be thought of as a collection of truth values. The functor (-) \Rightarrow \Omega is the analog of the contravariant powerset functor on \mathsf{Set}, and again is monadic, so for any topos \mathcal{T}, we have a wide generalisation of the equivalence above:

\mathcal{T}^{((-) \Rightarrow \Omega) \Rightarrow \Omega} \simeq \mathcal{T}^{op}

This result is important for establishing finite completeness of toposes, via their finite completeness, and theory of Eilenberg-Moore categories.

Monad Morphisms and Algebras

We now turn to an interesting property of the continuation monad, that can be thought of as a very general representation result.

Consider a term in the algebraic theory of monoids, for example:

x_1 \times (x_2 \times x_3)

where x_1, x_2, x_3 come from some set X of variables. How can we evaluate this term in a particular monoid, say (R,\times,1)?

Firstly, we need to know what values to use for each variable, which we could specify via a function X \rightarrow R. Secondly, we really only need to specify the value for each equivalence class of terms, so the elements of \mathbb{L}(X), where \mathbb{L} is the free monoid (list) monad. So a crude first step is we need a function:

\mathbb{L}(X) \times (X \Rightarrow R) \rightarrow R

Given what we have seen in this post, it seems natural to rearrange this to emphasise the terms are the input, into the form:

\mathbb{L}(X) \rightarrow (X \Rightarrow R) \Rightarrow R

Obviously, the way we evaluate terms should not depend on which set we use to name the variables, so we expect this actually to be a family of maps, natural in X.

The algebraic structure also suggests that:

  1. The value for a term that is just a variable should be the value assigned to that variable.
  2. Evaluation should be compatible with substitution of terms.

These final two conditions correspond to the monad morphism axioms. So we are interested in monad morphisms of type

\mathbb{L} \rightarrow ((-) \Rightarrow R) \Rightarrow R

Obviously, there’s nothing special about our example of the list monad, so we’re really interested in monad morphisms of the form:

\mathbb{T} \rightarrow ((-) \Rightarrow R) \Rightarrow R

It turns out, there is a bijection between:

  1. Eilenberg-Moore algebra \alpha : \mathbb{T}(R) \rightarrow R.
  2. Monad morphisms \sigma : \mathbb{T} \rightarrow ((-) \Rightarrow R) \Rightarrow R

For \mathsf{Set} monads, the monad morphism resulting from an Eilenberg-Moore algebra has action:

\sigma(t)(k) = \alpha(\mathbb{T}(k)(t))

In the other direction, give a monad morphism, we get an Eilenberg-Moore algebra with action:

\alpha(t) = \sigma(t)(\mathsf{id}_{R})

In fact, this result goes through in much greater generality, but discussing the technical details would get distracting. Interested readers can refer to Kock’s “On Double Dualization Monads”.

This correspondence between algebras and monad morphisms opens up new possibilities. To see this, as a preliminary step, say that two monad morphisms:

  1. \sigma_1 : \mathbb{T}_1 \rightarrow \mathbb{S}
  2. \sigma_2 : \mathbb{T}_2 \rightarrow \mathbb{S}

commute if the following equality holds:

\mathsf{dst} \circ (\sigma_1 \otimes \sigma_2) = \mathsf{dst}' \circ (\sigma_1 \otimes \sigma_2)

where \mathsf{dst} and \mathsf{dst}' are the two double strength morphism. With this in place, we can say that two Eilenberg-Moore algebras \alpha_1 : \mathbb{T}_1(R) \rightarrow R and \alpha_2 : \mathbb{T}_2(R) \rightarrow R commute if their corresponding monad morphisms \mathbb{T}_i \rightarrow ((-) \multimap R) \multimap R commute as defined above. We then say an algebra is commutative if it commutes with itself.

This extends the notion of commutativity we have encountered previously in two directions:

  1. We consider commutativity for individual algebras, rather than for a monad as a whole.
  2. We can consider mixed forms of commutativity, for algebras of potentially different monads on the same base object.

We can also relate this form of commutativity with the previous definition. The following are equivalent for a monad \mathbb{T}.

  1. Every Eilenberg-Moore algebra is commutative.
  2. Every monad morphism with domain \mathbb{T} commutes with itself.
  3. The monad \mathbb{T} is commutative.

This theorem deepens our understanding of commutativity, allowing us to relate algebra-wise and monad-wise notions.

Conclusion

This post is relatively long. Despite this, we have only very briefly mentioned continuations, which are a fiddly topic in themselves. The continuation monad is an intriguing example of a monad, which can be hard to grasp as first sight. It is what is known as a monad without rank, which limits the scope of the algebraic techniques we have encountered previously.

Further reading: Johnstone’s “Stone Spaces” discusses the complete atomic Boolean algebra duality with \mathsf{Set}, and that the free complete Boolean algebra doesn’t exist. His “Sketches of an Elephant” gives a comprehensive account of topos theory, with the important monadicity theorem which we discussed appearing in the first volume.

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out /  Change )

Twitter picture

You are commenting using your Twitter account. Log Out /  Change )

Facebook photo

You are commenting using your Facebook account. Log Out /  Change )

Connecting to %s

%d bloggers like this: