Taming the Flat Float Array Optimization: Tracking Separability in the Type System
summary
Extends the type/kind system to track three-valued separability axis so the compiler knows whether a type is definitely non-float, definitely float, or unknown. That lets previously-rejected layouts like unboxed existentials and an unboxed non-allocating option appear safely, avoids the per-access float-check and allocations for array get/set when the kind proves non-float, and enables array-specialized codegen instead of the extra branch/heap allocation path. Prototype is implemented in OxCaml kind system and compiles and validates the examples.
AI-written summary · about
chapters (9)
- 0:00Introduction
- 1:02Array representations in OCaml
- 5:00Non-uniform float arrays
- 8:53Float array checks impact
- 13:51Solving runtime with type labels
- 17:08Compile-time separability
- 20:25Tracking separability
- 22:58Real-world Oxaml
- 24:23Q&A
related talks
17mUnboxed types for OCaml
19mPolymorphic Reachability Types: Tracking Freshness, Aliasing, and Separation in(…)
30mLayout Polymorphism: Using static computation to allow efficient polymorphism over...
18mPolymorphic Reachability Types: Tracking Freshness, Aliasing, and Separation in ...
14mFloat Self-Tagging
51mArrays 2.0 - Opportunities and Challenges
58mPortable floating-point calculations
46mThe Calculated Typer (Functional Pearl)