论文标题
Freezeml：一流多态性的完整类型推断
FreezeML: Complete and Easy Type Inference for First-Class Polymorphism
论文作者
论文摘要
ML在提供静态键入多态性的情况下是显着的，而无需编程器编写任何类型的注释。这种简约的成本是，程序员仅限于一种多态性形式，其中只有在类型和类型变量的最外层才能发生量词，只能使用单态类型进行实例化。 一般来说，不受限制的系统F风格多态性的推断是不可确定的。然而，文献充斥着一系列提议，以弥合ML和System F之间的差距。 我们提出了一个新的建议Freezeml，这是ML的保守扩展，并具有两个新功能。首先，可以用任意系统F类型注释Let-和Lambda-Binders。其次，可变的发生可能会被冷冻，明确禁用实例化。 Freezeml配备了系统F之间来回的类型传播翻译，并接受类型的推理算法，即算法W的扩展，该算法是声音和完整的，并且产生主类型。
ML is remarkable in providing statically typed polymorphism without the programmer ever having to write any type annotations. The cost of this parsimony is that the programmer is limited to a form of polymorphism in which quantifiers can occur only at the outermost level of a type and type variables can be instantiated only with monomorphic types. Type inference for unrestricted System F-style polymorphism is undecidable in general. Nevertheless, the literature abounds with a range of proposals to bridge the gap between ML and System F. We put forth a new proposal, FreezeML, a conservative extension of ML with two new features. First, let- and lambda-binders may be annotated with arbitrary System F types. Second, variable occurrences may be frozen, explicitly disabling instantiation. FreezeML is equipped with type-preserving translations back and forth between System F and admits a type inference algorithm, an extension of algorithm W, that is sound and complete and which yields principal types.
