On Tue, July 24, 2012 12:30, Twan van Laarhoven wrote:
On 2012-07-24 10:10, Christian Sternagel wrote:
Dear all,
with respect to formal verification of Haskell code I was wondering whether (==) of the Eq class is intended to be commutative (for many classes such requirements are informally stated in their description, since Eq does not have such a statement, I'm asking here). Or are there any known cases where commutativity of (==) is violated (due to strictness issues)?
Strictness plays no role for Eq, since to test for equality both sides will have to be fully evaluated. I think (==) is supposed to be equivalence relation, which is symmetric (i.e. commutative); as well as reflexive and transitive.
There are some cases of (==) not being reflexive, Floats being the most notable one, but many people consider that to be a bug. I can't think of any instances that violate symmetry.
I agree, that (==) should be symmetric. However, it is easy to write Eq-instance, which violates this law: -- begin code data Foo = Foo Int deriving Show instance (Eq Foo) where (==) (Foo x) (Foo y) | x==0 = False | x==1 = True | otherwise = False value_1 = Foo 0 value_2 = Foo 1 compare_1 = value_1 == value_2 compare_2 = value_2 == value_1 -- end code compare_1 is False whereas compare_2 is True. So in your formal verification, the symmetric property of every Eq-instance has to be an axiom. I frankly don't know, whether the Haskell specification says anything about this. Frank