一句话：证明 Curry 风格原子多态系统 Fat 的可类型性可判定，并给出能处理非冗余约束的类型推断算法。
本文研究 Girard-Reynolds 多态系统 F 的预测性片段 Fat，其中全称实例化仅允许原子见证。尽管系统 F 的可类型性、类型居留和类型推断均不可判定，且已知 Fat 的类型居留仍不可判定，作者转而分析 Fat 的 Curry 风格变体中的可类型性与类型推断。论文证明该变体的可类型性是可判定的，并构造了一个类型推断算法，该算法能够处理非冗余约束（non-redundancy constraints）。这一结果刻画了原子多态在 Curry 风格下的判定边界，并为相关类型推断问题提供了算法途径。
It is well-known that typability, type inhabitation and type inference are undecidable in the Girard-Reynolds polymorphic system F. It has recently been proven that type inhabitation remains undecidable even in the predicative fragment of system F in which all universal instantiations have an atomic witness (system Fat). In this paper we analyze typability and type inference in Curry style variants of system Fat and show that typability is decidable and that there is an algorithm for type inference which is capable of dealing with non-redundancy constraints.
@article{paperbot1665,
title = {Typability and Type Inference in Atomic Polymorphism},
author = {M. Clarence Protin and Gilda Ferreira},
journal = {Logical Methods in Computer Science},
volume = {Volume 18, Issue 3},
year = {2022},
doi = {10.46298/lmcs-18(3:22)2022}
}