一句话：提出带显式类型应用、交集与并集类型的双向高阶多态类型推断，给出可靠、完备、可判定算法并在 Coq 中形式化。
主流语言（如 TypeScript、Flow、Scala）的多态类型系统常带有交集与并集类型，并实现了双向高阶多态类型推断，但既有实现缺乏对非结构子类型以及交集、并集类型的坚实理论。本文研究带显式类型应用、交集与并集类型的双向高阶多态类型推断，揭示这些特性间的非平凡交互。作者给出双向规格的类型系统，证明其良好性质，并设计可靠、完备且可判定的推断算法，刻画出可推断的类型类。论文还探索记录类型与扩大可推断类型集合等实用变体：部分变体虽失去完备性，却提升了表达力。所有结果均在 Coq 中形式化。
Modern mainstream programming languages, such as TypeScript, Flow, and Scala, have polymorphic type systems enriched with intersection and union types. These languages implement variants of bidirectional higher-rank polymorphic type inference, which was previously studied mostly in the context of functional programming. However, existing type inference implementations lack solid theoretical foundations when dealing with non-structural subtyping and intersection and union types, which were not studied before. In this paper, we study bidirectional higher-rank polymorphic type inference with explicit type applications, and intersection and union types and demonstrate that these features have non-trivial interactions. We first present a type system, described by a bidirectional specification, with good theoretical properties and a sound, complete, and decidable algorithm. This is helpful to identify a class of types that can always be inferred. We also explore variants incorporating practical features, such as handling records and inferring a larger class of types, which align better with real-world implementations. Though some variants no longer have a complete algorithm, they still enhance the expressiveness of the type system. To ensure rigor, all results are formalized in the Coq proof assistant.
@article{JiangCO25,
title = {Bidirectional Higher-Rank Polymorphism with Intersection and Union Types},
author = {Shengyi Jiang and Chen Cui and Bruno C. d. S. Oliveira},
journal = {Proceedings of the ACM on Programming Languages},
volume = {9},
number = {POPL},
year = {2025},
doi = {10.1145/3704907}
}