In this post we shall introduce two particular classes of monad that arise in practice. As usual, we shall endeavour keep things simple, often restricting our attention to an algebraic perspective on monads.
We shall write for the category of monads on a category , and monad morphisms between them. We shall also write for the category of endofunctors on and natural transformations between them. There is an obvious forgetful functor:
This functor does not in general have a left adjoint, so we have to consider existence of free objects individually. Let be an endofunctor. The monad is the free monad over if there exists a universal natural transformation such that for every monad and natural transformation there exists a unique monad morphism such that
Note this is the usual categorical notion of free object, relative to the forgetful functor above. It is important to emphasise that there are other forgetful functors from the category of monads for which we could consider free objects. This setting is normally what is intended when the term is used without qualification.
The notation is fairly common, and relates to the similar notation used for free monoids, as there are many analogies.
Example: For a set , the exception monad is the free monad over the constant endofunctor mapping everything to . For the usual encoding of coproducts in we have been using, the universal morphism is
and for the unique fill-in morphism is:
Having seen the abstract definition, and one example, it is natural to look for a more systematic strategy yielding free monads. For the approach we shall adopt, we are going to need a bit more machinery first.
For an endofunctor , there is a category of endofunctor algebras , with objects pairs , and a morphism is a -morphism such that:
Composition and identities are as in . These conditions are similar to those we saw in discussion of the Eilenberg-Moore category in an earlier post. In fact, the category is the full subcategory of consisting of the objects satisfying the unit and multiplication axioms for an Eilenberg-Moore algebra.
There is a forgetful functor . If this functor has a left adjoint , then this induces a monad on . Furthermore, we have an equivalence of categories
Recall that such an equivalence is certainly not automatic. This returns us to the topic of monadicity, that we touched upon in an earlier post. We have not introduced enough background on monadicity to discuss this properly yet, so we take this as a fact.
If a monad is of the form as in the discussion above, it is referred to as the algebraically free monad over . We can now state the main facts that we need:
- If is the algebraically free monad over , then it is the free monad over .
- If is a complete category, and for endofunctor , exists, then the forgetful functor has a left adjoint, and .
So in the case of monads, as the base category is complete, we can reduce the task of finding free monads to that of finding algebraically free monads.
To exploit this connection, we note that every algebraic signature induces a signature endofunctor, which we shall also write as . This functor is given by the follow coproduct:
where denotes the arity of operation symbol .
Example: Let be a signature with a single binary operation and a constant. Then the corresponding endofunctor is:
A -algebra is simply a pair . The function is equivalent to giving a binary function , corresponding to the binary operation symbol, and an element of , corresponding to the constant element. That is the same thing as specifying an algebra for the signature .
More generally, it is hopefully clear that for a signature , there is an isomorphism between the category of algebras for that signature, and the category of endofunctor algebras for the corresponding signature functor.
For a fixed signature, the free algebra over a set exists, and is given by the set of all -terms over . From the isomorphism above, this means that the left adjoint to the forgetful functor exists, and so therefore does the free monad over , with is the set of all terms over the signature. As usual, it is important to consider examples:
Example: As we have seen in earlier posts, the exception monad is induced by an equational presentation with a signature consisting of just constant elements for each exception, and no equations. The signature functor is then the constant functor , and so as we saw earlier, the exception monad is the free monad over this functor.
Example: Consider a signature with a single binary operation. This induces a functor:
For the free monad over this functor, if we write for the binary operation, the set consists of terms such as
We can identify these with binary trees, with the leaves labelled by elements of . So we have constructed a binary tree monad as the free monad over .
Example: Extending the previous example, for an arbitrary signature , the resulting free monad will have consisting of trees such that:
- The leaves are labelled with elements of , or constant symbols from the signature.
- The internal nodes of arity are labelled with an operation symbol of the same arity.
Of course, we could consider endofunctors that are not of the form of signature functors. There are certainly plenty of examples where the left adjoint we require exists. In order to get a concrete description of the induced monad, we would need an explicit description of these adjoints. This requires more technical machinery than we have had chance to introduce so far, so we shall defer this topic to a later post.
The free monad constructions in the previous section have some nice properties. If we fix an algebraic signature, and consider the free monad over the corresponding signature functor, as we observed, the elements of can be thought of as certain labelled trees. Looking a bit more carefully:
- The trees in the image of the monad unit are the trivial trees with just a leaf labelled by some element of .
- The functor action just relabels the leaves of trees, according to the function .
- The functor can be restricted to the non-trivial trees, as these are preserved by the functor action. We shall denote this functor .
- There is a natural isomorphism .
- Using this isomorphism, the monad unit is the left coproduct injection.
- The monad multiplication restricts to non-trivial terms as a natural transformation in the sense that .
So free monads “keep the variables separate” in a well behaved way. The categorical structure above allow us to separate the variables from the non-trivial terms. We now abstract these observations to recover another well-studied class of monads.
An ideal monad is a monad such that:
- There exists an endofunctor with .
- The unit is the left coproduct injection.
- There exists such that .
Example: Free monads are ideal monads. This is clearly true for those induced by signature functors as discussed above, but in fact this result holds for free monads yielded by more general constructions.
Obviously there would be no need for a separate notion if the only examples were free monads.
Example: The list monad we have discussed previously restricts to a non-empty list monad, and this monad is ideal. The list monad is not ideal. If we consider the list monad as the free monoid monad, we can see this algebraically, as , so the unit is not a coproduct injection. Similarly, the non-ideal multiset monad restricts to the non-empty multiset monad, which is ideal.
We do need to be a little bit careful though. The non-empty finite powerset monad is not ideal. Algebraically this monad is the free join semilattice (without unit element) monad. The idempotence equation then ensures the monad unit cannot be a coproduct injection.
Algebraically, the ideal monads are the ones where no non-trivial equation of the form is provable, as we have seen in the example above.
There are other interesting classes of ideal monads, making conceptual use of this idea of being able to separate the non-trival terms from the variables. These examples are a whole topic in themselves, and we shall reserve them for a later post.
Further background: For those interested in the mathematics of free monads, a good place to start is the final chapter of Barr and Well’s book “Toposes, Triples and Theories”. A good source for background on ideal monads is Ghani and Uustalu’s paper “Coproducts of Ideal Monads”.
Acknowledgements: Ralph Sarkis pointed out several typos in a previous version of this post, which has greatly improved the content.
5 thoughts on “Being Free is Certainly Ideal”