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. [...]