Thank you Duncan, you took the words out of my mouth. :)<br><br><div class="gmail_quote">On Jan 10, 2008 5:42 PM, Duncan Coutts &lt;<a href="mailto:duncan.coutts@worc.ox.ac.uk">duncan.coutts@worc.ox.ac.uk</a>&gt; wrote:<br>
<blockquote class="gmail_quote" style="border-left: 1px solid rgb(204, 204, 204); margin: 0pt 0pt 0pt 0.8ex; padding-left: 1ex;"><div class="Ih2E3d"><br>On Fri, 2008-01-11 at 01:12 +0100, Achim Schneider wrote:<br>&gt; Tillmann Rendel &lt;
<a href="mailto:rendel@rbg.informatik.tu-darmstadt.de">rendel@rbg.informatik.tu-darmstadt.de</a>&gt; wrote:<br>&gt;<br>&gt; &gt; Achim Schneider wrote:<br>&gt; &gt; &gt; [1..] == [1..]<br>&gt; &gt; &gt;<br>&gt; &gt; &gt; [some discussion about the nontermination of this expression]
<br>&gt; &gt; &gt;<br>&gt; &gt; &gt; The essence of laziness is to do the least work necessary to cause<br>&gt; &gt; &gt; the desired effect, which is to see that the set of natural numbers<br>&gt; &gt; &gt; equals the set of natural numbers, which, axiomatically, is always
<br>&gt; &gt; &gt; computable in O(1) by equality by identity.<br>&gt; &gt;<br>&gt; &gt; This would make sense if Haskell had inbuild equality and (==) where<br>&gt; &gt; part of the formal semantics of Haskell, wich it isn&#39;t. (==) is a
<br>&gt; &gt; library function like every other library function. How could the<br>&gt; &gt; language or a system implementing the language decide wether this or<br>&gt; &gt; any other library function returns True without actually running it?
<br>&gt; &gt;<br>&gt; The list instance for Eq might eg. know something about the structure<br>&gt; of the lists and be smart enough not to get caught in the recursion of x<br>&gt; = 1:1:x and y = 1:1:1:y so it could successfully compare x == y to
<br>&gt; True in six compares.<br><br></div>So let&#39;s imagine:<br><br>ones = 1 : ones<br><br>ones&#39; = repeat 1<br> &nbsp;where repeat n = n : repeat n<br><br>So you&#39;re suggesting that:<br><br>ones == ones = True<br>but
<br>ones&#39; == ones&#39; = _|_<br><br><br>Well if that were the case then &nbsp;it is distinguishing two equal values<br>and hence breaking referential transparency. We can fairly trivially<br>prove that ones and ones&#39; are equal so == is not allowed to distinguish
<br>them. Fortunately it is impossible to write == above, at least using<br>primitives within the language.<br><font color="#888888"><br>Duncan<br></font><div><div></div><div class="Wj3C7c"><br>_______________________________________________
<br>Haskell-Cafe mailing list<br><a href="mailto:Haskell-Cafe@haskell.org">Haskell-Cafe@haskell.org</a><br><a href="http://www.haskell.org/mailman/listinfo/haskell-cafe" target="_blank">http://www.haskell.org/mailman/listinfo/haskell-cafe
</a><br></div></div></blockquote></div><br>