A compilation method for ML-style polymorphic record calculi

ABSTRACT

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 Miler'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.

REFERENCES

• AB87: Malcolm P. Atkinson , O. Peter Buneman, Types and persistence in database programming languages, ACM Computing Surveys (CSUR), v.19 n.2, p.105-170, June 1987 [doi>10.1145/62070.45066]
• BTBO89: Val Breazu-Tannen , Peter Buneman , Atsushi Ohori, Can object-oriented databases be statically typed?, Proceedings of the second international workshop on Database programming languages, p.226-237, December 1989, Salishan Lodge, Gleneden Beach, Oregon, United States
• Car88: Luca Cardelli, A semantics of multiple inheritance, Information and Computation, v.76 n.2-3, p.138-164, February/March 1988 [doi>10.1016/0890-5401(88)90007-7]
• Car91: L. Cardelli. Extensible records in a pure calculus of subtyping. Technical report, DEC Systems Research Center, 1991.
• CDMB89: R. C. H. Conner , A. Dearle , R. Morrison , A. L. Brown, An object addressing mechanism for statically typed languages with multiple inheritance, Conference proceedings on Object-oriented programming systems, languages and applications, p.279-285, October 02-06, 1989, New Orleans, Louisiana, United States
• CM89: Luca Cardelli , John C. Mitchell, Operations on records, Proceedings of the fifth international conference on Mathematical foundations of programming semantics, p.22-52, July 1990, New Orleans, Louisiana, United States
• CW85: Luca Cardelli , Peter Wegner, On understanding types, data abstraction, and polymorphism, ACM Computing Surveys (CSUR), v.17 n.4, p.471-523, Dec. 1985 [doi>10.1145/6041.6042]
• DM82: Luis Damas , Robin Milner, Principal type-schemes for functional programs, Proceedings of the 9th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.207-212, January 25-27, 1982, Albuquerque, Mexico [doi>10.1145/582153.582176]
• Gir71: J.-Y. Girard. Une extension de l'interpretation de gSdel ~ l'analyse, et son application l'61imination des coupures dans l'analyse et th6orie des types. In Second Scandinavian Logic Symposium. North-Holland, 1971.
• GS89: J. H. Gallier , W. Snyder, Complete sets of transformations for general E-unification, Theoretical Computer Science, v.67 n.2-3, p.203-260, Oct. 1989 [doi>10.1016/0304-3975(89)90004-2]
• HP91: Robert Harper , Benjamin Pierce, A record calculus based on symmetric concatenation, Proceedings of the 18th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.131-142, January 21-23, 1991, Orlando, Florida, United States [doi>10.1145/99583.99603]
• JM88: Lalita Jategaonkar , John Mitchell, ML with extended pattern matching and subtypes, Proceedings of the 1988 ACM conference on LISP and functional programming, p.198-211, July 25-27, 1988, Snowbird, Utah, United States [doi>10.1145/62678.62702]
• MH88: J. C. Mitchell , R. Harper, The essence of ML, Proceedings of the 15th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.28-46, January 10-13, 1988, San Diego, California, United States [doi>10.1145/73560.73563]
• Mit84: John C. Mitchell, Coercion and type inference, Proceedings of the 11th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.175-185, January 15-18, 1984, Salt Lake City, Utah, United States [doi>10.1145/800017.800529]
• Mit90: John C. Mitchell, Type systems for programming languages, Handbook of theoretical computer science (vol. B): formal models and semantics, MIT Press, Cambridge, MA, 1991
• MTH90: Robin Milner , Mads Tofte , Robert Harper, The definition of Standard ML, MIT Press, Cambridge, MA, 1990
• OB88: Atsushi Ohori , Peter Buneman, Type inference in a database programming language, Proceedings of the 1988 ACM conference on LISP and functional programming, p.174-183, July 25-27, 1988, Snowbird, Utah, United States [doi>10.1145/62678.62700]
• OB89: A. Ohori , P. Buneman, Static type inference for parametric classes, Conference proceedings on Object-oriented programming systems, languages and applications, p.445-450, October 02-06, 1989, New Orleans, Louisiana, United States
• Oho89a: Atsushi Ohori, A simple semantics for ML polymorphism, Proceedings of the fourth international conference on Functional programming languages and computer architecture, p.281-292, September 11-13, 1989, Imperial College, London, United Kingdom [doi>10.1145/99370.99393]
• Oho89b: Atsushi Ohori , Peter Buneman , Val Breazu-Tannen, A study of semantics, types and languages for databases and object-oriented programming, 1989
• Rém89: D. Rémy, Type checking records and variants in a natural extension of ML, Proceedings of the 16th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.77-88, January 11-13, 1989, Austin, Texas, United States [doi>10.1145/75277.75284]
• Rém90: D. R~my. Typechecking records in a natural extension of ML. Technical report, INRIA-Rocquencourt, Le Chesnay Cedex, France, 1990.
• Rém91: D. R~my. Typing record concatenation for free. Technical report, INRIA-Rocquencourt, Le Chesnay Cedex, France., 1991.
• Rey74: John C. Reynolds, Towards a theory of type structure, Programming Symposium, Proceedings Colloque sur la Programmation, p.408-423, April 09-11, 1974
• Sta88: R. Stansifer, Type inference with subtypes, Proceedings of the 15th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.88-97, January 10-13, 1988, San Diego, California, United States [doi>10.1145/73560.73568]
• Tof88: M. Wofte. Operational Semantics and Polymorphic Type Inference. PhD thesis, Department of Computer Science, University of Edinburgh, 1988.
• Wan87: M. Wand. Complete type inference for simple objects. In Proc. IEEE Symposium on Logic in Computer Science, pages 37- 44, 1987.
• Wan88: M. Wand. Corrigendum: Complete type inference for simple object. In Proc. IEEE Symposium ou Logic in Computer Science, 1988.
• Wan89: M. Wand, Type inference for record concatenatiOn and multiple inheritance, Proceedings of the Fourth Annual Symposium on Logic in computer science, p.92-97, June 1989, Pacific Grove, California, United States

INDEX TERMS

Primary Classification:
  D. Software
  D.1 PROGRAMMING TECHNIQUES

Additional Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.2 Semantics of Programming Languages
          Subjects: Operational semantics
      F.3.3 Studies of Program Constructs
          Subjects: Type structure

General Terms:
Algorithms, Languages, Theory, Verification