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

[Christian Sternagel]

Sorry, I forgot to reply to the list.

On 07/26/2012 11:53 AM, Alexander Solla wrote:
>> (consider, e.g., 'head undefined' vs. 'head [undefined]')
This was a typo, I meant 'tail undefined' vs. 'tail [undefined]'.

> I'm not arguing one way or the other (I know what I do, unless there's
> a need to do the other).  What I'm saying is there are lots of ways to
> interpret a language, and we can choose between them.  If you want to
> analyze Haskell, you will have to choose an interpretation for it.
> Haskell, as a logic, is paraconsistent (i.e., it's unsound.  So your
> theory for Haskell either needs to keep contradiction in the object
> language (the "partial" case where we do not identify bottoms) or take
> it out of the object language and put it into the analytical
> meta-language.
The intention is not to use Haskell as a logic, but to use an existing 
logic (HOLCF, reference in an earlier mail; thus the interpretation is 
already fixed to a high degree) to formally verify Haskell programs. In 
order to do that the program to be verified has to be "rewritten" inside 
the logic and everything that is proved about this "formal variant" of 
the program should be transferable to the real program (assuming that 
"Haskell's semantics" was captured correctly).

Another problem is if the formalization is too strict, i.e., requires 
properties from functions that are not satisfied in practice and that's 
where my original question about commutativity of (==) came from. If 
there are "reasonable" Haskell programs for which (==) is 
non-commutative, we should not require it, since we could not formalize 
those programs then.

cheers

chris
>
> The classically valid inference:
>
> (x == y) = _|_ => (y == x) = _|_
>
> On 7/25/12, Christian Sternagel <c.sternagel at gmail.com> wrote:
>> 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
>>>>
>>
>>