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

[wren ng thornton]

On 7/30/12 9:51 PM, Christian Sternagel wrote:
> Thanks Wren, for the explanations (also in your previous mail)!
>
> On 07/30/2012 01:29 PM, wren ng thornton wrote:
>> On 7/24/12 9:19 PM, Christian Sternagel wrote:
>>> (x == y) = True ==> x = y
>>> (x == y) = False ==> not (x = y)
>>> (x == _|_) = _|_
>>> (_|_ == y) = _|_
>>>
>>> Those axioms state that (==) is sound w.r.t. to meta-equality and strict
>>> in both it's arguments.
>>
>> An immediate problem that arises here is: what exactly does
>> meta-equality denote in Isabelle/HOLCF? If it is meant to denote
>> syntactic identity or Leibniz equality a la Coq, then the first axiom is
>> certainly too strong for any interesting data types (e.g., Rational,
>> Data.Set, Data.Map, Data.IntSet,...)
>
> Btw: I don't agree that the axioms are too strong for *any* interesting
> data types ;). What about Bool, Int, [a], ...? (Again, this depends on
> how we interpret "interesting"; in formalizations the threshold for
> being interesting is typically lower.)

Urk. Should've been "many" :) I was waffling between a few different 
quantifiers there, and it seems the "m" was an unfortunate casualty of 
that conflict.

-- 
Live well,
~wren