-
Notifications
You must be signed in to change notification settings - Fork 251
Description
This issues was originally posted as agda/agda#4865, but I've moved it here, since it's largely an issue with the standard library implementation of strict inequality on floating point numbers.
The strict inequality on floats, induced via toWord
, is deeply unintuitive, featuring greatest hits such as:
_ : False (-1312.0 <? 1312.0)
_ = _
_ : True (1312.0 <? -1312.0)
_ = _
_ : False (-0.0 <? 0.0)
_ = _
_ : True (0.0 <? -0.0)
_ = _
I understand that the numeric equality induces a broken propositional equality, but it may be better to just patch up the numeric order, and face the fact that we don't have a total order, rather than constructing a deeply unintuitive total order, based on the bit representation.
If folks are start using Agda floating-point numbers, and use _<?_
, they will end up being very surprised.
I'm currently working to revisit floating-point numbers agda/agda#4868. In the meantime, I propose we simply remove the derived strict inequality from the standard library.
Activity
[-] Primitive strict inequality on Float is unintuitive [/-][+]Strict inequality on Float is unintuitive [/+]wenkokke commentedon Aug 25, 2020
I should mention that the equality indiced via
toWord
also has its issues, theoretically, since it distinguishes different NaNs. For instance, float32 NaNs are defined as any patterns111 1111 1xxx xxxx xxxx xxxx xxxx xxxx
(withxxx...
being any non-zero number), but the equality via Word distinguishes all of these.(However, I've not been able to find any distinguished NaNs in Agda, which leads me to believe that either the Agda implementation or the Haskell implementation normalises NaNs, or I've not searched hard enough.)
MatthewDaggitt commentedon Aug 26, 2020
That does indeed seem sensible 👍
Just to keep people up to date who aren't reading agda/agda#4868, as I understand it the equality is sound as Agda squashes all the NaNs instances into one in the backend.