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

On 24/07/12 14:44, timothyhobbs@seznam.cz wrote:

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.

Once you invoke unsafePerformIO, you can break the type system, and probably execute random assembly code and write to any memory location. So, at this point all bets for the rest of the program are of. It is up to the programmer to verify that all the necessary invariants still hold when you do unsafe stuff. In other words, the issue here is not with a particular Eq instance, it is with unsafePerformIO. Essentially `unsafePerformIO (x :: IO Int)` is not really an Int, but rather a value that behaves like one in most but not all cases. Also, let a = unsafePerformIO x in (a,a) is *not* the same thing as (unsafePerformIO x,unsafePerformIO x). For your entertainment: λ> do m <- newEmptyMVar ;putMVar m 1 ; let {a =(unsafePerformIO (do v <- takeMVar m; putMVar m 2; return v)); b = (unsafePerformIO (do v <- takeMVar m; putMVar m 1 ; return v))} ; print (a == b); print (b == a) False False Twan

Dear all, Thanks for your replies. Just to clarify: I am fully aware that inside Haskell there is no guarantee that certain (intended) requirements on type class instances are satisfied. I was asking whether the intention for Eq is that (==) is commutative, because if it was, I would require that as an axiom for the equivalent of Eq in our formal setting (I'm using the proof assistant Isabelle/HOLCF [1]). Afterwards only types for which one could prove commutativity could be instances of Eq. But if there where already "standard" instances which violated this requirement, adding it in the formal setting would prevent it from being applicable to "standard" Haskell programs. Btw: Isabelle/HOLCF unifies all error values and nontermination in a single bottom element _|_. Currently we are using the following axioms for our formal Eq class (where I'm using Haskell syntax although the real sources [2] use Isabelle/HOLCF syntax which is slightly different; (=) is meta-equality). (x == y) = True ==> x = y (x == y) = False ==> not (x = y) (x == _|_) = _|_ (_|_ == y) = _|_ Those axioms state that (==) is sound w.r.t. to meta-equality and strict in both it's arguments. The question is whether we should also add. (x == y) = _|_ ==> (y == x) = _|_ Which would directly imply (x == y) = (y == x) cheers chris [1] http://isabelle.in.tum.de (and http://isabelle.in.tum.de/dist/library/HOL/HOLCF/) [2] http://sourceforge.net/p/holcf-prelude

On 7/24/12 9:19 PM, Christian Sternagel wrote:

Dear all,

Thanks for your replies. Just to clarify: I am fully aware that inside Haskell there is no guarantee that certain (intended) requirements on type class instances are satisfied. I was asking whether the intention for Eq is that (==) is commutative, because if it was, I would require that as an axiom for the equivalent of Eq in our formal setting (I'm using the proof assistant Isabelle/HOLCF [1]). Afterwards only types for which one could prove commutativity could be instances of Eq. But if there where already "standard" instances which violated this requirement, adding it in the formal setting would prevent it from being applicable to "standard" Haskell programs.

Indeed, the standard wisdom is that Eq ought to denote an equivalence relation. However, the instance for Double and Float is not an equivalence relation. This is "necessary" due to Double/Float vaguely matching the IEEE-754 spec which requires that NaN /= NaN. If NaN is removed, I think Double/Float ought to behave as desired--- though there was a recent kerfluffle about the fact that the CPU-internal representation of Double/Float has more bits of precision than the in-memory representation, so vagaries about when values leave registers to be stored in memory will affect whether two values come out to be equal or not. Not to mention that Float/Double violate numerous laws of other classes; e.g., Ord is not a total ordering because of NaN; Num is not a ring because addition and multiplication are not associative (they are commutative though);... Depending on what your goals are, it may be best to avoid the entire cesspool of floating point numbers. It would limit the applicability of your work, though if analysis of number crunching isn't your goal then it's a legitimately pragmatic option. Another point to bear in mind is that even though Eq is widely recognized as denoting an equivalence relation, people sometimes willfully subvert this intention. I'm thinking in particular of the fact that the Num class has, until recently, required an Eq instance--- which in turn precludes some useful/cute Num instances like lifting Num operations over (Num b => a -> b), or implementing powerseries as infinite lists, etc. -- Live well, ~wren

Thanks Wren, for the explanations (also in your previous mail)! On 07/30/2012 01:29 PM, wren ng thornton wrote:

On 7/24/12 9:19 PM, Christian Sternagel wrote:

...

(x == y) = True ==> x = y (x == y) = False ==> not (x = y) (x == _|_) = _|_ (_|_ == y) = _|_

Those axioms state that (==) is sound w.r.t. to meta-equality and strict in both it's arguments.

An immediate problem that arises here is: what exactly does meta-equality denote in Isabelle/HOLCF? If it is meant to denote syntactic identity or Leibniz equality a la Coq, then the first axiom is certainly too strong for any interesting data types (e.g., Rational, Data.Set, Data.Map, Data.IntSet,...) Yes, we also stumbled about this (but I was only discussing it on the isabelle mailing list and not here, sorry). The conclusion was that for many type classes there are several "interesting" (whatever that means) instances. Thus, in the formalization we will use different "formal" type classes for different intended use-cases of Haskell type classes (e.g., one eq class for syntactic equality and another one that merely requires an equivalence relation, ...). That just means that there will not be a bijection between the formal class hierarchy and the actual class hierarchy of Haskell, but should not pose any further problems (I hope).

Btw: I don't agree that the axioms are too strong for *any* interesting data types ;). What about Bool, Int, [a], ...? (Again, this depends on how we interpret "interesting"; in formalizations the threshold for being interesting is typically lower.) cheers chris