Add Ord Laws to next Haskell Report

[Carter Schonwald]

true enough

Another cool thing that was pointed out to me, is that for NanFree Floats,
the Projective reals (err, floats) with a single infinity become a new type
over float/double (subject to how reals and floats) release. (thanks to
Wren for that point )

On Thu, Feb 7, 2019 at 5:43 PM George Wilson <george at wils.online> wrote:

> 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
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/libraries/attachments/20190207/874af901/attachment.html>