[Haskell-cafe] Re: Wikipedia on first-class object

[Jonathan Cast]

On 27 Dec 2007, at 10:44 AM, Achim Schneider wrote:

> Wolfgang Jeltsch <g9ks157k at acme.softbase.org> wrote:
>
>> Am Donnerstag, 27. Dezember 2007 16:34 schrieb Cristian Baboi:
>>> I'll have to trust you, because I cannot test it.
>>>
>>> let x=(1:x); y=(1:y) in x==y .
>>>
>>> I also cannot test this:
>>>
>>> let x=(1:x); y=1:1:y in x==y
>>
>> In these examples, x and y denote the same value but the result of x
>> == y is _|_ (undefined) in both cases.  So (==) is not really
>> equality in Haskell but a kind of weak equality: If x doesn’t equal
>> y, x == y is False, but if x equals y, x == y might be True or
>> undefined.
>>
> [1..] == [1..] certainly isn't undefined, it always evaluates to True,

If something happens, it does eventually happen.

More importantly, we can prove that [1..] == [1..] = _|_, since

   [1..] == [1..]
= LUB (n >= 1) [1..n] ++ _|_ == [1..n] ++ _|_
= LUB (n >= 1) _|_
= _|_

jcc