Unboxed Data Constructors: Efficient and Safe Big Number Handling in ML Languages

Explore a proposed language feature for ML-family languages that allows selective unboxing of data constructors in this conference talk from POPL'24. Dive into the concept of unboxing data constructors to optimize runtime representation without compromising safety. Learn about the static analysis required to prevent incorrect unboxing and its application to big numbers, enabling both efficient and safe code. Examine the prototype implementation for OCaml, including design choices and interactions with advanced features like Guarded Algebraic Datatypes. Discover the challenges of expanding type definitions in the presence of recursive types, and understand the algorithm developed to detect non-termination during reduction. Draw connections between this termination-monitoring algorithm and the normalization strategy used in cpp preprocessor macro expansion.

[POPL'24] Unboxed data constructors -- or, how cpp decides a halting problem