On Jul 24, 2012 1:35 PM, "Tristan Seligmann" <mithrandi@mithrandi.net> wrote:

On Jul 24, 2012 12:32 PM, "Twan van Laarhoven" <twanvl@gmail.com> 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 don't think this is necessarily true.  For example:

(==)  :: (Eq a)  => Maybe a -> Maybe a -> Bool
Nothing == Nothing = True
Nothing == Just _ = False
Just _ == Nothing = False
Just x == Just y = x == y

This particular example is still commutative, however (at least I think it is).