On Fri, Apr 12, 2013 at 3:37 PM, Timon Gehr
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.