In this post, we are going to return to the definition of a monad, but with a distinctly visual style. The starting point will be to use string diagrams, in the style of my book with Ralf Hinze (and it’s forthcoming sequel). As we are not restricted to the limitations of a paper book, we can go further, and explicitly show intuitions that are usually left implicit or described in accompanying text.
This post does not introduce a new mathematical notion. Instead we aim to use some new tools to convey the intuitions for ideas we already know.
AI Usage
Unlike all my usual posts, and my written work, the animations in this post were generated with the help of AI, using TikZ images I produced for my books with Ralf Hinze as key frames.
Monad in pictures and movies
For a monad
the unit axioms can be drawn using string diagrams as follows:
I like to think of equations such as these as as “freeze frames” showing the start and end points of a transition that is occurring across the equality. It then makes sense to directly apply this intuition, and show the equation as an animation as follows:
We can also draw the associativity axiom in string diagrams. In this diagrammatic format, it is useful to add a neutral intermediate trident shaped step.
Again, we can instead think of these equations as steps along a continuous journey across the equalities. That leads to the following:
Distributive laws in pictures and movies
So far, the diagrams and animations have only involved a single monad. For a pair of monads:
and a distributive law between them:
the required interaction between the two monads is given by four axioms, which can be drawn in string diagrams as follows:
The two unit axioms are the endpoints of dragging the unit of each monad across the functor wire of the other:
The two multiplication axioms have similar intuitions, allowing us to drag the multiplications across the functor wires of the other:
Combining monad associativity with the two distributive law multiplication axioms, the proof that the composite monad induced by a distributive law satisfies the associativity axiom becomes the following simple movie:
Summary
This post is mainly for fun, but I also think it is helpful to introduce new mechanisms that convey mathematical ideas in a form that is easy for humans to consume.
String diagrams have a lot of flexibility that we can use to make definitions and proofs easier to grasp. Many of the intuitions involve thinking of the proof steps in terms of motion or transitions, which immediately suggests the next step towards animated proofs.
