一句话：提出双向类型推断算法，在 Haskell 中无需项标注即可推断存在类型的引入与消除，并采用强存在类型。
与全称类型的成功相比，其对偶——存在类型——在推断与使用上困难得多，却对构造抽象类型、处理索引类型以及一等支持细化类型十分有用。本文以 Haskell 为背景，提出一种双向类型推断算法，能够在项中不含任何标注的情况下推断出在何处引入与消除存在类型，同时给出一个显式类型、类型安全的核心语言，可用作编译目标。该方法的关键在于采用强存在类型（strong existentials），它支持（惰性地）投影出被封装的内部数据，而不是只能通过模式匹配访问的弱存在类型。该方法保持向后兼容。
Despite the great success of inferring and programming with universal types, their dual—existential types—are much harder to work with. Existential types are useful in building abstract types, working with indexed types, and providing first-class support for refinement types. This paper, set in the context of Haskell, presents a bidirectional type-inference algorithm that infers where to introduce and eliminate existentials without any annotations in terms, along with an explicitly typed, type-safe core language usable as a compilation target. This approach is backward compatible. The key ingredient is to use strong existentials, which support (lazily) projecting out the encapsulated data, not weak existentials accessible only by pattern-matching.
@article{paperbot1123,
title = {An existential crisis resolved: type inference for first-class existential types},
author = {Richard A. Eisenberg and Guillaume Duboc and Stephanie Weirich and Daniel Lee},
journal = {Proceedings of the ACM on Programming Languages},
volume = {5},
number = {ICFP},
year = {2021},
doi = {10.1145/3473569}
}