Thu 30 Jun 2011
More on Comonads as Monad Transformers
Posted by Edward Kmett under Category Theory , Comonads , Haskell , Kan Extensions , Monads[3] Comments
Last time in Monad Transformers from Comonads I showed that given any comonad we can derive the monad-transformer
newtype CoT w m a = CoT { runCoT :: w (a -> m r) -> m r
and so demonstrated that there are fewer comonads than monads in Haskell, because while every Comonad gives rise to a Monad transformer, there are Monads that do not like IO, ST s, and STM.
I want to elaborate a bit more on this topic.
In Monads from Comonads we observed that for non-transformer version of CoT
type Co w = CoT w Identity
under the assumption that w = f . g for f -| g : Hask -> Hask, then
Co w ~ Co (f . g) ~ g . f
This demonstrated that the Co w is isomorphic to the monad we obtain by composing the adjunction that gave rise to our comonad the other way around.
But what about CoT?
Sadly CoT is a bit bigger.
We can see by first starting to apply the same treatment that we gave Co.
CoT w m a ~ forall r. w (a -> m r) -> m r ~ forall r. f (g (a -> m r)) -> m r ~ forall r. f (f() -> a -> m r) -> m r ~ forall r. f (a -> f () -> m r) -> m r ~ forall r. (a -> f () -> m r, f ()) -> m r ~ forall r. (a -> f () -> m r) -> f () -> m r ~ forall r. (a -> g (m r)) -> g (m r) ~ Codensity (g . m) a
(I'm using . to represent Compose for readability.)
But we've seen before that Codensity g a is in a sense bigger than g a, since given an Adjunction f -| g, Codensity g a ~ (g . f) a, not g a.
Moreover can compose adjunctions:
instance (Adjunction f g, Adjunction f' g') => Adjunction (Compose f' f) (Compose g g') where unit = Compose . leftAdjunct (leftAdjunct Compose) counit = rightAdjunct (rightAdjunct getCompose) . getCompose
So if n -| m, then we can see that Codensity (g . m) a ~ g . m . n . f, rather than the smaller g . m . f, which we can obtain using AdjointT f g m from Control.Monad.Trans.Adjoint in adjunctions.
So CoT isn't the smallest monad transformer that would be given by an adjunction.
In fact, it is isomorphic to AdjointT f g (Codensity m) a instead of AdjointT f g m a.
Sadly, there doesn't appear to be a general purpose construction of the smaller transformer just given an unseparated w = f . g.

June 30th, 2011 at 4:31 pm
Co w a ~ Co (f . g) ~ g . f
Shouldn’t that be Co w?
CoT w m a ~ Codensity (g . m) r
Shouldn’t that be Codensity (g . m) a?
June 30th, 2011 at 7:05 pm
Yes and yes. :)
June 30th, 2011 at 10:58 pm
[...] Last time, when we inspected CoT w m a we demonstrated that on one hand given a suitable adjunction f -| g, such that w = f . g, Co w ~ Co (f . g) ~ (g . f), but on the other CoT w m a was bigger than g . m . f, and that if n -| m, then CoT w m a ~ g . m . n . f. [...]