[Haskell-cafe] Is (==) commutative?
Twan van Laarhoven
twanvl at gmail.com
Tue Jul 24 14:12:58 CEST 2012
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
> So in your formal
> verification, the symmetric property of every Eq-instance has to be an
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.
More information about the Haskell-Cafe