package floatml

floatml - IEEE-754 floats for OCaml

Add Float16, Float32, Float64, and Float128 types to OCaml, with full support for arithmetic, comparisons, and conversions to bit representation.

It also provides AnyFloat, which hides the specific float type but will error if mismatched sizes are used together.

This project aims at being a reference implementation of IEEE-754 floating point types in OCaml, with a focus on correctness and completeness.

Implementation

All four formats are evaluated in software by Rust's rustc_apfloat — the LLVM APFloat port that rustc itself uses for compile-time float constant evaluation. This makes every result correctly rounded and bit-for-bit deterministic across every platform, and leans on a battle-tested soft-float rather than a hand-written one.

The numeric core lives in rust/lib.rs (macros generate the bindings for all four precisions); src/floatml.ml is a thin OCaml binding layer over it. Building therefore requires a Rust toolchain (cargo) on PATH in addition to the OCaml dependencies — this is declared to opam via the conf-rust-2021 package.

Performance and allocation

Crossing into Rust is the dominant cost of an operation — the soft-float arithmetic itself is a handful of nanoseconds — so the binding is built to make that crossing as close to free as possible. In native code an operation on Float16, Float32 or Float64 is a direct C call that touches neither the OCaml runtime nor the OCaml heap, and allocates at most the box for its result:

Comparisons, the classification predicates, compare and bits_equal allocate nothing at any precision. Float16 operators allocate nothing either, its bit pattern being an immediate int. Float128 is the outlier: its bit pattern is an (int64 * int64) pair, so every result costs a tuple and two boxed words. Only of_string and the integer conversions, which have to return an option of a bit pattern, allocate more than their result.

The test suite measures Gc.minor_words around each operation and fails if one starts allocating. It also runs twice, once native and once bytecode.

Vendored dependencies

The Rust crate's dependencies are committed under vendor/ and .cargo/config.toml redirects crates.io to them, so the build is fully offline (cargo build --offline --locked) — a requirement for opam's sandboxed CI. To update the Rust dependencies, edit Cargo.toml then re-vendor:

cargo update          # refresh Cargo.lock (optional)
cargo vendor vendor   # re-populate vendor/ to match Cargo.lock

Commit the updated Cargo.lock and vendor/ together.

Coverage

Every operation IEEE 754 requires of a binary format is here, squareRoot included — rustc_apfloat implements no square root, so that one is computed here, in software at all four precisions like everything else.

Arithmetic rounds to nearest-ties-to-even; an explicit rounding direction is taken where IEEE 754 makes it a parameter (roundToIntegral, convertToInteger, convertFromInt, and convertFormat). Note that rem is the IEEE 754 remainder, not C fmod — fmod is available separately.

Beyond that, everything rustc_apfloat exposes that maps to a Rust f64 intrinsic is bound:

What is not available: rustc_apfloat is a correctly-rounded soft-float for the basic operations, not a libm, so there are no transcendentals — no exp, ln, pow, sin, cos or their kin. Note that these have no single right answer to supply: IEEE 754 only recommends correct rounding for them (§9.2), and Rust's own f64::sin dispatches to the platform libm, so its result varies by target. sqrt is the opposite case — §5.4.1 mandates correct rounding, so it has one defined answer, which is why it can be evaluated here at all.

The library is developed for use inside Soteria, where we need concrete reductions for floating point values, that are sound with respect to IEEE-754 semantics (and SMT-lib's FloatingPoint).