On Eq, was Re: [Haskell-cafe] When to use fancy types [Re:
NumberTheory library]
Jacques Carette
carette at mcmaster.ca
Fri May 13 14:05:39 EDT 2005
"Marcin 'Qrczak' Kowalczyk" <qrczak at knm.org.pl> wrote:
> "Jacques Carette" <carette at mcmaster.ca> writes:
> > ajb at spamcop.net 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!
More information about the Haskell-Cafe
mailing list