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

[Christian Sternagel]

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,...)
Yes, we also stumbled about this (but I was only discussing it on the 
isabelle mailing list and not here, sorry). The conclusion was that for 
many type classes there are several "interesting" (whatever that means) 
instances. Thus, in the formalization we will use different "formal" 
type classes for different intended use-cases of Haskell type classes 
(e.g., one eq class for syntactic equality and another one that merely 
requires an equivalence relation, ...). That just means that there will 
not be a bijection between the formal class hierarchy and the actual 
class hierarchy of Haskell, but should not pose any further problems (I 
hope).

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

cheers

chris