> > "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
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
