"Jacques Carette" <[EMAIL PROTECTED]> writes: > [EMAIL PROTECTED] wrote: >> "Eq" is not merely a function of type a -> a -> Bool. It's a concept >> with semantics. It must be an equivalence relation, and it also must >> mean semantic equality. Functions that respect semantic equality have >> the property that x == y implies f x == f y. >> (No, none of these restrictions are in the language report. But I'd >> be annoyed if someone defined a version of Eq that didn't have these >> properties.) > > From what you argue above, and reading the IEEE 754 standard correctly, > instance Eq Float and instance Eq Double should be *removed* !
For me this indicates that the above is false. It's almost true but not strictly true.
It is deeper than that. It is the difference between extensional equality (which is what the property x == y implies f x == f y is about) versus intensional equality (forall p. p x == p y implies x == y).
+0 and -0 are extensionally equal, but not intensionally equal.
Similarly, 0.0 and sin(0.0) are extensionally equal, but not intensionally equal. A few programming languages (and a few logics) can handle this difference, but they turn out to be quite rare!
Removing instance Eq Double would force removing instances for Ord, Num and all other numeric classes, which is unnacceptable. There would be no instances of Floating left.
:-). Floating point computations are indeed THAT EVIL! They should NOT be considered to be in all those classes! Whoever put them there was not a numerical analyst...
BTW, OCaml recently removed pointer equality check from its implementation of structural equality, because this caused inconsistent results for floats which depended on optimization (a NaN was equal to itself or not depending on whether the compiler knew the type statically or called the general polymorphic equality function).
And there have been complaints about it on the caml-list. Rightfully so, in fact.
NaN is *defined* to be an 'object' x such that not (x == x). In almost all logics or type theories, there are no such objects. It definitely breaks most arguments based on Domains, CPOs, etc. And I say 'objects' because IEEE 754 specifies that there are a whole lot of *different* NaNs, meaning that there are different hardware-level representations.
Jacques
PS: I was manager of the team that implemented a fully IEEE-754/854 compliant numeric sub-system in Maple [Dave Hare was the numerical analyst in charge of that sub-project]. We wrestled with the specification of that sub-system until William Kahan (the Grand Guru of floating point) agreed that it was 'right'. It was a very intense learning experience! _______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
