add MonadThrow and MonadCatch instances for Stream

[mauke]

No description provided.

[treeowl]

Please leave a comment proving the MonadCatch law. Please also document (somewhere in the Haddocks) how these instances behave, preferably with a few examples, including both "good" examples of desirable behavior and "bad" examples of behavior that might not be what the user expected/desired.

[mauke]

Is the following correct/complete?

---

I can prove the MonadThrow and MonadCatch laws under the assumption that a >> b = a >>= \_ -> b (which I don't see formally stated anywhere, but I'm going to assume it anyway).

Lemma 1:

throwM e >>= f = throwM e

Proof:

throwM e >>= f =-- MonadThrow law (in reverse) for some arbitrary action 'w'-- (in particular, you can always choose w = throwM e)
(throwM e >> w) >>= f =-- my assumption
(throwM e >>=\_ -> w) >>= f =-- Monad associativity
throwM e >>= (\x -> (\_ -> w) x >>= f) =-- beta reduction
throwM e >>= (\_ -> w >>= f) =-- my assumption, again
throwM e >> (w >>= f)
-- MonadThrow law
throwM e

Lemma 2:

fmap f (throwM e) = throwM e

Proof:

fmap f (throwM e) =-- behavior of fmap for monads
throwM e >>=return. f
-- lemma 1
throwM e

Theorem 1 (MonadThrow law for Stream f m):

throwM e >> f = throwM e

Proof:

throwM e >> f =-- definition of throwM, (>>) for Stream
lift (throwM e) *> f =-- definition of lift for StreamEffect (fmapReturn (throwM e)) *> f =-- lemma 2 for mEffect (throwM e) *> f =-- definition of (*>) for StreamEffect (fmap loop (throwM e)) =-- this 'loop' is a local function in (*>) and hides a reference to 'f'-- lemma 2 for mEffect (throwM e) =-- lemma 2 for mEffect (fmapReturn (throwM e)) =-- definition of lift for Stream
lift (throwM e) =-- definition of throwM for Stream
throwM e

Theorem 2 (MonadCatch law for Stream f m):

catch (throwM e) f = f e

Proof:

catch (throwM e) f =-- definition of throwM for Stream
catch (lift (throwM e)) f =-- definition of lift for Stream
catch (Effect (fmapReturn (throwM e))) f =-- lemma 2 for m
catch (Effect (throwM e)) f =-- definition of catch for StreamEffect (fmap loop (throwM e) `catch` (return. f)) =-- lemma 2 for mEffect (throwM e `catch` (return. f)) =-- MonadCatch law for mEffect (return (f e))
-- definition of effect
effect (return (f e))
-- specification/law of effect
(join . lift) (return (f e))
-- associativity of (.)
join ((lift .return) (f e))
-- MonadTrans law
join (return (f e))
-- definition of joinreturn (f e) >>=id-- Monad lawid (f e)
-- definition of id
f e

[mauke]

As for examples of desirable behavior, do you mean something like this?

S.print (doS.yield "start"do { xs <- liftIO $fmaplines (readFile"some-imaginary-file");
S.each xs }
S.yield "finish"
)
{-"start"*** Exception: some-imaginary-file: openFile: does not exist (No such file or directory)-}

S.print (doS.yield "start"do { xs <- liftIO $fmaplines (readFile"some-imaginary-file");
S.each xs }
`catchIOError` (\e ->do
liftIO $ hPutStrLn stderr $"caught an error: "++show e
S.yield "something else"
)
S.yield "finish"
)
{-"start"caught an error: some-imaginary-file: openFile: does not exist (No such file or directory)"something else""finish"-}

What would "bad" behavior look like?

[mauke]

@treeowl Ping?

[treeowl]

Been sick for a week. Please ping again later.

[mauke]

Get well soon!

[mauke]

Ping?

[Topsii]

@treeowl ping