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 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