[Prev][Next][Index][Thread]

Polymorphic Record Calculus and Compilation


I thought some of the readers of the mailing list might be interested
in the following paper, which is available through anonymous FTP.
Comments are welcome.

				Atsushi Ohori
				Research Inst. for Mathematical Sciences
				Kyoto University
				Sakyo-ku, Kyoto 606-01, Japan
				Email: ohori@kurims.kyoto-u.ac.jp



"A Polymorphic Record Calculus and its Compilation"
by Atsushi Ohori
(Submitted for publication. Available as a preprint RIMS-1013,
 RIMS, Kyoto University, 1995.
 For anonymous ftp, connect to: ftp.kurims.kyoto-u.ac.jp
 and copy the file: pub/paper/member/ohori/RecordCalc.ps.Z
 using binary mode transfer.)

Abstract:
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 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, POPL92)