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

Achim Schneider barsoap at web.de
Thu Jan 10 19:12:02 EST 2008

Tillmann Rendel <rendel at rbg.informatik.tu-darmstadt.de> 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. 

More information about the Haskell-Cafe mailing list