Every free monad over a ??? functor yields a comonad?

Question

In this answer to "Can a monad be a comonad?" we see that

Every Cofree Comonad over an Alternative functor yields a Monad.

What would be the dual to this? Is there a class of functors that automatically make a free monad over them a comonad?

Answer 1

Well yes, you can dualize the construction, but the only member of the resulting class is the empty functor, whose free monad (the identity monad) is indeed also a comonad. Not very exciting.

The construction you refer to actually needs rather little to go through, so let's abandon the baggage of Hask and work in the following generality. Let

• (C, ⊗, 1) be a monoidal category

• F : C -> C a monoid-valued functor, that is, there are maps 1 -> FX and FX ⊗ FX -> FX that are natural in X, and unital and associative

Define TX = X ⊗ F(TX). Assume this recursive definition makes sense somehow and we can make recursive definitions on T. Then we can make T into a monad with the following structure maps:

• unit given by

      X = X ⊗ 1
       -> X ⊗ F(TX)            [unit map of F]
        = TX
  

• join given by

  T(TX) = TX ⊗ F(TTX)
        = X ⊗ F(TX) ⊗ F(TTX)
       -> X ⊗ F(TX) ⊗ F(TX)    [join recursively under F]
       -> X ⊗ F(TX)            [multiplication of F]
        = TX
  

When ⊗ is the Cartesian product, this construction is the monad structure on the free comonad on an Alternative functor that you refer to. In fact, the Applicative part of the Alternative structure is irrelevant. Only the class methods of Alternative itself (plus Functor) are needed: a monoid-valued functor. Element-wise, the steps that make up join as described above are given by

(x :< xs) :< xss  ->  (x :< xs, xss)
                  ->  (x, xs, xss)
                  ->  (x, xs, fmap join xss)
                  ->  (x, xs <|> fmap join xss)
                  ->  x :< (xs <|> fmap join xss)

and this is easily seen (by setting k = id) to agree with

(a :< m) >>= k = case k a of
                   b :< n -> b :< (n <|> fmap (>>= k) m)

Since our initial structure was so minimal, it is easily dualized. So let (C, ⊗, 1) continue to be a monoidal category but now assume

• G : C -> C a comonoid-valued functor, that is, there are maps GX -> 1 and GX -> GX ⊗ GX that are natural in X, and counital and coassociative

Then we can define UX = X ⊗ G(UX) (again assuming that this somehow makes sense) and by dual constructions equip U with the structure of a comonad. That is in a sense the real answer here, but to address your specific question we should consider what happens for some concrete choices of ⊗.

First suppose ⊗ is again the Cartesian product. Then every functor G is comonoidal-valued in a unique way (counitality forces GX -> GX x GX to be the diagonal). So for any functor G, we get a comonad UX = X x G(UX). In fact this turns out to just the usual cofree comonad on a functor construction (justifying the "cofree comonad" part of your slogan; when F is monoid-valued we can set G = F and G is automatically comonoid-valued, and then T and U have the same underlying functor).

Dually if ⊗ is the coproduct ⨿ then any G which is comonoidal-valued for ⨿ is also monoidal-valued for ⨿ in a unique way, so UX = X ⨿ G(UX) is also the free monad on G as well as being a comonad.

But in Hask the unit object for ⨿ is the empty type 0, and the counit of G is supposed to have type GX -> 0, which is possible only when GX = 0 for all X (this is true in any cartesian closed category). So, there are no interesting examples of this construction in Hask. This lack of symmetry is a typical phenomenon of categories that resemble Set.