TY - GEN

T1 - Compilation method for ML-style polymorphic record calculi

AU - Ohori, Atsushi

PY - 1992/12/1

Y1 - 1992/12/1

N2 - Polymorphic record calculi have recently attracted much attention as a typed foundation for object-oriented programming. This is based on the fact that a function that selects a field l of a record can be given a polymorphic type that enables it to be applied to various records containing a field l. Recent studies have established techniques to develop an ML-style type inference algorithm for such a polymorphic type system. There seems to be, however, no established method to compile an ML-style polymorphic record calculus into efficient code. The purpose of this paper is to present one such method. We define a polymorphic record calculus as an extension of Damas and Milner's proof system for ML. For this calculus, we define an implementation calculus where records are represented as arrays of (references to) values and field selection is performed by direct indexing. To represent polymorphic field selection, the implementation calculus contains an abstraction mechanism over indexes. We then develop an algorithm to translate the polymorphic record calculus into the implementation calculus by refining a type inference algorithm; it simultaneously computes a principal type scheme in the polymorphic record calculus and a correct implementation term in the implementation calculus. The type inference is shown to be sound and complete in the sense of Damas-Milner's algorithm for ML. Moreover, the polymorphic type system is shown to be sound with respect to an operational semantics of the translated terms in the implementation calculus.

AB - Polymorphic record calculi have recently attracted much attention as a typed foundation for object-oriented programming. This is based on the fact that a function that selects a field l of a record can be given a polymorphic type that enables it to be applied to various records containing a field l. Recent studies have established techniques to develop an ML-style type inference algorithm for such a polymorphic type system. There seems to be, however, no established method to compile an ML-style polymorphic record calculus into efficient code. The purpose of this paper is to present one such method. We define a polymorphic record calculus as an extension of Damas and Milner's proof system for ML. For this calculus, we define an implementation calculus where records are represented as arrays of (references to) values and field selection is performed by direct indexing. To represent polymorphic field selection, the implementation calculus contains an abstraction mechanism over indexes. We then develop an algorithm to translate the polymorphic record calculus into the implementation calculus by refining a type inference algorithm; it simultaneously computes a principal type scheme in the polymorphic record calculus and a correct implementation term in the implementation calculus. The type inference is shown to be sound and complete in the sense of Damas-Milner's algorithm for ML. Moreover, the polymorphic type system is shown to be sound with respect to an operational semantics of the translated terms in the implementation calculus.

UR - http://www.scopus.com/inward/record.url?scp=0026977485&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=0026977485&partnerID=8YFLogxK

M3 - Conference contribution

AN - SCOPUS:0026977485

SN - 0897914538

T3 - Conference Record of the Annual ACM Symposium on Principles of Programming Languages

SP - 154

EP - 165

BT - Conference Record of the Annual ACM Symposium on Principles of Programming Languages

A2 - Anon, null

PB - Publ by ACM

T2 - 19th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages

Y2 - 19 January 1992 through 22 January 1992

ER -