Add Ord Laws to next Haskell Report

[George Wilson]

I think we've gotten a bit off-track here. Certainly we have
disagreements about what should be done regarding floating-point
values in GHC over the longer term, but that shouldn't hold up the
report.
I would prefer to see the total order laws added as Daniel suggested,
while documenting that Float and Double have non-lawful instances due
to NaNs. If the handling of doubles is later improved we can simply
delete that line of documentation.

On Fri, 8 Feb 2019 at 08:34, Carter Schonwald
<carter.schonwald at gmail.com> wrote:
>
> additionally (for posterity), merjin pointed out to me that we do want x/0 to not be an exception when abs(x)!= 0, because  +/- infinity are perfectly valid and useful mathematical objects
>
> On Thu, Feb 7, 2019 at 5:31 PM Merijn Verstraaten <merijn at inconsistent.nl> wrote:
>>
>>
>> > On 7 Feb 2019, at 22:41, David Feuer <david.feuer at gmail.com> wrote:
>> >
>> > Even if Ord becomes lawful for floating point, there will still be massive problems reasoning about it because the Num instances can't support the ring laws, let alone the ordered ring laws. What should `compare NaN n` be?
>>
>> Our goal is to make "compare NaN n" impossible to happen. You can only (try) to compare with NaN if you can *get* a NaN value. But IEEE-754 pretty clearly does *NOT* require computations that evaluate to NaN to be represented as values.
>>
>> "Trap representations" (i.e., anything vaguely exception like) are an acceptable IEEE-754 compliant way of implementing NaN. All the major CPU platforms support trapping floating point exceptions, not many languages make use of this.
>>
>> > If it's an exception, then the ordering is not total, you can't store NaN in a Set, etc.
>>
>> I think this argument is without merit. Yes, it would mean you can't store NaN in a Set anymore (because you wouldn't even be able to have a NaN value...). But that's like complaining Int is broken because I can't store "(5 `div` 0)" in a Set. So far everyone seems perfectly ok with the exception raised by division by zero, so why not NaN?
>>
>> > If it's LT or GT, then you get a total ordering, but a rather weird one. So yeah, you'd be able to store NaN in a Set and have an NaN key in a Map, but then as soon as you start looking at where these are coming from and where they're going, everything goes weird and you need type-specific code anyway.
>>
>> If we accept value NaN's (as opposed to trapping NaNs) then we can't have Ord anyway, at least not without giving up on IEEE-754 compliance, as IEEE-754 demands "NaN" compares unequal with itself, which breaks any sort of ordering based function (even simple things like sort, as I painfully discovered in Python...)
>>
>> Cheers,
>> Merijn
>
> _______________________________________________
> Libraries mailing list
> Libraries at haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries