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]
.
1
|
|
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
:
1 2 |
|
If we apply the counit
for this comonad to the free monoid, we get the join
for our monad:
1
|
|
And to get the duplicate
or extend
operation in the comonad, we just turn the crank on the adjunction:
1 2 |
|
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.
1 2 |
|
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:
1 2 3 |
|
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:
1
|
|
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:
1
|
|
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:
1 2 3 |
|
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:
1 2 |
|
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.
1 2 3 |
|
Sending that over to the comonad category, we get the join
for our monad:
1 2 |
|
Comments