<div dir="ltr"><br><div class="gmail_extra"><br><br><div class="gmail_quote">On Fri, Apr 12, 2013 at 3:37 PM, Timon Gehr <span dir="ltr"><<a href="mailto:timon.gehr@gmx.ch" target="_blank">timon.gehr@gmx.ch</a>></span> wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div><br></div><div>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
Please see Sec<br>
10.2 Unique supply trees -- you might see some familiar code. Although<br>
my example was derived independently, it has the same kernel of<br>
badness as the example in Launchbury and Peyton-Jones. The authors<br>
point out a subtlety in the code, admitting that they fell into the<br>
trap themselves.<br>
</blockquote>
<br></div>
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.)</blockquote><div><br></div><div>
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: </div>
<div><br></div><div>"It is necessary that four and four is eight"</div><div><br></div><div>"The number of planets is eight"</div><div><br></div><div>does not imply</div>
<div><br></div><div>"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.</div>
<div><br></div><div>In particular, quotation marks, necessity, and unsafeInterleaveST are referentially opaque contexts.</div></div></div></div>