Fabian Giesen
FUN FACT about Verse now that UEFN is out: the floating point is not quite IEEE-754 double, but it's close. Specifically the functional logic programming part of Verse (which is to say, its foundation) requires a few axioms that IEEE floats don't satisfy, so the float semantics are slightly tweaked.
Mar 24, 2023 at 6:12amWeb
Show threadFabian GiesenMar 24, 2023
Specifically
1. Verse really _really_ needs ∀x: x=x to hold or all hell breaks loose, so in Verse all NaNs compare as equal to all other NaNs, and you can check for NaN-ness by testing whether they compare equal to any other known NaN.
2. Likewise, for any x, y and any pure function f, Verse needs x=y => f(x)=f(y). IEEE signed zeros break that (take e.g. f(x)=1/x).
Show threadFabian GiesenMar 24, 2023
IEEE signed zeros still exist under the hood in the VM, but any IEEE operation that could tell +0 and -0 apart (there are not many) needs to canonicalize to one of them (we chose +0).
Show threadFabian GiesenMar 24, 2023
There are still two infinities +∞ and -∞, but e.g. 1/+0 = 1/-0 = +∞.
Show threadsuperjerMar 28, 2023
@rygorous 1/0 is actually neutral infinity (not positive or negative)
Show threadFabian GiesenMar 28, 2023
@superjer Not in IEEE floating point.
Show threadsuperjerMar 28, 2023
@rygorous well then they're missing out!
Show threadFabian GiesenMar 28, 2023
@superjer on the contrary, it was in the drafts as an option (projective closure mode) but removed from the first finalized version of the standard in 1985.
Show threadsuperjerMar 28, 2023
@rygorous ok wow. once again I thought I was making up something stupid enough to be original, but i was wrong
Show threadFabian GiesenMar 28, 2023
@superjer https://en.wikipedia.org/wiki/Compactification_(mathematics)#An_example
Compactification (mathematics) - Wikipedia

Show threadTom ForsythMar 24, 2023
@rygorous As the gods intended!
Show threadTristamMar 24, 2023
@rygorous this is really cool. I’d idly wondered about the feasibility of papering over IEEE float weirdness versus all the hoops we jump through in rust to work around those semantics (not being able to sort arrays of floats out-of-the-box has annoyed me once too often)
Show threadFabian GiesenMar 24, 2023
@swiftcoder Verse floats still have _those_ issues. NaNs are equal to each other but still unordered wrt everything else, so all the caveats of not getting a total order still apply.
Show threadFabian GiesenMar 24, 2023

@swiftcoder we considered making the default order on floats total (by decreeing that NaNs not just equal themselves, but also are > +inf) but ultimately decided against it as probably a bridge too far.

(We already pay an extra cost on FP compares for the current semantics, because there is no way to get "were both operands NaN" out of the standard compare results, so if there was any NaN, we need to do an extra test to detect and handle NaN-vs-NaN.)

Show threadFabian GiesenMar 24, 2023

@swiftcoder Verse floats used to have a total order with NaN < -inf until last year. I argued that if we put NaNs anywhere, it's better to put them at the top, because there's an asymmetry and FP compares idiomatically use abs(x - y) < threshold (or <=) more often that > or >=. NaN < -inf means x-y=NaN => test passes.

Ultimately the NaN=NaN thing and 1/+0 = 1/-0 were necessary for Verse semantics to be consistent, total order was not.

Show threadTristamMar 24, 2023
@rygorous that makes sense. Unfortunate that total ordering is expensive to solve, because it’s extremely rare I’m in a situation where I actually care about NaN ordering - most software by the time you generate a NaN you are thoroughly out of bounds anyway 🤷‍♀️
Show threadFabian GiesenMar 24, 2023
@swiftcoder It's not _that_ expensive (not that different from what we already need) but if you bake it into the semantics of what a floating-point compare is, you need to stick with it on every floating-point compare, and every FP compare between two unknown floats needing an extra rare branch for the "unordered" case (plus fix-up code) adds up in terms of extra insns executed, branch predictor pollution and I$ density.
Show threadFabian GiesenMar 24, 2023
@swiftcoder
That said, both current Verse semantics and total order are much cheaper if you're not comparing two unknown floats, but rather one float against a statically known value (e.g. literal constant). In that case we already know whether said value is or isn't a NaN, and only need to establish whether the other operand is, which can often be decided from a single regular FP compare (i.e. no extra overhead in that case).
Show threadTristamMar 24, 2023
@rygorous Makes sense. I had wondered whether tackling it the other direction could work - introduce a NonNaNf32 type, and then check conversions + all the ops that potentially produce NaNs
Show threadDaniel BorgesMar 24, 2023
@swiftcoder @rygorous Yes. Considering how failure is handled in Verse, why not have code that produces NaN be a failure?
Show threadFabian GiesenMar 24, 2023
@msk @swiftcoder NaN is a value that can be in memory or passed around. Considering NaNs a failure is bad because that would make absolutely everything that works with floats have a "decides" effect.
Show threadFabian GiesenMar 24, 2023
@msk @swiftcoder That is, any function working with any floats would be forced to have a "decides" effect, because all the basic arithmetic ops have ways to produce NaNs from non-NaNs:
+inf + (-inf) is NaN, as is +inf - (+inf) so + and - are out
0*inf is NaN so * is out
0/0 is NaN so / is out
Show threadFabian GiesenMar 24, 2023
@msk @swiftcoder moreover the mere act of looking at the value of a variable produced outside Verse (i.e. native code) would also have a decides effect, or more likely, you would need to have a distinct type for "float, mustn't be NaN" (used inside Verse) and IEEE floats and then converting between them would be "decides", but that basically bifurcates all your numeric code (e.g. vector math libs) between the Verse and non-Verse worlds
Show threadFabian GiesenMar 24, 2023
@msk @swiftcoder It would also imply that not only does every floating-point arithmetic operation have a "decides" side effect, it needs to check for NaNs after every operation; these could be coalesced/sunk down dependent calcs since NaNs propagate but between all of these consequences, this would be hugely disruptive for semantics, ergonomics of using the language, and for code gen.
Show threadDaniel BorgesMar 24, 2023
@rygorous @swiftcoder I didn’t know the orthogonality between decides and computes. However having the ieee float world be distinct of verse float world would imho be a feature, not an issue ^^ marshalling would be weird though
Show threadFabian GiesenMar 24, 2023
@swiftcoder And we didn't feel like we had much of a principled reason for that choice. So we limited changes to what was necessary and kept the partial order in the end.