On Sun, 18 Apr 2010, wren ng thornton wrote:
lift ma = morph (\k -> join (fmap (k . return) ma))
Monad laws simplify that to lift ma = morph (\k -> ma >>= k . return)
The type of morph requires us to Church-encode things needlessly; what we mean to say is: morph (fmap return ma).
Hmm. If I understand this (and your other emails) correctly, you’re saying my interface class Monad m => MonadMorphIO m where morphIO :: (forall b. (m a -> IO b) -> IO b) -> m a should be equivalent to a simpler interface class Monad m => MonadJoinIO m where joinIO :: IO (m a) -> m a via some isomorphism like morphIO f = joinIO (f return) joinIO m = morphIO (\w -> m >>= w) I would be very happy to get the simpler interface to work, because it’s Haskell 98. However, if I write joinIO m = morphIO (\w -> m >>= w) morphIO' f = joinIO (f return) and define catch using morphIO' instead of morphIO: m `catch` h = morphIO $ \w -> w m `Control.Exception.catch` \e -> w (h e) m `catch'` h = morphIO' $ \w -> w m `Control.Exception.catch` \e -> w (h e) then catch' fails to actually catch anything: *Main> throwIO NonTermination `catch` \NonTermination -> return "moo" "moo" *Main> throwIO NonTermination `catch'` \NonTermination -> return "moo" *** Exception: <<loop>> Am I doing something wrong? Anders
On 04/19/10 02:15, Anders Kaseorg wrote:
I would be very happy to get the simpler interface to work, because it’s Haskell 98. However, if I write joinIO m = morphIO (\w -> m>>= w) morphIO' f = joinIO (f return) and define catch using morphIO' instead of morphIO: m `catch` h = morphIO $ \w -> w m `Control.Exception.catch` \e -> w (h e) m `catch'` h = morphIO' $ \w -> w m `Control.Exception.catch` \e -> w (h e) then catch' fails to actually catch anything:
*Main> throwIO NonTermination `catch` \NonTermination -> return "moo" "moo" *Main> throwIO NonTermination `catch'` \NonTermination -> return "moo" *** Exception:<<loop>>
Am I doing something wrong?
Well, let's see what happens if we apply it to the fairly easy
instance MonadMorphIO IO where morphIO f = f id
then joinIO m = morphIO (\w -> m >>= w) = (\w -> m >>= w) (id) = m >>= id = join m morphIO' f = joinIO (f return) = join (f return) morphIO = f id m `catch` h = morphIO $ \w -> w m `Control.Exception.catch` \e -> w (h e) [w = id] = id m `Control.Exception.catch` \e -> id (h e) m `catch'` h = morphIO' $ \w -> w m `Control.Exception.catch` \e -> w (h e) [w = return] = join (return m `Control.Exception.catch` \e -> return (h e)) 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. -Isaac
On Mon, 19 Apr 2010, Isaac Dupree wrote:
Do you see the difference?
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.) Anders
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] That is, when we take the monad to be the identity monad or equivalently to be "no monad", then parametricity yields: (forall b. (m a -> b) -> b) <-> (m a). Apparently this makes some sort of appeal to special properties about the identity monad (e.g., being both pointed and copointed) since it doesn't generalize to every monad in the way I suggested. <musing> Perhaps the correct version is this? forall a n. Monad n => (forall b. (m a -> n b) -> n b) <-> n (m (n a)) Of course that may not solve your H98 concerns. Not all monads m provide a universal law (forall n, n.m.n -> n.m) so to define the law you'd need MPTCs to relate m and n. But if we monomorphize to just n=IO that would simplify things; but then we'd need (Traversable m) in order to collapse the two layers of IO... </musing> [1] Oleg discusses a similar need to be careful about appeals to parametricity when dealing with monads: http://okmij.org/ftp/Computation/lem.html -- Live well, ~wren
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
participants (3)
-
Anders Kaseorg -
Isaac Dupree -
wren ng thornton