Unifier thinks 0.0 = -0.0 which means you can prove Void
Closed this issue · 8 comments
This isn't my discovery, this is copypasta from discussion on the IRC. Credit to {AS}, scshunt, Melvar and ladyfriday.
enolan at Behemoth in ~/mystuff/code/Idris-dev [master]
$ .cabal-sandbox/bin/idris
____ __ _
/ _/___/ /____(_)____
/ // __ / ___/ / ___/ Version 0.9.19-git:6fc713d
_/ // /_/ / / / (__ ) http://www.idris-lang.org/
/___/\__,_/_/ /_/____/ Type :? for help
Idris is free software with ABSOLUTELY NO WARRANTY.
For details type :warranty.
idris: bind: resource busy (Address already in use)
Idris> the ((False = True) -> Void) (\Refl impossible) $ cong {f = (>0) . (1/)} $ the (-0.0 = 0.0) Refl
case block in {val0} Void Refl Refl : Void
To explain, 1/-0.0 is -Infinity and 1/0.0 is +Infinity, so we have -Infinity = Infinity, False = True, and then Void. The unifier needs to be more precise about what floats are and aren't equal.
This originally came about as a discussion of:
Idris> :let NaN = 0.0 / 0.0
Idris> the (NaN = NaN) Refl
(input):1:5:When elaborating argument x to function Prelude.Basics.the:
Can't unify
x = x
with
NaN = NaN
Specifically:
Can't unify
NaN
with
NaN
Which itself came about in a discussion of how NaN behaves in types (it's interesting when Foo a unifies with Foo a, but Foo NaN doesn't with Foo NaN).
I'll add that the fact that two NaNs won't unify is also potentially an issue, but we weren't able to find a way to get Void from that because, even though you can get NaN = NaN and NaN = NaN -> Void, the two won't unify.
The suggestion in the channel was bit-pattern identity for floats. This would make some NaNs equal, and others not, with no obvious way to tell the difference - I'm a bit worried about that. Also, does't IEEE mandate that NaN compared with anything is always False? On the other hand, worrying too much about the underlying meaning of machine types is perhaps the wrong thing to do, and bit-pattern equality is certainly easy to explain.
The proposal would also make 0.0 and -0.0 unequal, which is good.
IEEE describes an equality test (and indeed a partial order) for floats which includes that negative zero is equal to positive zero, and that every NaN is incomparable with every NaN including itself. However it also describes a total order which will differentiate these cases, including different NaNs, and order them all, in such a way that x < y ⇒ totalOrder x y = LT but not the reverse. See IEEE floating point#Total-ordering predicate. Since it orders every possible float representation, the corresponding equality must be bit-pattern equality.
Which is to say, there is apparently a specific provision for this sort of requirement, and even a stronger one than ours. Now we just have to find implementations.
Interesting!
My feeling about comparisons is that = is definitional equality, and that may differ from == equality. The issue with zeroes in particular means that we shouldn't be afraid to separate them for floating-point types.
The unification thing for NaNs means that writing patterns is hard, but in practice we would be better served by some sort of IsNan predicate or the like.
Since there is no literal form for NaNs, you can’t match on them in the first place.
Edit: Wait, you mean IsNaN : Double -> Type?
Allow me to add a possibly slightly prettier version of the proof at the beginning:
Idris> replace {P = \x => if 1 / x < 0 then () else Void} (the (-0.0 = 0.0) Refl) ()
() : Void
I think that my concerns about bit-pattern identity for NaN were misplaced. We need to distinguish them for the same reason that we need to distinguish -0.0 and 0.0. #3101 does this.