Unboxed data constructors -- or, how cpp decides a halting problem

on YouTube ↗20m

" summary

Adds selective unboxing to OCaml with a prototype compiler and a static check that rejects unboxings that would create overlapping representations, yielding up to 20% microbenchmark speedup and lower memory use for big integers. The checker computes a syntactic head-shape abstraction of types, expands type definitions by reduction, and runs an on‑the‑fly termination monitor for first‑order lambda normalization that is proven sound and complete. The algorithm mirrors macro expansion strategies in the cpp preprocessor.

AI-written summary · about

" chapters (11)

1. 0:00Unboxed data constructors
2. 1:04Existing unboxing in OCaml
3. 2:49Extending to multiple constructors
4. 4:54Static analysis for unboxing
5. 7:18Head shapes via type normalization
6. 9:01Termination in type normalization
7. 13:17Halting problem decidability
8. 14:44Comparison with model checking
9. 15:55Q&A: Tag elimination
10. 17:24Comparison with Rust optimizations
11. 19:10Q&A: Unboxed record layout