Type inference with rank 1 polymorphism for type-directed compilation of ML
Type inference with rank 1 polymorphism for type-directed compilation of ML
复制标题
用于 ML 类型定向编译的 1 级多态性类型推断
DOI：
10.1145/317636.317796
复制
发表时间：
1999
期刊：
影响因子：
--
通讯作者：
Nobuaki Yoshida
中科院分区：
文献类型：
--
作者：
A. Ohori;Nobuaki Yoshida
本文为ML风格的程序设计语言定义了一个扩展的多态类型系统，并给出了一个完善的类型推理算法。与传统的ML类型规则不同，所提出的类型系统允许完全秩1多态性，其中多态类型可以出现在其他类型中，例如产品类型，不相交的联合类型和函数类型的范围类型。由于这个特性，所提出的类型系统显著地减少了多态性的仅值限制，这是目前大多数ML风格的不纯语言所采用的。它也是高效实现多态类型定向编译的基础。扩展的类型系统实现了更有效的类型推理算法，也有助于开发更有效的多态类型传递实现。我们表明，传统的ML多态性有时会在编译时阐述和运行时类型传递执行时引入指数级开销，并且这些问题可以通过我们的类型推理系统消除。与基于半统一的秩2类型推理系统相比，该算法利用传统的一阶统一方法为任意类型表达式推导出最一般的类型，因此易于在ML语言族的现有实现中采用.
This paper defines an extended polymorphic type system for an ML-style programming language, and develops a sound and complete type inference algorithm. Different frdm the conventional ML type discipline, the proposed type system allows full rank 1 polymorphism, where polymorphic types can appear in other types such as product types, disjoint union types and range types of function types. Because of this feature, the proposed type system significantly reduces the value-only restriction of polymorphism, which is currently adopted in most of ML-style impure languages. It also serves as a basis for efficient implementation of type-directed compilation of polymorphism. The extended type system achieves more efficient type inference algorithm, and it also contributes to develop more efficient type-passing implementation of polymorphism. We show that the conventional ML polymorphism sometimes introduces exponential overhead both at compile-time elaboration and run-time type-passing execution, and that these problems can be eliminated by our type inference system. Compared with a more powerful rank 2 type inference systems based on semi-unification, the proposed type inference algorithm infers a most general type for any typable expression by using the conventional first-order unification, and it is therefore easily adopted in existing implementation of ML family of languages.