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

[Twan van Laarhoven]

On 24/07/12 13:32, Frank Recker wrote:
> I agree, that (==) should be symmetric. However, it is easy to write
> Eq-instance, which violates this law:

It is impossible to specify laws such as symmetry in Haskell, which is why they 
are usually stated in the documentation. However, this style of documentation is 
a relatively recent trend (last 5 years or so). I suspect that is why the 
documentation for the Eq class does not specify the laws for an equivalence 
relation.


> So in your formal
> verification, the symmetric property of every Eq-instance has to be an
> axiom.

An alternative for equational reasoning is to not use Eq, but just directly use 
syntactic equality. I.e. write (=) instead of (==).


 > I frankly don't know, whether the Haskell specification says
 > anything about this.

I checked, and it doesn't say anything about laws for Eq instances. The closest 
it comes is with the remark that "The Ord class is used for totally ordered 
datatypes", but there is no requirement that Ord and Eq be coherent, or even 
that (==) and (/=) are coherent.


Twan