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

[Jonathan Cast]

On 27 Dec 2007, at 12:20 PM, Achim Schneider wrote:

> Jonathan Cast <jonathanccast at fastmail.fm> wrote:
>
>> 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) _|_
>> = _|_
>>
> As far as I understand
> http://www.haskell.org/haskellwiki/Bottom
> , only computations which cannot be successful are bottom, not those
> that can be successful, but aren't.

Um, no.  Haskell has no formal denotational semantics, but everyone  
knows what it should be.  And _|_ is a polymorphic value in that  
domain.  _|_ is the denotation of every Haskell expression whose  
denotation is _|_.

> Kind of idealizing reality, that is.
>
> Confusion of computations vs. reductions

In Haskell, these are the same thing (modulo IO).

> and whether time exists or
> not is included for free here. Actually, modulo mere words, I accept
> both your and my argument as true

Huh?

> , but prefer mine.

Preference doesn't come into it.  By definition, the denotations of  
Haskell functions are monotone continous functions on pointed  
complete partial orders.

> You _do_ accept that you won't ever see Prelude.undefined in ghci
> when evaluating
> let x=(1:x); y=(1:y) in x==y

Huh?

> , and there won't ever be a False in the chain of &&'s, don't you?

Huh?

> The question arises, which value is left from the possible values of
> Bool when you take away False and _|_?

Why take away _|_?

> And now don't you dare to say that _|_ /= undefined.

undefined is one of many Haskell expressions that has _|_ as a  
denotation.  It is not a normal form, certainly, but that's ok.

You seem to think that _|_ is defined in terms of operational  
semantics.  Haskell hasn't got an operational semantics, just a  
denotational semantics that implementations must produce an  
operational semantics to match with.  _|_ is a denotational idea,  
defined in terms of partial orders and least upper bounds.  An  
infinite list is the least upper bound of an infinite set of partial  
lists, and the value of any function (such as \x -> x == x) applied  
to it is the least upper bound of the values of that function applied  
to those partial lists.

By definition.

jcc