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

[wren ng thornton]

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

While Eq is intended to denote an equivalence relation, it is just that; 
it is not an equality relation. This means you should be treating Eq as 
defining a setoid (or partial setoid, for instances like Double/Float). 
That is, you must distinguish between the raw type and the type 
quotiented by its (==). The containers libraries have taken pains to try 
and ensure that the difference cannot be observed within Haskell, but 
not all instances are so doctrinaire.

-- 
Live well,
~wren