u/mttdin r/ProgrammingLanguages • Recommends
The Simple Essence of Monomorphization (OOPSLA 2025)
#monomorphization#polymorphism#typetheory
11K subscribers • 61 videos on Hallway
Advanced. Deep dive for people who know the field.
401 views11 months ago1 recommendation
Programming languagesSystems programmingCompilers and interpretersComputation and complexity
This talk presents a formal treatment of monomorphization based on type-based flow analysis that generalizes to higher-rank and existential types.
The Simple Essence of Monomorphization (Video, OOPSLA1 2025) Matthew Lutze, Philipp Schuster, and Jonathan Immanuel Brachthäuser (Aarhus University, Denmark; University of Tübingen, Germany; University of Tübingen, Germany) Abstract: Monomorphization is a common implementation technique for parametric type-polymorphism, which avoids the potential runtime overhead of uniform representations at the cost of code duplication. While important as a folklore implementation technique, there is a lack of general formal treatments in the published literature. Moreover, it is commonly believed to be incompatible with higher-rank polymorphism. In this paper, we formally present a simple monomorphization technique based on a type-based flow analysis that generalizes to programs with higher-rank types, existential types, and arbitrary combinations. Inspired by algebraic subtyping, we track the flow of type instantiations through the program. Our approach only supports monomorphization up to polymorphic recursion, which we uniformly detect as cyclic flow. Treating universal and existential quantification uniformly, we identify a novel form of polymorphic recursion in the presence of existential types, which we coin polymorphic packing. We study the meta-theory of our approach, showing that our translation is type-preserving and preserves semantics step-wise. Article: doi.org/10.1145/3720472 Supplementary archive: doi.org/10.5281/zenodo.14591555 (Badges: Artifacts Available, Artifacts Evaluated — Reusable, Results Reproduced) ORCID: orcid.org/0000-0002-2904-5099, orcid.org/0000-0001-8011-0506, orcid.org/0000-0001-9128-0391 Video Tags: monomorphization, polymorphic recursion, polymorphic packing, higher-rank types, existential types, oopslaa25main-p140-p, doi:10.1145/3720472, doi:10.5281/zenodo.14591555, orcid:0000-0002-2904-5099, orcid:0000-0001-8011-0506, orcid:0000-0001-9128-0391, Artifacts Available, Artifacts Evaluated — Reusable, Results Reproduced Presentation at the OOPSLA1 2025 conference, October 13–15, 2025.splashcon.org/track/OOPSLA Sponsored by ACM SIGPLAN,What people say. Recommended as a formal and elegant treatment of monomorphization in compiler design.
u/mttdin r/ProgrammingLanguages • Recommends