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 Stream
Effect (fmap Return (throwM e)) *> f =
  -- lemma 2 for m
Effect (throwM e) *> f =
  -- definition of (*>) for Stream
Effect (fmap loop (throwM e)) =  -- this 'loop' is a local function in (*>) and hides a reference to 'f'
  -- lemma 2 for m
Effect (throwM e) =
  -- lemma 2 for m
Effect (fmap Return (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 (fmap Return (throwM e))) f =
  -- lemma 2 for m
catch (Effect (throwM e)) f =
  -- definition of catch for Stream
Effect (fmap loop (throwM e) `catch` (return . f)) =
  -- lemma 2 for m
Effect (throwM e `catch` (return . f)) =
  -- MonadCatch law for m
Effect (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 join
return (f e) >>= id
  -- Monad law
id (f e)
  -- definition of id
f e

[mauke]

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

S.print (do
    S.yield "start"
    do { xs <- liftIO $ fmap lines (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 (do
    S.yield "start"
    do { xs <- liftIO $ fmap lines (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