一句话：提出基于类型流分析的简单单态化技术，可处理高阶与存在类型，并证明其类型与语义保持。
单态化是参数多态的常见实现技术，可避免统一表示带来的运行时开销，但会造成代码重复；文献中缺乏通用形式化处理，且通常认为它与高阶多态不兼容。本文提出一种简单的单态化技术，核心是基于类型的流分析来追踪类型实例化在程序中的流动，并借鉴代数子类型思想。该方法可推广到高阶类型、存在类型及其任意组合；仅支持到多态递归，并将多态递归统一检测为循环流。作者还指出存在类型下一种新的多态递归形式，称为 polymorphic packing。元理论结果表明，翻译保持类型，并逐步保持语义。
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{paperbot3171,
title = {The Simple Essence of Monomorphization},
author = {Matthew Lutze and Philipp Schuster and Jonathan Immanuel Brachthäuser},
journal = {Proceedings of the ACM on Programming Languages},
volume = {9},
number = {OOPSLA1},
year = {2025},
doi = {10.1145/3720472}
}