[Haskell-cafe] What unsafeInterleaveIO is unsafe

[Claus Reinke]

>> > > "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.
>> "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"! <= return 1
>  ==> evaluate (throw "urk!") <= evaluate 1

    throw (ErrorCall "urk") <= evaluate (throw (ErrorCall "urk"))

as demonstrated here

    *Main> throw (ErrorCall "urk") `seq` ()
    *** Exception: urk
    *Main> evaluate (throw (ErrorCall "urk")) `seq` ()
    ()

So that first step already relies on IO (where the two are equivalent).

This is very delicate territory. For instance, one might think that
this 'f' seems to define a "negation function" of information content

    f x = Control.Exception.catch (evaluate x >> let x = x in x) (\(ErrorCall _)->return 0) >>= 
print

and hence violates monotonicity

    (_|_ <= ()) => (f _|_ <= f ())

since

    *Main> f undefined
    0
    *Main> f ()
    Interrupted.

But that is really mixing context-free expression evaluation and
context-sensitive execution of io operations. Most of our favourite
context-free equivalences only hold within the expression evaluation
part, while IO operations are subject to additional, context-sensitive
rules. For instance, without execution

    *Main> f () `seq` ()
    ()
    *Main> f undefined `seq` ()
    ()

but if we include execution (and the context-sensitive equivalence
that implies, lets call it ~), we have

    f () ~ _|_ <= return 0 ~ f _|_

so 'f' shows that wrapping both sides of an inequality in 'catch' need
not preserve the ordering (modulo ~) - its whole purpose is to recover
from failure, making something more defined (modulo ~) by translating
_|_ to something else. Which affects your second implication.

If the odd properties of 'f' capture the essence of your concerns, I think
the answer is to keep =, <=, and ~ clearly separate, ideally without losing
any of the context-free equivalences while limiting the amount of
context-sensitive reasoning required. If = and ~ are mixed up, however,
monotonicity seems lost.

The semantics in the "imprecise exceptions" paper combines a
denotational approach for the context-free part with an operational
semantics for the context-sensitive part. This tends to use the good
properties of both, with a clear separation between them, but a
systematic treatment of the resulting identities was left for future work.

Claus