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
_______________________________________________
Haskell-Cafe mailing list
[email protected]
http://www.haskell.org/mailman/listinfo/haskell-cafe
