POPL 2024
Sun 14 - Sat 20 January 2024 London, United Kingdom
Fri 19 Jan 2024 14:00 - 14:20 at Kelvin Lecture - Types 3 Chair(s): Steven Ramsay

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 cpp preprocessor.

Fri 19 Jan

Displayed time zone: London change

13:20 - 14:40
Types 3POPL at Kelvin Lecture
Chair(s): Steven Ramsay University of Bristol
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
Henry DeYoung CMU, Andreia Mordido University of Lisbon, Frank Pfenning Carnegie Mellon University, USA, Ankush Das Amazon
Unboxed data constructors -- or, how cpp decides a halting problem
Nicolas Chataing ENS Paris, Stephen Dolan Jane Street, Gabriel Scherer INRIA Saclay, Jeremy Yallop University of Cambridge
Polymorphic Type Inference for Dynamic Languages
Giuseppe Castagna CNRS; Université Paris Cité, Mickaël Laurent Université Paris Cité / IRIF, Kim Nguyễn Université Paris-Saclay
Link to publication DOI