Skip to content

Strict inequality on Float is unintuitive  #1284

@wenkokke

Description

@wenkokke
Contributor

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

changed the title [-] Primitive strict inequality on Float is unintuitive [/-] [+]Strict inequality on Float is unintuitive [/+] on Aug 25, 2020
wenkokke

wenkokke commented on Aug 25, 2020

@wenkokke
ContributorAuthor

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 pattern s111 1111 1xxx xxxx xxxx xxxx xxxx xxxx (with xxx... 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

MatthewDaggitt commented on Aug 26, 2020

@MatthewDaggitt
Contributor

In the meantime, I propose we simply remove the derived strict inequality from the standard library.

That does indeed seem sensible 👍

I should mention that the equality indiced via toWord also has its issues, theoretically, since it distinguishes different NaNs

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.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Metadata

Metadata

Assignees

No one assigned

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

      Development

      No branches or pull requests

        Participants

        @MatthewDaggitt@wenkokke

        Issue actions

          Strict inequality on Float is unintuitive · Issue #1284 · agda/agda-stdlib