On Fri, 2008-01-11 at 01:12 +0100, Achim Schneider wrote: > Tillmann Rendel <[EMAIL PROTECTED]> 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
