Exceptions and IO

[Alastair Reid]

Ashley Yakeley <ashley@semantic.org> writes:
> My confusion surrounding exceptions in the IO monad comes from the fact 
> that IO failures and "bottom" are not cleanly separated.

I'd phrase it slightly differently:

  One of the strengths of Hugs/GHC's Exception handling is that
  they unify errors with exceptions :-)

> I had always assumed the IO monad looked something like this:
> [...]
> But in fact IO looks more like this:
> [...]

A monadic explanation/semantics of exception handling invalidates many
standard transformations.  But, since it's a familiar way to define
the semantics, let's ignore that and press on.

1) Haskell98 IO-monad exception handling is left unchanged.
   That is, we either use

>      newtype IO a = IO (RealWorldState -> Either IOError
>                                                  (RealWorldState,a))

   or an equivalent continuation passing representation.
   (Hugs uses a continuation passing representation.)

2) We can transform pure Haskell code into equivalent monadic code
   using the identity monad:

     type Id a = a

     instance Monad Id where
       (>>=) = flip (.)
       return = id

   and the usual monadic translation:

     e1 e2  =>  liftM e1 e2
     x      =>  return x

3) Now for the switcheroo!
   Change the identity monad to an exception monad:

     type E a = Either IOFailure a

     instance Monad E where
       m >>= k = either Left k m
       return = Right

  define error by:

     error msg = Left (userError msg)

  and tweak the IO monad to propagate errors from pure code (details
  left as exercise).
   
What you have now is essentially what Hugs and GHC do at runtime.
(Well... in truth both of them use something like a
continuation-passing exception monad - but the effect is the same.)


This transformation preserves equational reasoning but gets in the way
of many other standard equalities.  For example, the following
equality no longer holds:

  x + y :: Integer = y + x :: Integer 

which tends to upset programmers doing transformational programming.
(To see the problem, let x = error "x" and y = error "y".)

Worse(?) still, this equality no longer holds:

  f $ x   =  f $! x   if f is strict

which tends to upset compiler writers since it is the starting point
for many optimization.

Since Haskell programmers and compilers exploit equalities like these
all the time, we developed a semantics which allows the actual
implementation but also allows implementations which reorder
evaluation.  I won't try to summarize the semantics here - best to
read a paper about it such as this:

  http://research.microsoft.com/Users/simonpj/Papers/except.ps.gz

or:

  http://research.microsoft.com/Users/simonpj/Papers/imprecise-exn-sem.htm


-- 
Alastair Reid        reid@cs.utah.edu        http://www.cs.utah.edu/~reid/