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

[Alexander Solla]

On Fri, Apr 12, 2013 at 3:37 PM, Timon Gehr <timon.gehr at gmx.ch> wrote:

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


If the final result depends on the order of evaluation, then the context in
which the result is defined is not referentially transparent.  If a context
is referentially opaque, then equational reasoning "can fail" -- i.e., it
is no longer a valid technique of analysis, since the axioms on which it
depends are no longer satisfied:

"It is necessary that four and four is eight"

"The number of planets is eight"

does not imply

"It is necessary that the number of planets is eight", as "equational
reasoning" (or, better put, "substitution of equals", the first order axiom
for equality witnessing Leibniz equality) requires.

In particular, quotation marks, necessity, and unsafeInterleaveST are
referentially opaque contexts.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/haskell-cafe/attachments/20130419/1364a375/attachment.htm>