[Haskell-cafe] What unsafeInterleaveIO is unsafe

[Jonathan Cast]

On Mon, 2009-03-16 at 22:01 +0000, Duncan Coutts wrote:
> On Mon, 2009-03-16 at 14:17 -0700, Jonathan Cast wrote:
> > On Mon, 2009-03-16 at 22:12 +0100, Henning Thielemann wrote:
> > > On Sun, 15 Mar 2009, Claus Reinke wrote:
> > > 
> > > > import Data.IORef
> > > > import Control.Exception
> > > >
> > > > main = do
> > > >   r <- newIORef 0
> > > >   let v = undefined
> > > >   handle (\(ErrorCall _)->print "hi">>return 42) $ case f v of
> > > >     0 -> return 0
> > > >     n -> return (n - 1)
> > > >   y <- readIORef r
> > > >   print y
> > > 
> > > I don't see what this has to do with strictness. It's just the hacky 
> > > "exception handling" which allows to "catch" programming errors.
> > 
> > And which I have a sneaking suspicion actually *is* `unsafe'.  Or, at
> > least, incapable of being given a compositional, continuous semantics.
> 
> See this paper:
> 
> "A semantics for imprecise exceptions"
> http://research.microsoft.com/en-us/um/people/simonpj/papers/imprecise-exn.htm
> 
> Basically if we can only catch exceptions in IO then it doesn't matter,
> it's just a little extra non-determinism and IO has plenty of that
> already.

I'm not sure that helps much.  Given the following inequalities (in the
domain ordering) and equations:

  throw "urk! " <= 1
  evaluate . throw = throwIO
  evaluate x = return x          -- x total
  catch (throwIO a) h = h a
  catch (return x) h = return x

we expect to be able to reason as follows:

      throw "urk"! <= return 1
  ==> evaluate (throw "urk!") <= evaluate 1
  ==> catch (evaluate (throw "urk!")) (const $ return 2) <= catch
(evaluate 1) (const $ return 2)

while

    catch (evaluate (throw "urk!")) (const $ return 2)
  = catch (throwIO "urk!") (const $ return 2)
  = const (return 2) "urk!"
  = return 2

and

    catch (evaluate 1) (const $ return 2)
  = catch (return 1) (const $ return 2)
  = return 1

So return 2 <= return 1, in the domain ordering?  That doesn't seem
right.

jcc