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