一句话：提出结合多态、交并类型与子类型的类型系统，并给出可靠且终止的类型重建算法，适用于动态语言。
针对动态语言中函数常表现出重载与多态行为、且缺少类型标注难以静态检查的问题，本文提出一种受控融合一阶多态、交类型、并类型与子类型的类型系统。系统通过交引入规则表达函数的重载行为，通过并消除规则实现类型收窄，并借助 Hindley–Milner 为未标注函数推断多态类型。作者证明了该类型系统的安全性，并定义了一个可靠且终止的类型重建算法。该工作使静态类型推断能够更好地刻画动态语言程序，为动态语言的类型化提供了理论候选方案。
We present a type system that combines, in a controlled way, first-order polymorphism with intersection types, union types, and subtyping, and prove its safety. We then define a type reconstruction algorithm that is sound and terminating. This yields a system in which unannotated functions are given polymorphic types (thanks to Hindley-Milner) that can express the overloaded behavior of the functions they type (thanks to the intersection introduction rule) and that are deduced by applying advanced techniques of type narrowing (thanks to the union elimination rule). This makes the system a prime candidate to type dynamic languages.
@article{paperbot2596,
title = {Polymorphic Type Inference for Dynamic Languages},
author = {Giuseppe Castagna and Mickaël Laurent and Kim Nguyễn},
journal = {Proceedings of the ACM on Programming Languages},
volume = {8},
number = {POPL},
year = {2024},
doi = {10.1145/3632882}
}