[Haskell-cafe] What unsafeInterleaveIO is unsafe

[Jonathan Cast]

On Tue, 2009-03-17 at 01:16 +0000, Claus Reinke wrote:
> >> > > "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

Oops, left a superfluous return in there.  I meant

         throw "urk!" <= 1

(The inequality is at Int).

> >  ==> evaluate (throw "urk!") <= evaluate 1
> 
>     throw (ErrorCall "urk") <= evaluate (throw (ErrorCall "urk"))

Sure enough.

But throwIO (ErrorCall "urk") /= _|_:

    Control.Exception> throwIO (ErrorCall "urk!") `seq` ()
    ()

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

Come again?

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

Could you elaborate on this?  It sounds suspiciously like you're saying
Haskell's axiomatic semantics is unsound :: IO.

> 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 ~),

So

   a ~ b = `The observable effects of $(x) and $(y) are equal'

?

> we have
> 
>     f () ~ _|_ <= return 0 ~ f _|_
> 
> so 'f' shows that wrapping both sides of an inequality in 'catch' need
> not preserve the ordering (modulo ~)

If f _|_ <= f (), then it seems that (<=) is not a (pre-) order w.r.t.
(~).  So taking the quotient of IO Int over (~) gives you a set on which
(<=) is not an ordering (and may not be a relation).

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

So

    catch (throwIO e) h ~ h e

but it is not the case that

    catch (throwIO e) h = h e

?  That must be correct, actually:

    Control.Exception> let x = Control.Exception.catch (throwIO
(ErrorCall "urk!")) (\ (ErrorCall _) -> undefined) in x `seq` ()
    ()

So catch is total (even if one or both arguments is erroneous), but the
IO executor (a beast totally distinct from the Haskell interpreter, even
if they happen to live in the same body) when executing it feels free to
examine bits of the Haskell program's state it's not safe for a normal
program to inspect.  I'll have to think about what that means a bit
more.

> The semantics in the "imprecise exceptions" paper combines a
> denotational approach for the context-free part with an operational
> semantics

[Totally OT tangent: How did operational semantics come to get its noun?
The more I think about it, the more it seems like a precís of the
implementation, rather than a truly semantic part of a language
specification.]

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

jcc