Re: [Haskell-cafe] Re: Why purely in haskell?

Thank you Duncan, you took the words out of my mouth. :) On Jan 10, 2008 5:42 PM, Duncan Coutts wrote:

On Fri, 2008-01-11 at 01:12 +0100, Achim Schneider wrote:

...

Tillmann Rendel wrote:

...

Achim Schneider wrote:

...

[1..] == [1..]

[some discussion about the nontermination of this expression]

The essence of laziness is to do the least work necessary to cause the desired effect, which is to see that the set of natural numbers equals the set of natural numbers, which, axiomatically, is always computable in O(1) by equality by identity.

This would make sense if Haskell had inbuild equality and (==) where part of the formal semantics of Haskell, wich it isn't. (==) is a library function like every other library function. How could the language or a system implementing the language decide wether this or any other library function returns True without actually running it?

The list instance for Eq might eg. know something about the structure of the lists and be smart enough not to get caught in the recursion of x = 1:1:x and y = 1:1:1:y so it could successfully compare x == y to True in six compares.

So let's imagine:

ones = 1 : ones

ones' = repeat 1 where repeat n = n : repeat n

So you're suggesting that:

ones == ones = True but ones' == ones' = _|_

Well if that were the case then it is distinguishing two equal values and hence breaking referential transparency. We can fairly trivially prove that ones and ones' are equal so == is not allowed to distinguish them. Fortunately it is impossible to write == above, at least using primitives within the language.

Duncan

_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe