"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.h... 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