Unboxed data constructors -- or, how cpp decides a halting problem
We propose a new language feature for ML-family languages, the ability to selectively unbox certain data constructors, so that their runtime representation gets compiled away to just the identity on their argument.
Unboxing must be statically rejected when it could introduce confusions, that is, distinct values with the same representation.
We discuss the use-case of big numbers, where unboxing allows to write code that is both efficient and safe, replacing either a safe but slow version or a fast but unsafe version.
We explain the static analysis necessary to reject incorrect unboxing requests.
We present our prototype implementation of this feature for the OCaml programming language, discuss several design choices and the interaction with advanced features such as Guarded Algebraic Datatypes.
Our static analysis requires expanding type definitions in type expressions, which is not necessarily normalizing in presence of recursive type definitions. In other words, we must decide normalization of terms in the first-order lambda-calculus with recursion. We provide an algorithm to detect non-termination on-the-fly during reduction, with proofs of correctness and completeness.
Our termination-monitoring algorithm turns out to be closely related to the normalization strategy for macro expansion in the
Fri 19 JanDisplayed time zone: London change
13:20 - 14:40
|When Subtyping Constraints Liberate: A Novel Type Inference Approach for First-Class Polymorphism
Lionel Parreaux HKUST (The Hong Kong University of Science and Technology), Aleksander Boruch-Gruszecki EPFL, Andong Fan HKUST (The Hong Kong University of Science and Technology), Chun Yin Chau HKUST (The Hong Kong University of Science and Technology)DOI Pre-print File Attached
|Parametric Subtyping for Structural Parametric PolymorphismDistinguished PaperRemote
|Unboxed data constructors -- or, how cpp decides a halting problem
|Polymorphic Type Inference for Dynamic Languages
Giuseppe Castagna CNRS; Université Paris Cité, Mickaël Laurent Université Paris Cité / IRIF, Kim Nguyễn Université Paris-SaclayLink to publication DOI