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

[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?

Haskell is a programming language, not a theorem prover.

   Tillmann