Paper submitted for publication. Comments are welcome. Available as a preprint RIMS-1013, RIMS, Kyoto Univ., 1995, by anonymous ftp .
Abstract:
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 in this paper 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, which extends Milner's type inference algorithm and Damas and Milner's account of ML's let polymorphism. The soundness of the type system and the completeness of the type inference algorithm are shown. 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 of the code 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.
(A preliminary summary of some of the results of the paper appeared in A. Ohori, A compilation method for ML-style polymorphic record calculi, POPL'92)
Atsushi Ohori, Research Inst. for Mathematical Sciences, Kyoto Univ.
Sakyo-ku, Kyoto 606-01, Japan. Email: ohori@kurims.kyoto-u.ac.jp