
wren ng thornton wrote:
Anders Kaseorg wrote:
Isaac Dupree wrote:
Do you see the difference? The effects are sequenced in different places. The return/join pair moves all the effects *outside* the operations such as catch... thus defeating the entire purpose of morphIO.
Yes; my question is more whether Wren has a more clever way to get an isomorphism (forall b. (m a -> IO b) -> IO b) <-> IO (m a) that would make the simpler interface work out. (Or maybe I misunderstood what he was getting at.)
Yeah no, that's what I was getting at. Since it doesn't quite work out, I should probably rethink my appeal to parametricity re Kleisli arrows.[1]
No, my parametricity was correct, just the implementations were wrong: {-# LANGUAGE RankNTypes #-} module MorphIO where import Prelude hiding (catch) import Control.Monad import qualified Control.Exception as E import Control.Exception (NonTermination(..)) class Monad m => MonadMorphIO m where morphIO :: (forall b. (m a -> IO b) -> IO b) -> m a class Monad m => MonadJoinIO m where -- | Embed the IO into the monad m joinIO :: IO (m a) -> m a -- | Extract the IO computation to the top level, -- rendering the m pure from IO. partIO :: m a -> IO (m a) joinIO' m = morphIO (m >>=) morphIO' f = joinIO (f partIO) instance MonadMorphIO IO where morphIO f = f id instance MonadJoinIO IO where joinIO = join partIO = fmap return -- N.B. fmap return /= return catch m h = morphIO $ \w -> w m `E.catch` \e -> w (h e) catch' m h = morphIO' $ \w -> w m `E.catch` \e -> w (h e) test = E.throwIO NonTermination `catch` \NonTermination -> return "moo" test' = E.throwIO NonTermination `catch'` \NonTermination -> return "moo" -- Live well, ~wren