[Haskell-cafe] unsafeInterleaveST (and IO) is really unsafe

[oleg at okmij.org]

Timon Gehr wrote:
> I am not sure that the two statements are equivalent. Above you say that
> the context distinguishes x == y from y == x and below you say that it
> distinguishes them in one possible run.

I guess this is a terminological problem. The phrase `context
distinguishes e1 and e2' is the standard phrase in theory of
contextual equivalence. Here are the nice slides
        http://www.cl.cam.ac.uk/teaching/0910/L16/semhl-15-ann.pdf

Please see adequacy on slide 17. An expression relation between two
boolean expressions M1 and M2 is adequate if for all program runs (for
all initial states of the program s), M1
evaluates to true just in case M2 does. If in some circumstances M1
evaluates to true but M2 (with the same initial state) evaluates to
false, the expressions are not related or the expression relation is
inadequate.

See also the classic
        http://www.ccs.neu.edu/racket/pubs/scp91-felleisen.ps.gz
(p11 for definition and Theorem 3.8 for an example of a
distinguishing, or witnessing context).

> In essence, lazy IO provides unsafe constructs that are not named
> accordingly. (But IO is problematic in any case, partly because it
> depends on an ideal program being run on a real machine which is based
> on a less general model of computation.)

I'd agree with the first sentence. As for the second sentence, all
real programs are real programs executing on real machines. We may
equationally prove (at time Integer) that 
        1 + 2^100000 == 2^100000 + 1
but we may have trouble verifying it in Haskell (or any other
language). That does not mean equational reasoning is useless: we just
have to precisely specify the abstraction boundaries. BTW, the
equality above is still useful even in Haskell: it says that if the
program managed to compute 1 + 2^100000 and it also managed to compute
2^100000 + 1, the results must be the same. (Of course in the above
example, the program will probably crash in both cases).  What is not
adequate is when equational theory predicts one finite result, and the
program gives another finite result -- even if the conditions of
abstractions are satisfied (e.g., there is no IO, the expression in
question has a pure type, etc).

> I think this context cannot be used to reliably distinguish x == y and y
> == x. Rather, the outcomes would be arbitrary/implementation
> defined/undefined in both cases.

My example uses the ST monad for a reason: there is a formal semantics
of ST (denotational in Launchbury and Peyton-Jones and operational in
Moggi and Sabry). Please look up ``State in Haskell'' by Launchbury
and Peyton-Jones. The semantics is explained in Sec 6. Please see Sec
10.2 Unique supply trees -- you might see some familiar code. Although
my example was derived independently, it has the same kernel of
badness as the example in Launchbury and Peyton-Jones. The authors
point out a subtlety in the code, admitting that they fell into the
trap themselves. So, unsafeInterleaveST is really bad -- and the
people who introduced it know that, all too well.