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.

> 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. 

_______________________________________________
Haskell-Cafe mailing list
[email protected]
http://www.haskell.org/mailman/listinfo/haskell-cafe

Reply via email to