I have a coroutine transformer
data Step y m a = Done a | Yield y (CoT y m a)
data CoT y m a = CoT (m (Step y m a))
with Monad instance
unCoT :: CoT y m a -> m (Step y m a)
unCoT (CoT m) = m
instance Monad m => Monad (CoT y m) where
return = CoT . return . Done
CoT x >>= f = CoT $ do
x' <- x
case x' of
Done a -> unCoT (f a)
Yield y x' -> return (Yield y (x' >>= f))
If I define an MFunctor class with Monad m and Monad n constraints I can define hoist
class MFunctor t where
hoist :: (Monad n, Monad m) => (forall a. m a -> n a) -> t m b -> t n b
instance MFunctor (CoT y) where
hoist f (CoT m) = CoT $ do
step <- f m
return (case step of Done x -> Done x
Yield y m' -> Yield y (hoist f m'))
But mmorph's hoist only has a Monad m constraint. Can I define my hoist without it, or is this a lack of generality of MFunctor?
EDIT: I worked out it is possible! But my question still stands: are we sure there's no lack of generality here?
instance MFunctor (CoT y) where
hoist f (CoT m) = CoT $ f $ do
step <- m
return (case step of Done x -> Done x
Yield y m' -> Yield y (hoist f m'))
mmorph was developed in the context of the pipes-3.* series (it used to be an internal pipes module), which had functions like this:
raise
:: (Monad m, MFunctor t1, MonadTrans t2)
=> t1 m r -> t1 (t2 m) r
raise = hoist lift
If you add the Monad n constraint to hoist then you have to add a Monad (t2 m) constraint to raise. I generally try to minimize constraints in my libraries and I couldn't find any MFunctor instances that needed the Monad n constraint, so I removed it.
Side note: CoT y m a is the same thing as Producer y m a from pipes, which already has an MFunctor instance.
You can use any type t for which you can define hoist' :: (Monad m, Monad n) => (forall t. m t -> n t) -> t m a -> t n a as a MFunctor. But you will only be able to use the resulting t n a if you have a Monad instance on n. We do this by deferring the application of the natural transformation. Or a fancy way of saying this would be applying the coyoneda lemma.
{-# LANGUAGE RankNTypes, GADTs #-}
import Control.Monad.Morph
-- Slightly weaker than MFunctor due to the monad constraint on n.
class MFunctor' t where
hoist' :: (Monad m, Monad n) => (forall b. m b -> n b) -> t m a -> t n a
data MCoyoneda t n a where
MCoyoneda :: Monad m => (forall b. m b -> n b) -> t m a -> MCoyoneda t n a
liftMCoyoneda :: Monad m => t m a -> MCoyoneda t m a
liftMCoyoneda = MCoyoneda id
lowerMCoyoneda' :: (MFunctor' t, Monad n) => MCoyoneda t n a -> t n a
lowerMCoyoneda' (MCoyoneda f tma) = hoist' f tma
-- The result is actually slightly stronger than 'MFunctor', as we do not need
-- a monad for 'm' either.
hoistMCoyoneda :: (forall b. m b -> n b) -> MCoyoneda t m a -> MCoyoneda t n a
hoistMCoyoneda f (MCoyoneda trans tma) = MCoyoneda (f . trans) tma
instance MFunctor (MCoyoneda t) where
hoist = hoistMCoyoneda
So I don't think we loose generality, because if you can not implement an instance for MFunctor then nothing is lost by the Monad constraint on lowerMCoyoneda'.
I discovered this running into a similar problem with RVarT.
If you love us? You can donate to us via Paypal or buy me a coffee so we can maintain and grow! Thank you!
Donate Us With