A polymorphic record calculus and its compilation
A polymorphic record calculus and its compilation
复制标题
多态记录演算及其编译
DOI：
10.1145/218570.218572
复制
发表时间：
1995
期刊：
影响因子：
--
通讯作者：
A. Ohori
中科院分区：
文献类型：
--
作者：
A. Ohori
这项工作的动机是提供一个类型理论的基础，开发一个实用的多态编程语言与标记记录和标记的变种。我们的目标是建立一个多态类型的纪律和有效的编译方法与这些标记的数据结构的演算。我们定义了一个二阶，多态记录演算的Girard-Reynolds多态lambda演算的扩展。然后，我们开发了一个ML风格的类型推理算法的谓词子集的二阶记录演算。证明了类型系统的可靠性和类型推理算法的完备性。这些结果扩展了米尔纳的类型推断算法、Damas和米尔纳对ML的let多态性的解释以及哈珀和米切尔对XML的分析。为了建立一个高效的编译方法的多态记录演算，我们首先定义了一个实现演算，记录表示为向量的元素被访问的直接索引，和变量表示为值标记的自然数指示的位置在向量中的功能在开关语句。然后，我们开发了一个算法，利用类型推断算法获得的类型信息，将多态记录演算转换为实现演算。编译算法的正确性证明，即，编译算法保持类型和操作行为的程序。基于这些结果，标准ML已被扩展为带有标记的记录，并已实现其编译器。
The motivation of this work is to provide a type-theoretical basis for developing a practical polymorphic programming language with labeled records and labeled variants. Our goal is to establish both a polymorphic type discipline and an efficient compilation method for a calculus with those labeled data structures. We define a second-order, polymorphic record calculus as an extension of Girard-Reynolds polymorphic lambda calculus. We then develop an ML-style type inference algorithm for a predicative subset of the second-order record calculus. The soundness of the type system and the completeness of the type inference algorithm are shown. These results extend Milner's type inference algorithm, Damas and Milner's account of ML's let polymorphism, and Harper and Mitchell's analysis on XML. To establish an efficient compilation method for the polymorphic record calculus, we first define an implementation calculus, where records are represented as vectors whose elements are accessed by direct indexing, and variants are represented as values tagged with a natural number indicating the position in the vector of functions in a switch statement. We then develop an algorithm to translate the polymorphic record calculus into the implementation calculus using type information obtained by the type inference algorithm. The correctness of the compilation algorithm is proved ; that is, the compilation algorithm is shown to preserve both typing and the operational behavior of a program. Based on these results, Standard ML has been extended with labeled records, and its compiler has been implemented.