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

[Timon Gehr]

On 04/12/2013 10:24 AM, oleg at okmij.org wrote:
>
> 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.

It likely is.

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

The only occurrence of 'distinguish' is in the Leibniz citation.

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

In my mind, 'evaluates-to' is an existential statement. The adequacy 
notion given there is inadequate if the program execution is 
indeterministic, as I would have expected it to be in this case. (They 
quickly note this on slide 18, giving concurrency features as an example.)

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

Thanks for the pointer, I will have a look. However, it seems that the 
semantics the definition and the proof rely on are deterministic?

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

Which is really hard. I think equational reasoning is helpful because it 
is valid for ideal programs and it seems therefore to be a good 
heuristic for real ones.

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

The abstraction bound is where exact reasoning necessarily stops.

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

InterleaveST is first referred to in chapter 10. As far as I can tell, 
the construct does not have specified a formal semantics.

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

They informally note that the final result depends on the order of 
evaluation and is therefore not always uniquely determined. (because the 
order of evaluation is only loosely specified.)

> So, unsafeInterleaveST is really bad -- and the
> people who introduced it know that, all too well.
>

I certainly do not disagree that it is bad. However, I am still not 
convinced that the example actually shows a violation of equational 
reasoning. The valid outputs, according to the informal specification in 
chapter 10, are the same for both expressions.