jckarter

everyone already knows i'm a dog

the swift programming language is my fault to some degree. mostly here to see dogs, shitpost, fix old computers, and/or talk about math and weird computer programming things. for effortposts check the #longpost pinned tag. asks are open.


email
mailto:joe@duriansoftware.com
discord
jckarter

Longinus
@Longinus

Invalid operand type to `=`. Expected `any Comparable`, got `Float`.
yes

(<): { n | ¬isNaN(n) } → { m | ¬isNaN(m) } → Bool
further

x+1 = x //True
?


Longinus
@Longinus

Secondary Unpopular Opinion™: the Standard does say that equality checking is not a Boolean operation.


fullmoon
@fullmoon

the standard actually defines a total ordering on all floating point values!

i feel like not enough people know this


You must log in to comment.

in reply to @fullmoon's post:

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:

  1. you're using the float as an int because your PL has bad number types
  2. you actually want to be testing if the values are within some epsilon of each other
  3. you're interested in bitwise equality and want NaN to be equal to NaN
    I feel like the case were you're doing a numeric algorithm where IEEE-754 equality is actually the thing you want a much rarer.

in reply to @Longinus's post:

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.