Tillmann Rendel
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.
Haskell is a programming language, not a theorem prover.
Yes I know. That's why I wrote axiomatic and operational semantics, not denotational; I didn't want to start a bar fight. -- (c) this sig last receiving data processing entity. Inspect headers for past copyright information. All rights reserved. Unauthorised copying, hiring, renting, public performance and/or broadcasting of this signature prohibited.