Coproducts of Monads

Often the simplest way to form a combination of two objects in category theory is to take their coproduct. In this post, we are going to investigate coproduct of monads, beginning as usual from an algebraic perspective.

Sums of Theories

We begin by considering a pair of $\mathsf{Set}$ -monads given by equational presentations. We shall investigate how a suitable method of combining those presentations yields a corresponding operation on monads.

Given two equational presentations, $(\Sigma_1, E_1)$ and $(\Sigma_2, E_2)$ , we can define a new equational presentation with:

Operations the disjoint union $\Sigma_1 \uplus \Sigma_2$ .
Equations given by the union $E_1 \cup E_2$ .

We shall refer to this as the sum $(\Sigma_1, E_1) + (\Sigma_2, E_2)$ of the two component theories.

This combines the two equational theories such that there is “no interaction between them”. This can be seen by considering the algebras of the resulting theory. An algebra for $(\Sigma_1, E_1) + (\Sigma_2, E_2)$ consists of

A fixed choice of universe $A$ .
A $(\Sigma_1, E_1)$ -algebra structure on $A$ .
A $(\Sigma_2, E_2)$ -algebra structure on $A$ .

The sum of theories induces an operation $\mathbb{T}_1 \oplus \mathbb{T}_2$ on the monads induced by these equational presentations. In fact, the resulting monad is the coproduct of $\mathbb{T}_1$ and $\mathbb{T}_2$ .

Coproducts of Free Monads

Forming coproducts of monads via an operation on their algebraic presentations as we have just described has some limitations. In particular:

To exploit it, we need to identify presentations for our monads of interest.
We don’t get a description of the monad $\mathbb{T}_1 \oplus \mathbb{T}_2$ directly in terms of the component monads $\mathbb{T}_1$ and $\mathbb{T}_2$ .
Realistic applications will probably involve categories other that $\mathsf{Set}$ . We would prefer constructions that generalise smoothly to other settings.

To address some of these problems, we shall begin by examining the simple case of coproducts of free monads. For a pair of signatures $\Sigma_1$ and $\Sigma_2$ , the free monads for the corresponding signature functors must satisfy:

$\Sigma_1^* \oplus \Sigma_2^* \cong (\Sigma_1 + \Sigma_2)^*$

This follows immediately from the universal property, or via a simple direct calculation. We then recall that free monads can be constructed using least fixed points, so we have:

$(\Sigma_1^* \oplus \Sigma_2^*)(X) \cong \mu Z. X + \Sigma_1(Z) + \Sigma_2(Z)$

We can think of this as building the coproduct in stages. In the first stage, we begin with the set of variables $X$ . In subsequent stages, we:

Apply every operation symbol in $\Sigma_1$ to terms constructed in the previous stage.
Apply every operation symbol in $\Sigma_2$ to terms constructed in the previous stage.
Add back in the set of variables $X$ again.

Example: Let $\Sigma_1$ and $\Sigma_2$ both contain a single unary operation symbol, $\sigma_1$ and $\sigma_2$ respectively. The terms over set of variables $\{ x \}$ will be:

$x$ .
$x, \sigma_1(x), \sigma_2(x)$ .
$x, \sigma_1(x), \sigma_2(x), \sigma_1(\sigma_1(x)), \sigma_2(\sigma_2(x)), \sigma_1(\sigma_2(x)), \sigma_2(\sigma_1(x))$
…

This lets us build up the elements of the coproduct of free monads, using the underlying signature functor. This is a step in the right direction, but ideally we would use the monads themselves in the construction. To try and achieve this, we notice that each term consists of layers of operations from one signature, followed by layers of operations from the other signature, eventually applied to variable symbols.

Example: Continuing the previous example, we end up with terms like:

$\sigma_2(\sigma_2(\sigma_1(x))$

We can see this as a layer of two $\Sigma_2$ operations, followed by a layer with one $\Sigma_1$ operation applied to a variable.

Can we build up these layers directly, using the free monads $\Sigma^*_1$ and $\Sigma^*_2$ ? A naive first attempt would be to try the fixed point construction:

$\mu Z. X + \Sigma^*_1(Z) + \Sigma^*_2(Z)$

If we consider the first few approximants to this fixed point, we get:

$X + \Sigma_1^*(\emptyset) + \Sigma_2^*(\emptyset)$ .
$X + \Sigma_1^*(X + \Sigma_1^*(\emptyset) + \Sigma_2^*(\emptyset)) + \Sigma_2^*(X + \Sigma_1^*(\emptyset) + \Sigma_2^*(\emptyset))$ .
…

This is not quite what we want. For example, $\Sigma_1^*(X + \Sigma_1^*(\emptyset) + \Sigma_2^*(\emptyset))$ will contain a copy of the variables. So we are going to end up with two many copies of the variables in our fixed point. Intuitively, $\Sigma_1^*(X)$ muddles together both bare variables and non-trivial terms.

Hopefully this rings a bell. We have previously seen that free monads are ideal monads. Recall that an ideal monad abstracts the idea of “keeping variables separate”. An ideal monad $\mathbb{T}$ has a subfunctor $\mathbb{T}'$ such that:

$\mathbb{T}(X) \cong X + \mathbb{T}'(X)$

In the case of free monads ${\Sigma^{*}}'(X)$ contains all the guarded terms. These are exactly the terms that are not bare variables. As a second attempt at a fixed point construction, we consider

$\mu Z. X + {\Sigma^*}'_1(Z) + {\Sigma^*}'_2(Z)$

Unfortunately, this is still not quite right. The first few approximants to this fixed point are:

$X + {\Sigma^*}'_1(\emptyset) + {\Sigma^*}'_2(\emptyset)$ .
$X + {\Sigma^*}'_1(X + {\Sigma^*}'_1(\emptyset) + {\Sigma^*}'_2(\emptyset)) + {\Sigma^*}'_2(X + {\Sigma^*}'_1(\emptyset) + {\Sigma^*}'_2(\emptyset))$ .
…

The problem now is that this construction will build up some terms in more than one way, resulting in redundant duplicate copies.

Example: Continuing our previous example, we can consider $\sigma_1(\sigma_1(x))$ as arising either directly as a term in ${\Sigma^*}'_1(X)$ , or in two steps by applying ${\Sigma^*}'_1$ to ${\Sigma^*}'_1(X)$ , by applying $\sigma_1$ to $\sigma_1(x)$ .

To address this, we must be more careful to build up terms in alternating layers of operations from each signature, in a unique way. To achieve this explicit alternation, we instead solve a fixed point equation in two variables:

$(\Sigma^\dagger_1(X), \Sigma^\dagger_2(X)) = \mu (Z_1, Z_2). ({\Sigma^*}'_1(X + Z_2),{\Sigma^*}'_2(X + Z_1))$

This will produce terms with alternating layers of operations from the two signatures. $\Sigma^\dagger_1(X)$ will contain terms with a $\Sigma_1$ operation on top, and dually for $\Sigma^\dagger_2$ . We then recover:

$(\Sigma_1^* \oplus \Sigma_2^*)(X) \cong X + \Sigma^\dagger_1(X) + \Sigma^\dagger_2(X)$

Coproducts of Ideal Monads

So far, we have rearranged the construction of a coproduct of free monads into language which involves fixed points. Has all this reshuffling got us anywhere?

Well we could consider applying the same construction to arbitrary ideal monads. Firstly, we calculate the fixed point:

$(\mathbb{T}^\dagger_1(X), \mathbb{T}^\dagger_2(X)) = \mu (Z_1, Z_2). (\mathbb{T}'_1(X + Z_2), \mathbb{T}'_2(X + Z_1))$

Assuming the required fixed points exist, we can then form the coproduct as:

$(\mathbb{T}_1 \oplus \mathbb{T}_2)(X) \cong X + \mathbb{T}^\dagger_1(X) + \mathbb{T}^\dagger_2(X)$

It is worth considering what this says. Firstly, from the algebraic perspective we’re now building up equivalence classes of terms under provable equality, not just raw terms. The intuitive reason that this construction works is that the layers cannot interact. We can prove equalities within a layer, but once a layer of terms from the other theory is inserted, this layer is insulated from interacting with anything else. Hence, we can build up the equivalence classes of $\mathbb{T}_1 \oplus \mathbb{T}_2$ , not just the underlying terms, inductively in layers, which is rather a pleasing outcome.

In fact, this is true for arbitrary categories and ideal monads, as long as the required fixed points exist. For example, we can also apply this result to the completely iterative monads that we saw previously.

Summing Up

The ideas in this post mainly follows Ghani and Uustalu’s “Coproducts of Ideal Monads”, which is strongly recommended for further reading. There are other explicit constructions for coproducts of comonads, for example in the case of a free monad and an arbitrary monad, as described in Hyland, Plotkin and Power’s “Combining Effects: Sum and Tensor”. “Coproducts of Monads on Set” by Adámek, Milius, Bowler and Levy gives a detailed analysis in the case of $\mathsf{Set}$ -monads. We should also point out that even in the case of $\mathsf{Set}$ -monads, coproducts of pairs of monads do not always exist.

Sums of Theories

Coproducts of Free Monads

Coproducts of Ideal Monads

Summing Up

Share this:

Like this:

Related

Leave a Reply Cancel reply