Taming the Flat Float Array Optimization: Tracking Separability in the Type System
OCaml’s flat float array optimization stores floating-point values directly in arrays rather than through pointers, preventing performance degradation for numerical algorithms. However, this optimization requires that all types be \textit{separable} — containing either all float values or none. This restriction prevents certain useful types, such as unboxed existentials and an unboxed version of options. We present the approach taken by OxCaml (OCaml with Jane Street’s extensions) to tracking separability through the type system using a three-valued separability axis. This design enables previously rejected non-separable types while maintaining compatibility with existing code and enabling new optimizations for arrays of known non-float types. Our implementation builds on OxCaml’s kind system but could be adapted to vanilla OCaml.
| Paper (ocaml2025-paper6.pdf) | 374KiB | 
Fri 17 OctDisplayed time zone: Perth change
| 10:30 - 12:15 | |||
| 10:3030m Talk | Taming the Flat Float Array Optimization: Tracking Separability in the Type System OCamlFile Attached | ||
| 11:0030m Talk | A Mechanically Verified Garbage Collector for OCaml OCaml Sheera Shamsu IIT Madras, Dipesh Kafle NIT Trichy, Tiruchirappalli, India, Dhruv Maroo IIT Madras, Chennai, Kartik Nagar IIT Madras, Karthikeyan Bhargavan Cryspen, France, KC Sivaramakrishnan IIT Madras and TaridesLink to publication DOI Pre-print Media Attached File Attached | ||
| 11:3030m Talk | OCaml Package Management with (only!) Dune OCamlFile Attached | ||
