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

[Frank Recker]

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