[Haskell-cafe] Is (==) commutative?

[Christian Sternagel]

Dear Alexander,

Let me clarify again: by "we identify all bottoms" I mean that any error 
and also nontermination is identified with _|_ . However, I did not mean 
that [_|_] is identified with _|_ (since the point of a formal treatment 
is exactly to correctly consider the lazy semantics of Haskell). In 
Haskell there definitely is a difference between 'undefined' and 
'[undefined]' (consider, e.g., 'head undefined' vs. 'head [undefined]') 
so this must be taken in to account in a rigorous treatment.

Btw: I didn't get which inference you meant when you where saying it is 
"classically valid".

cheers

chris

On 07/26/2012 11:13 AM, Alexander Solla wrote:
> Depending on the context, it may or may not be wise to distinguish
> between undefined and [undefined].  This is a matter of strictness,
> laziness, and totality.  If you identify all bottoms as one, you
> essentially restrict yourself to (what might as well be, for the
> purposes of this discussion) a strict subset of the Haskell language.
>
> If you distinguish between values that "contain" bottom and "are"
> bottom, then you need to deal with the semantics of laziness.
>
> Like I said, it is classically valid, so choosing these semantics
> means that it will be safe.  But the undecidability of comparing
> distinct bottoms means that you have to make a choice.
>
> On 7/24/12, Christian Sternagel <c.sternagel at gmail.com> wrote:
>>> It's a classically valid inference, so you're "safe" in that respect,
>>> and it is true that evaluating x == y requires traversing x and y, so
>>> that if x or y "are" bottom, (x == y) and (y == x) will both be bottom.
>> Well, (x == y) could result in bottom, even if neither x nor y are
>> bottom, e.g., [undefined] == [undefined]. -cheers chris
>>