Principal engineer at Mercury. I've authored the Dhall configuration language, the Haskell for all blog, and countless packages and keynote presentations.
I'm a midwife to the hidden beauty in everything.
💖 @wiredaemon
Invalid operand type to `=`. Expected `any Comparable`, got `Float`.
yes
(<): { n | ¬isNaN(n) } → { m | ¬isNaN(m) } → Bool
further
x+1 = x //True
?
Secondary Unpopular Opinion™: the Standard does say that equality checking is not a Boolean operation.
the standard actually defines a total ordering on all floating point values!
i feel like not enough people know this
you've probably seen me say it before, but I think == on floats is bad pl design generally. the majority of the times it's used one of the following is true:
Picking an appropriate epsilon value is also often nontrivial. There’s some pretty decent discussion of it here, in the context of figuring out what to do about it in Swift. https://github.com/swiftlang/swift-evolution/blob/main/proposals/0259-approximately-equal.md
It's just pseudocode with syntax I think most people should understand.
That said I did try to port (<): { n | ¬isNaN(n) } → { m | ¬isNaN(m) } → Bool to some actual langs.
I failed to have LiquidHaskell reject invalid uses but Frama-C with Eva, WP and Z3 do support IEEE-754 floats, and the equivalent code is validated:
extern int printf(const char *const retrict, ...);
//@ requires \is_finite(n) && \is_finite(m);
int myLt(float n, float m)
{
return n < m;
}
int main()
{
printf("%d\n%\n",
myLt(5.0, 42.0), //succeeds
myLt(0.0/0.0, 5.0) //Alarm: 1 nan or infinite floating-point value
);
}
But it also kinda complains all the time about NaN and ±∞ so YMMV.