does anyone know of a programming language which tracks degenerate floating-point numbers at a type level? like tracking "float that can't be NaN" as a separate type from "float that can be NaN"?
- she/her
enthusiast enthusiast
offsite reposts: @nex3-reposts
clips & pics: @nex3-moments
Cohost utilities:
- Image grid generator
- Backloggd formatter
- Letterboxd formatter
- Timeline deduplicator
- Syntax highlighter
header photo by me
You must log in to comment.
in reply to @nex3's post:
I think Rust's Option<T> does what you're looking for?
https://doc.rust-lang.org/stable/std/option/enum.Option.html
oh, yeah, I see what you want. I can't think of any languages that explicitly do things that way for basic types, but as @Anschel points out below, there are ways to accomplish the effect you're looking for?
Generally I just try to structure things in such a way that I'm doing a check if the number is valid in specific points in my computation, so I return (for example) None or my Some<f64> that I can do math on. 🤷♀️
There was some discussion to that effect in rust a few years ago, but I don't think it went anywhere. https://internals.rust-lang.org/t/pre-rfc-nonnan-type/8418/18
I feel like this would incur some pretty serious performance downsides. You'd have to do some kind of check after most (all?) arithmetic operations, which would be generally less efficient than doing one check at the end of your function. That said, someone seems to have done it for Rust
Bill Kahan, at whose feet many of the sins and successes of IEEE 754 may be laid, said that the preferred/performant way of working with NaN was: validate your input, do a sensible amount of computation, then check for NaN at the end.
Yeah, especially given the significant performance overhead of branching on (most?) modern hardware.
well the idea of doing it at the type system level is that you can track where NaN can and can't be without runtime checks
Yeah, but how well can that be checked without knowing the values? Infinity plus negative infinity produces NaN, as do 0/0 and 0*infinity. So literally any arithmetic could take non-NaN input and still produce NaN output.
You might be able to get somewhere with a type that was, say, guaranteed to always be a positive real number. Then you could (I think, don't quote me on this) do everything unchecked except subtraction. But that's obviously quite limiting. At the end of the day, the reason NaN and infinity were included in the standard in the first place is that they come up naturally in situations that are hard to avoid through static analysis.
ETA: even then you'd have to worry about over- and underflows
You might be able to do something with a refinement type system like Liquid Haskell's so that you could state the NaN-generating cases you mention - e.g. the type of division becomes something like NonNaN -> {b : NonNaN | b != 0 } -> NonNaN. You'll then have to propagate these numeric constraints all throughout the program though, which I expect is not going to be fun. I'm also not certain how ready Liquid Haskell is for general use, and don't know of any other refinement type implementations.
If you want to get really niche, languages like AtelierB (used by three people at one French university and for some reason my undergraduate course here in the UK) let you specify pre- and post-conditions on values and could let you state the necessary non-NaN conditions, but I can tell you from experience that AtelierB is deeply unfun to use and not ready for any kind of real programming.
Dependently typed languages as @cactus mentions might also be sufficient to implement this via some sort of float type with bounds on its value - effectively a more general version of the "positive real number" type you suggest. But again the constraint propagation is unlikely to be fun. But at least there are a fair few dependent languages out there with reasonable implementations like Agda.
But yeah, while there are type systems that would theoretically let you enforce these conditions, I expect programming with them is going to be a nightmare.
Even if programming with them were a dream come true due to superb tooling and excellent language ergonomics, the performance will be complete trash on real-world problems.
It is a million-dollar Millennium Prize question whether the Navier-Stokes equations have a singularity in finite time. It would be shocking if a dependent type system could assure us otherwise. (Especially in the face of floating-point approximation errors!)
a brief examination of a handful of dependently typed languages (which seem like they'd be the most likely to do this sort of thing) seems to indicate none of them have a separate NonNaNFloat type or anything. but i may have missed something
Call me NaN-pilled due to my long and traumatic experience in scientific computing, but I think NaN is too baked in to IEEE 754 floats. A performant and computationally useful NaN-less float needs an entirely different design, which then faces the challenge of not having hardware support.
Maybe one question to explore would be, are the scenarios where a NaN-less float is truly necessary amenable to fixed-point arithmetic? Another question to explore is whether or not one can capitalize on Kahan’s recommended computation strategy I mention above by creating a monadic context which takes in NonNaN and spits out Either T NonNaN and uses plain old floats in its interior.
“Just create a monad outside of which all floats are guaranteed to be non-NaN” is a solution I imagine is not going to endear itself to the folks I used to work with who were using Fortran95 as their daily driver, but for a long time those were the folks who needed convincing for anything to catch on in floating point.
Pinned Tags