Move MonadIO to base
dan.doel at gmail.com
Fri Apr 23 15:46:46 EDT 2010
On Friday 23 April 2010 1:39:36 pm Anders Kaseorg wrote:
> On Fri, 23 Apr 2010, Tyson Whitehead wrote:
> > Are you then saying that liftIO should be able to be defined via
> > morphIO? I would be curious to see that as, after a bit of trying, I
> > still can't see how to. Specifically, I can't capture the results of
> > the desired IO operation.
> Yes, just like lift is defined via morph:
> liftIO' :: (MonadMorphIO m) => IO a -> m a
> liftIO' m = morphIO $ \down -> m >>= down . return
> main = runContT (runReaderT main' ()) return
> main' = do
> liftIO' $ putStrLn "What is your name?"
> name <- liftIO' $ getLine
> liftIO' $ putStrLn $ "Hello " ++ name
Can lift really be defined from morph, though? Given just:
class MonadTrans t where
morph :: Monad m => (forall b. (t m a -> m b) -> m b) -> t m a
trying to define:
lift :: (Monad m, MonadTrans t) => m a -> t m a
lift m = morph (\k -> m >>= k . return)
yields an error. Monad m and MonadTrans t do not imply Monad (t m), which is
what that definition requires.
Now, it's not possible to define a Monad (t m) instance using the traditional
class, because there's no way to define (>>=). So, despite the fact that t m
should always be a monad, that isn't something we're allowed to assume for a
general case (since, indeed, the instance may not be declared).
The one thing we can define with lift is return, as:
return x = lift (return x)
however, this is no help, because we're using return to try and define lift
via morph. And it doesn't look to me that there's a better way to define
return via morph:
* We're given an x : a and f : (forall b. (t m a -> m b) -> m b) -> t m a
* We need to produce a (t m a); the only way to do this is to call f
* f (\k -> ...)
- Now we have k : t m a -> m b, and need to produce an (m b)
- But producing a (t m a) from an a is what we're trying to do in the
first place. We can't recurse, though, as that'd just be infinite
recursion (to compute return' f x, compute return' f x).
So I don't think there's anything to be done. lift cannot be defined from
morph unless you make assumptions that are not permissible (unless I've missed
liftIO from morphIO is different, because the precondition on MonadMorphIO has
ensured that the analogue of (t m) is actually a monad, with a non-circular
definition of return.
More information about the Libraries