Freedom and Forgetfulness

I’ve been having fun exploring adjunctions lately and thinking about how we can take a monad apart and compose it the other way to get a comonad, and vice versa. Often I’ll find that a comonad counterpart of a given monad gives an interesting perspective on that monad, and ditto for a monad cousin to a given comonad.

The monad for monoids

Let’s take an example. There is a category of monoids Mon with monoids as objects and monoid homomorphisms as arrows between them. Then there is a functor from Set to Mon that takes any ordinary type A to the free monoid generated by A. This is just the List[A] type together with concatenation as the multiplication and the empty list as the identity element.

This free functor has a right adjoint that takes any monoid M in Mon to its underlying set M. That is, this right adjoint “forgets” that M is a monoid, leaving us with just an ordinary type.

If we compose these two functors, we get a monad. If we start with a type A, get its free monoid (the List[A] monoid), and then go from there to the underlying type of the free monoid, we end up with the type List[A]. The unit of our adjunction is then a function from any given type A to the type List[A].

Structure ⊣ Interpretation

But then what is the counit? Remember that for any adjunction, we can compose the functors one way to get a monad, and compose them the other way to get a comonad.

In that case we have to start with a monoid M, then “forget”, giving us the plain type M. Then we take the free monoid of that to end up with the List[M] monoid.

But notice that we are now in the monoid category. In that category, List is a comonad. And since we’re in the category of monoids, the counit has to be a monoid homomorphism. It goes from the free monoid List[A] to the monoid A:

If we apply the counit for this comonad to the free monoid, we get the join for our monad:

And to get the duplicate or extend operation in the comonad, we just turn the crank on the adjunction:

The duplicate just puts each element into its own sublist. With regard to extend, this just means that given any catamorphism on List, we can turn that into a homomorphism on free monoids.

All the interesting parts of List are the parts that make it a monoid, and our comonad here is already in a category full of monoids. Therefore the coKleisli composition in this comonad is kind of uninteresting. All it’s saying is that if we can fold a List[A] to a B, and a List[B] to a C, then we can fold a List[A] to a C, by considering each element as a singleton list.

Forget ⊣ Cofree

Let’s now consider another category, call it End(Set), which is the category of endofunctors in Set.

The arrows in this category are natural transformations:

There’s another category, Com, which is the category of comonads on Set. The arrows here are comonad homomorphisms. A comonad homomorphism from F to G is a natural transformation f: F ~> G satisfying the homomorphism law:

There is a forgetful functor Forget: Com -> End(Set) that takes a comonad to its underlying endofunctor (forgetting that it’s a comonad). And this functor has a right adjoint Cofree: End(Set) -> Com which generates a cofree comonad on a given endofunctor F. This is the following data type:

Note that not only is the endofunctor Cofree[F,?] a comonad (in Set) for any functor F, but the higher-order type constructor Cofree is itself is a comonad in the endofunctor category. It’s this latter comonad that is induced by the Forget ⊣ Cofree adjunction. That is, we start at an endofunctor F, then go to comonads via Cofree[F,?], then back to endofunctors via Forget.

The unit for this adjunction is then a comonad homomorphism. Remember, this is the unit for a monad in the category Com of comonads:

This will start with a value of type F[A] in the comonad F, and then unfold an F-branching stream from it. Note that the first level of this will have the same structure as x.

If we take unit across to the End(Set) category, we get the duplicate for our comonad:

Note that this is not the duplicate for the Cofree[F,?] comonad. It’s the duplicate for Cofree itself which is a comonad in an endofunctor category.

Turning the crank on the adjunction, the counit for this comonad now has to be the inverse of our unit. It takes the heads of all the branches of the given F-branching stream.

Sending that over to the comonad category, we get the join for our monad: