The n-Category Café

Take a look at this Agda-style¹ definition of an algebraic datatype, a structure. $$\begin{aligned} {\color{#CD6600} data} \:& {\color{#0000CD} Expr}\::\:{\color{#0000CD} Set}\:{\color{#CD6600}where}\\ & {\color{#008B00} lit} : \mathbb{N} \to {\color{#0000CD} Expr}\\ & {\color{#008B00} add} : {\color{#0000CD} Expr} \times {\color{#0000CD} Expr} \to {\color{#0000CD} Expr}\\ & {\color{#008B00} mul} : {\color{#0000CD} Expr} \times {\color{#0000CD} Expr} \to {\color{#0000CD} Expr} \end{aligned}$$ The intention of the programmer is to define datatype ${\color{#0000CD} Expr}$ that can be constructed in exactly three ways. One can either apply a natural number to the function ${\color{#008B00} lit}$ (for “literal”), find a pair of ${\color{#0000CD} Expr}$s and apply them to the function ${\color{#008B00} add}$, or do the same thing to ${\color{#008B00} mul}$. In fact, ${\color{#0000CD} Expr}$ is defined precisely in terms of these three functions, which we call constructors, and it is the least such set whose building blocks are ${\color{#008B00} lit}$, ${\color{#008B00} mul}$ and ${\color{#008B00} add}$. In the end, ${\color{#0000CD} Expr}$ consists of expressions such as “${\color{#008B00} add}$ (${\color{#008B00} lit}$ 5) (${\color{#008B00} mul}$ (${\color{#008B00} lit}$ 4) (${\color{#008B00} lit}$ 2))”, “${\color{#008B00} lit}$ 0” and so on.

Such datatypes are not the only ones we can define in functional languages such as Agda. The dual notion is that of a record or a class. Well, here’s a classic. $$\begin{aligned} {\color{#CD6600} record}\:& {\color{#0000CD} Stream}\::\:{\color{#0000CD} Set}\:{\color{#CD6600}where}\\ & {\color{#CD6600} field} \\ & {\color{#EE1289} head} : \mathbb{N} \\ & {\color{#EE1289} next} : {\color{#0000CD} Stream}\\ \end{aligned}$$ ${\color{#0000CD} Stream}$ is a datatype, like ${\color{#0000CD} Expr}$ before. In fact, ${\color{#0000CD} Stream}$ is the set of all infinite sequences of natural numbers only in this case functions ${\color{#EE1289} head}$ and ${\color{#EE1289} next}$ do not represent ways to construct a ${\color{#0000CD} Stream}$ instance. Rather, they show the exact opposite, so they are destructors for a ${\color{#0000CD} Stream}$! Perhaps a more accurate representation would be something akin to $$\begin{aligned} {\color{#CD6600} record}\:& {\color{#0000CD} Stream}\::\:{\color{#0000CD} Set}\:{\color{#CD6600}where}\\ & {\color{#CD6600} field} \\ & {\color{#EE1289} head} : {\color{#0000CD} Stream} \to \mathbb{N} \\ & {\color{#EE1289} next} : {\color{#0000CD} Stream} \to {\color{#0000CD} Stream}\\ \end{aligned}$$

By saying “destructor”, the idea is that a ${\color{#0000CD} Stream}$ can be applied to either ${\color{#EE1289} head}$ or ${\color{#EE1289} next}$ to get a natural number or another ${\color{#0000CD} Stream}$ respectively. Hence, destructors are different when compared to constructors in that they are not used to build an instance of a datatype out of a number of ingredients, but to pick it apart and present the observations that one can make out of it. In the case of ${\color{#0000CD} Stream}$, i.e. infinite sequences of natural numbers, we can always observe the ${\color{#EE1289} head}$, the number at the current position in the stream, and move on to observe the rest of the ${\color{#0000CD} Stream}$ (i.e. observing the ${\color{#EE1289} next}$ ${\color{#0000CD} Stream}$), to repeat the process.

We can witness the first traces of a duality by comparing the codomains of constructors with the domains of destructors. At one end, constructors all map to the same thing, ${\color{#0000CD} Expr}$, while all destructors map from the same thing, ${\color{#0000CD} Stream}$. But the antitheses do not end here as, interestingly, instances of ${\color{#0000CD} Expr}$ and ${\color{#0000CD} Stream}$ are meant to be used in radically different ways.

Let us define a simple function that “calculates” the value of an ${\color{#0000CD} Expr}$ expression. In this case we want to define a function such that “${\color{#008B00} add}$ (${\color{#008B00} lit}$ 5) (${\color{#008B00} mul}$ (${\color{#008B00} lit}$ 4) (${\color{#008B00} lit}$ 2))” amounts to 13 or that “${\color{#008B00} lit}$ 0” amounts to 0. This is simple enough. $$\begin{aligned} & {\color{#0000CD} calc} : {\color{#0000CD} Expr} \to \mathbb{Z} \\ & {\color{#008B00} lit}\:n \mapsto n \\ & {\color{#008B00} add}\:(l,r) \mapsto ({\color{#0000CD} calc}\:l) + ({\color{#0000CD} calc}\:r)\\ & {\color{#008B00} mul}\:(l,r) \mapsto ({\color{#0000CD} calc}\:l) * ({\color{#0000CD} calc}\:r) \end{aligned}$$

${\color{#0000CD} calc}$ is an example of a simple inductive definition. The key is that it composes values of smaller sub-${\color{#0000CD} Expr}$essions to specify the result of the whole ${\color{#0000CD} Expr}$ession. “Composition” is a rather fitting word here, as the definition of ${\color{#0000CD} calc}$ is essentially a recipe on how to mix ${\color{#0000CD} Expr}$essions together. Now, how about a small dose of un-mixing? $$\begin{aligned} & {\color{#0000CD} zip} : {\color{#0000CD} Stream} \times {\color{#0000CD} Stream} \to {\color{#0000CD} Stream} \\ & {\color{#EE1289} head}\:({\color{#0000CD} zip}\:(l,r)) = {\color{#EE1289} head}\:l \\ & {\color{#EE1289} next}\:({\color{#0000CD} zip}\:(l,r)) = {\color{#0000CD} zip}\:(r, {\color{#EE1289} next}\:l) \end{aligned}$$

Our new function ${\color{#0000CD} zip}$ takes apart two ${\color{#0000CD} Stream}$s by specifying, at each given step, how to (i) extract a natural number and (ii) extract a new ${\color{#0000CD} Stream}$ out of them. The end result is that of a coinductive definition. Notice how ${\color{#0000CD} zip}$ maps onto ${\color{#0000CD} Stream}$s and compare it to ${\color{#0000CD} calc}$ that maps from ${\color{#0000CD} Expr}$s. Once again, the arrows are reversed. Strange.

Let’s forget about that mystery for a second and try out a couple of proofs. For starters, notice that ${\color{#0000CD} calc}$ maps all elements of ${\color{#0000CD} Expr}$ to positive integers. This is a property that we can prove inductively.

$$\begin{aligned} & {\color{#0000CD} prop}\: : \forall\:(e : {\color{#0000CD} Expr}) \to {\color{#0000CD} calc}\:e \geq 0 \\ & {\color{#0000CD} prop}\:(lit\:n) = true\:as\:n \geq 0 \\ & {\color{#0000CD} prop}\:({\color{#008B00} add}\:l\:r) = {\color{#008B00} true}\:as\:{\color{#0000CD} prop}\:l\:\wedge\:{\color{#0000CD} prop}\:r\\ & \:\:\:\:\:\:\:\:\:\:\:\:\wedge\:{\color{#0000CD} calc}\:({\color{#008B00} add}\:l\:r) = {\color{#0000CD} calc}\:l + {\color{#0000CD} calc}\:r\\ & {\color{#0000CD} prop}\:({\color{#008B00} mul}\:l\:r) = {\color{#008B00} true}\:as\:{\color{#0000CD} prop}\:l\:\wedge\:{\color{#0000CD} prop}\:r \\ & \:\:\:\:\:\:\:\:\:\:\:\:\wedge\:{\color{#0000CD} calc}\:({\color{#008B00} mul}\:l\:r) = {\color{#0000CD} calc\:l} \cdot {\color{#0000CD} calc\:r} \end{aligned}$$ The above is an example of a mechanized Agda proof written in a mathematician-friendly way. We encode the fact that ${\color{#0000CD} calc}$ produces positive values as property/function ${\color{#0000CD} prop}$. A valid proof requires ${\color{#0000CD} prop}$ being true for each of the constructors of ${\color{#0000CD} Expr}$, which is trivial for ${\color{#008B00} lit}$ and slightly more involved for ${\color{#008B00} add}$ and ${\color{#008B00} mul}$. In the latter two cases we invoke the induction hypothesis on both operands, which translates to two nested calls to ${\color{#0000CD} prop}$.

The above proof is an example of the so-called Curry-Howard correspondence, relating mathematical proofs with programs written in typed functional languages. The main aspects of it are the fact that propositions can be encoded as types (first line of the proof) and proofs as definitions. Indeed, ${\color{#0000CD} prop}$ is simply a function that we are giving a definition for.

Now let’s try something similar for ${\color{#0000CD} Stream}$. First, we define function even that only picks positions $0,2,4,\dots$ from a ${\color{#0000CD} Stream}$. $$\begin{aligned} & {\color{#0000CD} even} : {\color{#0000CD} Stream} \to {\color{#0000CD} Stream} \\ & {\color{#EE1289} head}\:({\color{#0000CD} even}\:xs) = {\color{#EE1289} head}\:xs \\ & {\color{#EE1289} next}\:({\color{#0000CD} even}\:xs) = {\color{#0000CD} even}\:({\color{#EE1289} next}\:({\color{#EE1289} next}\:xs)) \end{aligned}$$

If we “double” a ${\color{#0000CD} Stream}$ $xs$ (as in ${\color{#0000CD} zip}\:(xs , xs)$) and apply the result to ${\color{#0000CD} even}$, we will obviously recover the original ${\color{#0000CD} Stream}$ $xs$. We once again write down the proof, only this time it is coinductive. $$\begin{aligned} & {\color{#0000CD} prop2} : \forall\:(xs : {\color{#0000CD} Stream}) \to {\color{#0000CD} even}\:({\color{#0000CD} zip}\:(xs , xs)) \equiv xs \\ & {\color{#EE1289} head}\:({\color{#0000CD} even}\:({\color{#0000CD} zip}\:(xs , xs))) \equiv {\color{#EE1289} head}\:xs\:&& (1)\\ & {\color{#EE1289} next}\:({\color{#0000CD} even}\:({\color{#0000CD} zip}\:(xs , xs))) \equiv {\color{#EE1289} next}\:xs\:as\:\\ & \:\:\:\:\:\:\:\:\:\:\:\:{\color{#EE1289} next}\:({\color{#0000CD} even}\:({\color{#0000CD} zip}\:(xs , xs))) \equiv {\color{#0000CD} even}\:({\color{#0000CD} zip}\:({\color{#EE1289} next}\:xs , {\color{#EE1289} next}\:xs))) && (2) \\ & \:\:\:\:\:\:\:\:\:\:\:\:{\color{#0000CD} even}\:({\color{#0000CD} zip}\:({\color{#EE1289} next}\:xs , {\color{#EE1289} next}\:xs))) \equiv {\color{#EE1289} next}\:xs && (3) \end{aligned}$$ where (1) and (2) are true by definition of ${\color{#0000CD} even}$ and ${\color{#0000CD} zip}$ and (3) is obtained via coinduction on ${\color{#EE1289} next}$ $xs$.

The proof essentially asserts that both the ${\color{#EE1289} head}$ and the ${\color{#EE1289} next}$ part of the two streams in question are identical. If we look closely, we can observe the subtle “structural” differences between ${\color{#0000CD} prop}$ and ${\color{#0000CD} prop2}$: in the case of the former, we had to provide a valid proof for each ${\color{#0000CD} Expr}$ constructor, while in the latter case, we had to provide a valid proof of equivalence for each ${\color{#0000CD} Stream}$ destructor! What’s going on here?

Constructors and destructors, induction and coinduction, composition and decomposition are all elements of a duality that transcends functional programming going all the way up to the very foundations of thought: It’s the duality of structure vs observation. And it is a duality that universal (co)algebra gives a very satisfying account for.

The Category Theory Within

We’ll now give a brief overview of the main building blocks of universal (co)algebra. Along the way, we will revisit our Agda examples in order to see how this simple and rather abstract theory can be used in concrete situations.

Given endofunctors $T, F: \mathbf{Set} \rightarrow \mathbf{Set}$², a $T$-algebra $(S, a_{S})$ consists of a set $S$ together with a function $a_{S}: T(S) \rightarrow S$. Dually, an $F$-coalgebra $(X, \alpha_X)$ consists of a set $X$ together with a function $\alpha_X: X \rightarrow F(X)$. We’ve already encountered examples of both algebras and coalgebras:

1. Consider the endofunctor $E$ which maps a set $U$ to $Ex(U) = N + (U \times U) + (U \times U)$, and a function $f$ to $Ex(f) = id_{N} + (f \times f) + (f \times f)$. Then, $({\color{#0000CD} Expr}, {\color{#008B00} lit} + {\color{#008B00} add} + {\color{#008B00} mul})$ is an $E$-algebra.
2. Consider the endofunctor $S$ which maps a set $X$ to $S(X) = N \times X$, and a function $f$ to $S(f) = id_{N} \times f$. Then, $({\color{#0000CD} Stream}, ({\color{#EE1289} head}, {\color{#EE1289} next}))$ is an $S$-coalgebra.

A $T$-algebra homomorphism between two $T$-algebras $(U, a_U), (V, a_V)$ is any function $f:U \rightarrow V$ where $a_V \circ T(f) = f \circ a_U$. Dually, an $F$-coalgebra homomorphism between two $F$-algebras $(X, \alpha_X), (Y, \alpha_Y)$ is any function $f:X \rightarrow Y$ where $\alpha_Y \circ f = F(f) \circ \alpha_X$. In terms of commuting diagrams these conditions amount to:

Once again, we’ve already seen examples of both algebra and coalgebra homomorphisms:

1. ${\color{#0000CD} calc}$ is an $E$-algebra homomorphism.
2. ${\color{#0000CD} zip}$ is an $S$-coalgebra homomorphism.

We leave it to the reader to check the commutativity conditions for these homomorphisms, which are summarised in the diagrams below:

The function ${\color{#0000CD} zipStep}$ above is defined as ${\color{#0000CD} zipStep}\:(l, r) = ({\color{#EE1289} head}\:l, (r, {\color{#EE1289} next}\:l))$. If we keep use zipStep according to the (pseudo)-agda style code below we can recover the behaviour of ${\color{#0000CD} zip}$.

$$\begin{aligned} & {\color{#0000CD} altZip} : {\color{#0000CD} Stream} \times {\color{#0000CD} Stream} \to {\color{#0000CD} Stream} \\ & {\color{#EE1289} head}\:({\color{#0000CD} altZip}\:(l,r)) = lHead \\ & {\color{#EE1289} next}\:({\color{#0000CD} altZip}\:(l,r)) = {\color{#0000CD} altZip}\:(r, lNext) \\ & \:\:{\color{#CD6600}where}\\ & \:\:\:\: lHead\:r\:nextL = {\color{#0000CD} altZip}\:(l,r) \end{aligned}$$

So ${\color{#0000CD} zipStep}$ is in a sense equivalent to a single step of the ${\color{#0000CD} zip}$ function. This is not a coincidence! We’ll return to this point shortly when we talk about coinduction.

$T$-algebras and algebra homomorphisms form a category. We refer to an initial object of this category as an initial algebra. Dually, $F$-coalgebras and coalgebra homomorphisms form a category whose final objects we refer to as final coalgebras. Initiality and finality occupy a central role in universal (co)algebra. This is what we explore next.

Take an initial $T$-algebra $(A, a_a)$ together with an arbitrary $T$-algebra $(U, a_u)$. By initiality, there exists a unique $T$-algebra homomorphism $f: A \rightarrow S$. We say that such a function $f$ is inductively defined. Intuitively, an inductive function $f$ breaks complicated elements of $A$ down into their constituent parts, applies some function on each constituent part, and mixes the results together to obtain an action on the whole element. If you’re an eagle eyed reader you’ll know that we’ve already encountered a function that behaves this way. Remember how ${\color{#0000CD} calc}$ breaks complicated ${\color{#0000CD} Expr}$s down into smaller sub-${\color{#0000CD} Expr}$s and mixes their results together to get a result for the whole ${\color{#0000CD} Expr}$? Well now we know that this behaviour is indicative of the fact that ${\color{#0000CD} calc}$ is inductively defined (note that in this case ${\color{#0000CD} Expr}$ is an initial $T$-algebra³).

Now consider the dual scenario where we have a final $F$-coalgebra $(Z, \alpha_Z)$ together with an arbitrary $F$-coalgebra $(Y, \alpha_Y)$. By universality there must be a unique coalgebra homomorphism $g:Y \rightarrow Z$. We call such a function g coinductively defined. A nice intuition here is to think of $(Y, \alpha_Y)$ as a dynamic system evolving according to the transition structure given by $\alpha_Y$, then the function $g$ is the result of applying the transition $\alpha_Y$ over and over again. Repeated application of a transition structure might sound awfully familiar to you, as in fact it should. We were only just talking about how ${\color{#0000CD} zip}$ can be thought of as repeated applications of ${\color{#0000CD} zipStep}$. Again, this is indicative of the fact that ${\color{#0000CD} zip}$ is a coinductive definition, and that ${\color{#0000CD} Stream}$ is a final coalgebra.

With that our whirlwind tour comes to a close. We’ve seen how universal algebra gives us tools for exploring the structure of things, while universal coalgebra allows us to explore their behaviour. Together they gave us a way to rigorously analyse the duality between structure and behaviour. Earlier in the article we made the rather bold claim that this duality transcends the examples we’ve seen here and goes up all the way to the foundations of thought. We’ll end on a similarly dramatic note by giving you a philosophical question to ponder:

Is a “thing” best defined by its constituent parts (structure) or by its observable actions(behaviour).

Further Reading

If you’re interested in learning more there’s many facets of the structure vs behaviour duality that we didn’t have space to talk about. Things like congruence vs bisimulation, minimality vs simplicity, and freeness vs cofreeness. A good starting point for further reading is the paper which motivated this blog post, Universal Coalgebra: a theory of systems. In this classic work the author introduces universal coalgebra as an abstract theory for capturing the behaviour of a wide class of dynamic systems⁴. Even though it is a fantastic introduction to universal coalgebra the focus on duality in this article is arguably limited. A paper that does extensively cover duality is An introduction to (co)algebra and (co)induction. This is also a great article for readers who may be newer to category theory as the material is presented in set-theoretic language whenever possible. Much of the material from both these papers is now available as part of an introductory book on coalgebras. Finally, since our examples focused on functional programming we mention that chapter 24 of Category Theory for Programmers gives a nice account of how (co)algebras are used in the functional programming language Haskell.

1 Agda is a functional programming language often used as a theorem prover. ↩

2 This definition can easily be generalised to endofunctors on an arbitrary category $\mathcal{C}$.↩

3 Proving this fact directly is a rather fun excercise that we leave for the reader. Hint: First build up a homomorphism $f$ from ${\color{#0000CD} Expr}$ into an arbitrary $Ex$-algebra by considering where $f$ could send elements such as ${\color{#008B00} lit}$ 0 or add (${\color{#008B00} mul}$ 5) (${\color{#008B00} mul}$ (${\color{#008B00} mul}$ 4) (${\color{#008B00} lit}$ 2)) to in the target set. Then assume for the sake of contradiction that $f$ is not unique, i.e. send some of the objects to a different place in the target set. You should be able to show that this new function breaks the algebra homomorphism commutativity conditions. Once you’ve proven this have a go at showing that ${\color{#0000CD} Stream}$ is a final coalgebra.↩

4 These so-called dynamic systems are by no means limited to the functional programming examples in this blog post. In fact, the main appeal of universal coalgebra comes from the omni-presence of dynamic systems around us. Labelled transition systems, finite automata, Kripke models arising in modal logic, And even the evolution of quantum systems are just a few examples of such systems.↩