On Eq, was Re: [Haskell-cafe] When to use fancy types [Re: NumberTheory library]

[Jacques Carette]

"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!