<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">&lt;<a href="mailto:timon.gehr@gmx.ch" target="_blank">timon.gehr@gmx.ch</a>&gt;</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 &quot;can fail&quot; -- 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>&quot;It is necessary that four and four is eight&quot;</div><div><br></div><div>&quot;The number of planets is eight&quot;</div><div><br></div><div>does not imply</div>
<div><br></div><div>&quot;It is necessary that the number of planets is eight&quot;, as &quot;equational reasoning&quot; (or, better put, &quot;substitution of equals&quot;, 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>