[Haskell-cafe] What unsafeInterleaveIO is unsafe
claus.reinke at talk21.com
Mon Mar 16 21:16:26 EDT 2009
>> > > "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"
>> 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
> 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) >>=
and hence violates monotonicity
(_|_ <= ()) => (f _|_ <= f ())
*Main> f undefined
*Main> f ()
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.
More information about the Haskell-Cafe