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

There's always this, for ALL types a :(  So even where you would think that the documentation can claim that a given Eq instance follows the law of commutativity, it really cannot. Prelude Control.Concurrent System.IO.Unsafe> do m <- newEmptyMVar ;putMVar m 1 ; print $ (unsafePerformIO (do v <- takeMVar m; putMVar m 2; return v)) == (unsafePerformIO (do v <- takeMVar m; putMVar m 1 ; return v)) ; print $ (unsafePerformIO (do v <- takeMVar m; putMVar m 1; return v)) == (unsafePerformIO (do v <- takeMVar m; putMVar m 2 ; return v)) False True ---------- Původní zpráva ---------- Od: Jonas Almström Duregård Datum: 24. 7. 2012 Předmět: Re: [Haskell-cafe] Is (==) commutative? "Hi, I suppose you need to define what commutativity means in the presence of undefined values. For instance if error "0" is different from error "1" then you do not have commutativity. Also nontermination needs to be considered, for instance "(fix $ \x->x) == undefined" typically fails to terminate but "undefined == (fix $ \x->x)" typically yields an error. Regards, Jonas On 24 July 2012 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)?

cheers

chris

_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe (http://www.haskell.org/mailman/listinfo/haskell-cafe)

_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe (http://www.haskell.org/mailman/listinfo/haskell-cafe)"