Lennart Augustsson lennart at augustsson.net
Fri Jan 11 02:16:12 EST 2008

```Thank you Duncan, you took the words out of my mouth. :)

On Jan 10, 2008 5:42 PM, Duncan Coutts <duncan.coutts at worc.ox.ac.uk> wrote:

>
> On Fri, 2008-01-11 at 01:12 +0100, Achim Schneider wrote:
> > 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.
>
> 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
>
> _______________________________________________