In this post, I’m going to introduce a very flexible graphical language that we can use to talk about many different kinds of type systems. This language consists of diagrams called “string diagrams.” Then I’ll use this to show how the monad laws correspond to the monoid laws, in a certain kind of setting (i.e. a category of endofunctors).

This graphical language makes few assumptions about the kind of programming language we’re using. For example, it makes copies and discards explicit, making it a natural language for talking about a linearly typed programming language. In fact, all three structural rules are visible:

• Copy (contraction): allowing you to use a variable multiple times
• Discard (weakening): allowing you to ignore a variable
• Swapping (exchange): allowing you to use variables in a different order than they’re listed

Here, a diagram will have inputs coming in on the left, and outputs going out on the right. These diagrams will correspond to expressions. An open expression will be a diagram which has inputs (as opposed to a closed expression, which has no inputs). The inputs will correspond to the free variables in the expression.

First, we will look at well-typed expressions in context. We will write these with a $\vdash$ (turnstile) separating the typing context (the list of in-scope variables and their types) and the expression that we’re looking at with its type. So, for example, $x : \mathsf{Nat}, y : \mathsf{Nat} \vdash x + y : \mathsf{Nat}$ is an expression that has two natural number free variables and adds them together to get another $\mathsf{Nat}$.

We can draw the expression

$x : \mathsf{Nat}, y : \mathsf{Nat}, z : \mathsf{Nat} \vdash x + (y \times z) : \mathsf{Nat}$

as the diagram:

The input wires, going top to bottom, are the context’s variables in order.

Note that you can think of an entire diagram as being a single box, where the input ports are the inputs to the diagram and the output ports are the outputs of the diagram. This allows you to think compositionally about diagrams, breaking them into smaller pieces. Substitution corresponds to wiring two diagrams together. For example, that adding-and-multiplying example from earlier could be thought of as taking the expression $a : \mathsf{Nat}, b : \mathsf{Nat} \vdash a + b : \mathsf{Nat}$ and substituting in the expression $y : \mathsf{Nat}, z : \mathsf{Nat} \vdash y \times z : \mathsf{Nat}$ for the variable $b$. This corresponds to wiring the diagram for addition to the diagram for multiplication in the way shown in the figure above. As wires do not need names, this gives us something a little bit like de Bruijn indices but without needing to deal with actual numbers.

More technically, this is a category where boxes/diagrams (morphisms) are well-typed expressions (and morphisms between contexts), and wires are types (and “stacks” of wires are typing contexts). Composition is substitution of expressions. In particular, it is a monoidal category which gives you a “tensor product.” This tensor product is exactly what allows us to do vertical juxtaposition in the graphical language (i.e. it gives us typing contexts). A tensor product in a monoidal category is usually written as $\otimes$.

Now, let’s see what the structural rules look like visually. For example, the weakened expression $x : \mathsf{Nat}, y : \mathsf{Nat} \vdash x + 1 : \mathsf{Nat}$ looks like:

The expression $x : \mathsf{Nat} \vdash x \times x : \mathsf{Nat}$, which uses contraction, looks like:

And finally, exchange corresponds to allowing wire crossings. For example, the expression $x : \mathsf{Nat}, y : \mathsf{Nat}, z : \mathsf{Nat} \vdash y - (x + z) : \mathsf{Nat}$, which uses exchange, looks like:

While the diagrams we’ve seen so far have only one output, a diagram can also have multiple outputs. This corresponds to a tuple of expressions (i.e. a morphism between contexts).

Monoids

A monoid is a mathematical structure representing things that are, in some sense, “combinable.” It consists of a set $M$ together with an element of $M$, called the unit, and a binary operation on $M$ for combining two $M$ elements (often called the “multiplication” of the monoid), along with three laws. We can draw these laws as equations between diagrams. There are many examples of monoids, including natural numbers with addition, natural numbers with multiplication, lists with concatenation, and many more. For concreteness, we will look at the laws in terms of list concatenation.

Two of the laws say that combining any $x$ in $M$ with the unit just gives back $x$ unchanged:

Writing symbolically, these say that the expressions $x : \mathsf{List}\; a \vdash [] \mathbin{++} x : \mathsf{List}\;a$ and $x : \mathsf{List}\;a \vdash x \mathbin{++} [] : \mathsf{List}\; a$ are both equal to the expression $x : \mathsf{List}\;a \vdash x : \mathsf{List}\;a$.

The remaining law says that if we want to combine three things, it does not matter which two we combine first:

More generally, you can have a monoid in any monoidal category. We take an object $M$, a unit $I \to M$ (where $I$ is the unit of the tensor product), and a multiplication $M \otimes M \to M$.

Categories of endofunctors

Let’s now consider endofunctors on our category of types, such as those given by the Functor type class in Haskell. We can actually think of a category of endofunctors using this sort of graphical language! Our wires will be endofunctors and our boxes will be natural transformations between them. Our “typing contexts” will consist of a composition of endofunctors. In our original category, the “empty tensor product” was given by the empty product (the unit type). Here, the empty tensor product is given by the identity functor, as this is the unit for functor composition. So, a natural transformation $\alpha : \mathsf{Id} \to F$ will be drawn as having no input.

Does it make sense to think of endofunctor composition as being like context concatenation? Well, we need to be able to take some natural transformation $\alpha : F \to G$ and put it above some other natural transformation $\beta : H \to K$ to get something that takes $F \circ H$ and gives back $G \circ K$. We will follow the convention that the top wire corresponds to the outermost functor layer.

We can also see that this composition is associative. That means we are able to think of it as giving a kind of “typing context.” But, unlike our language from the first section, note that we actually do not have any of the structural rules (not even exchange)! In general:

• We cannot duplicate a functor layer
• We cannot discard a functor layer
• We cannot swap functor layers

The language in the first section has all the structural rules, because it is a Cartesian monoidal category. This means that its monoidal product is exactly the categorical product (i.e. product types).

But, we are still able to talk about such a language just fine in this graphical language. The fmap operation (the functor’s action on morphisms) lets us take a natural transformation and move it “under” one functor layer. Here’s an example of that:

The $H$ layer remains unchanged, while the $F$ layer gets $\alpha$ applied to it to obtain $G$.

Let’s return to our simple example of monoids. Let’s go ahead and draw them as they appear in this category:

In Haskell terms, these laws are:

• join . pure = id
• join . fmap pure = id
• join . join = join . fmap join

Now look at the diagrams. Note that these laws are exactly the laws for a monoid! The diagrams are visually identical to the monoid laws from the previous section, except for the labels. A monad is, very literally, a monoid in a category of endofunctors. We obtain the definition of monad just by writing the laws for monoids down as they appear in a category of endofunctors, using functor composition as our “context concatenation” operation for our “typing contexts.”

Much like in the case of monoids in our category from the first section, the monad laws say: $\mathsf{pure}$ is the unit for $\mathsf{join}$, and if we combine (join) three functor layers, it doesn’t matter which two layers we join first.

Conclusion

We first learned about string diagrams, and then applied them to a simple programming language. Then, we used the same kinds of diagrams to describe pieces of the category of endofunctors. The payoff was that the monad laws are the monoid laws, drawn with endofunctors as wires and functor composition as vertical stacking. So, we saw that a monad really is a monoid in a category of endofunctors.

Later, I plan to give more examples of monoidal categories and to explore the duals of the structural rules: coweakening and cocontraction. If we have the structural rules and their duals in a “compatible” way, they form what’s called a “special commutative Frobenius algebra,” which allows us to create “junctions” with many inputs and many outputs. These junctions are sometimes called “spiders.” One example of a monoidal category which has this is $\mathsf{Rel}$, the category of sets and relations.

Further reading

• “Introducing String Diagrams” by Hinze and Marsden
• “Picturing Quantum Processes” by Coecke and Kissinger