Fabian GiesenFUN 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.
Tristam@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)
@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.
@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.)
@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.
@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 🤷♀️
@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.
@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
Daniel Borges@swiftcoder @rygorous Yes. Considering how failure is handled in Verse, why not have code that produces NaN be a failure?
@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.
@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
+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
@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
@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