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