The title of this post is a common sort of remark that is made about monads. Similar examples might be:
- The multiset monad is the free commutative monoid monad.
- The finite powerset monad is the free join semilattice monad.
Sorting out what statements such as these mean is our current purpose. In order to do so, we need to admit to being a little bit naughty up until now. Any good category theory book or course will quickly tell you that it is important not to just consider mathematical structures, but also the transformations between them. In the earlier posts, there was a lot of discussion of monads, but no mention of what the morphisms between them might be. Without pinning this down, we cannot compare monads in any meaningful way.
Monad Morphisms
There are actually a few choices for maps between monads. We shall consider the simplest case, morphisms between monads over some fixed base category . More complex notions of transformation of monads are also useful, and tend to form 2-categories rather than mere categories. We shall return to this topic again later.
A monad morphism is a natural transformation between the underlying endofunctors
satisfying two axioms:
- Unit axiom:
.
- Multiplication axiom:
.
We mentioned in an earlier post that a monad can be seen as a monoid in a precise sense. From that point of view, monad morphisms are exactly monoid morphisms. Again, we shall avoid getting into the details of these statements. For now, it is sufficient to think of a monad morphism as a natural transformation between the underlying endofunctors that interacts well with the additional monad structure.
Example: For any monad , the monad unit is a monad morphism
, from the identity monad into
.
Example: The identity natural transformation is a monad morphism, and monad morphisms are closed under composition as natural transformations. That is, monads on and monad morphisms between them form a category.
Example: If is a monad morphism, and it has an inverse as a natural transformation, the inverse is also a monad morphism.
Lists and free monoids
Now we have addressed the issue of monad morphisms, we are ready to show how the list monad is the free monoid monad. Recall that the free monoid monad was given forming equivalence classes of terms induced by an equational presentation of the theory of monoids. We shall denote this monad
. The list monad has universe
consisting of (some set theoretic encoding of) lists of elements from
.
and
aren’t equal, so we must consider a more liberal notion of being “the same”. There is a natural transformation
given inductively by:
.
.
.
Here, denotes the concatenation of the two input lists. The notation is also a bit unfortunate as square brackets denote both equivalence classes of terms, and lists of values. Intuitively, all
does is form a list of all the variables appearing in any representative of the equivalence class, in the order which they appear from left to right. The axioms of the theory of monoids ensure this is a well defined map, and in fact it is a monad morphism.
has an inverse given inductively on lists by:
.
.
Here is list formation via the usual cons operation you might see in Haskell for example.
So we have seen that the list monad “is” the free monoid monad in that they are isomorphic as monads on . The analogous statements about the free commutative monoid and free join semilattice monads arise via similar arguments. (Of course, there is a lot more to check than I’ve done explicitly here, that the maps are well defined, that they are natural, that the monad morphism axioms hold,…).
There are other senses in which the list monad is the free monoid monad, but to discuss those, we will need to introduce the Eilenberg-Moore category of a monad, which we shall discuss in a later post.