一句话：提出基于多界多态的子类型类型推断系统 F≤ 与算法 SuperF，显著提升一等多态的类型推断能力。
一等/非谓词二阶多态（System F）下的类型推断仍有基本问题，例如可靠地类型检查 (λx.(x 123, x True)) id。本文提出基于多界多态的方法，即带多个下界与上界的隐式多态子类型；定义声明式系统 F≤（源自 Cretin 与 Rémy 的隐式强制转换），并设计 SuperF 算法，在检查 System F 用户注解时推断多态多界 F≤ 类型。为终止推断，SuperF 采用避免递归的启发式，代价是可拒绝少量合法程序，但实践中很少触发。作者表明 SuperF 远比此前所有一等多态类型推断系统强大，显著推进了通用语言类型推断技术水平。
Type inference in the presence of first-class or “ impredicative ” second-order polymorphism à la System F has been an active research area for several decades, with original works dating back to the end of the 80s. Yet, until now many basic problems remain open, such as how to type check expressions like ( λ x . ( x 123 , x True ) ) id reliably. We show that a type inference approach based on multi-bounded polymorphism , a form of implicit polymorphic subtyping with multiple lower and upper bounds, can help us resolve most of these problems in a uniquely simple and regular way. We define F ≤ , a declarative type system derived from the existing theory of implicit coercions by Cretin and Rémy (LICS 2014), and we introduce SuperF, a novel algorithm to infer polymorphic multi-bounded F ≤ types while checking user type annotations written in the syntax of System F. We use a recursion-avoiding heuristic to guarantee termination of type inference at the cost of rejecting some valid programs, which thankfully rarely triggers in practice. We show that SuperF is vastly more powerful than all first-class-polymorphic type inference systems proposed so far, significantly advancing the state of the art in type inference for general-purpose programming languages.
@article{paperbot2611,
title = {When Subtyping Constraints Liberate: A Novel Type Inference Approach for First-Class Polymorphism},
author = {Lionel Parreaux and Aleksander Boruch-Gruszecki and Andong Fan and Chun Yin Chau},
journal = {Proceedings of the ACM on Programming Languages},
volume = {8},
number = {POPL},
year = {2024},
doi = {10.1145/3632890}
}