Move MonadIO to base

[Dan Doel]

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 
something).

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.

-- Dan