Typing record concatenation for free

ABSTRACT

We show that any functional language with record extension possesses record concatenation for free. We exhibit a translation from the latter into the former. We obtain a type system for a language with record concatenation by composing the translation with type-checking in a language with record extension. We apply this method to a version of ML with a record extension and obtain an extension of ML with either asymmetric or symmetric concatenation. The latter extension is simple, flexible and has a very efficient type inference algorithm in practice. Concatenation together with removal of fields needs one more construct than extension of records. It can be added to the version of ML with record extension. However, many typed languages with record cannot type such a construct. The method still applies to them, producing type systems for record concatenation without removal of fields. Object systems also benefit of the encoding which shows that multiple inheritance does not actually require the concatenation of records but only their extension.

REFERENCES

• Car86: L Cardelli, Amber, Proc. of the thirteenth spring school of the LITP on Combinators and functional programming languages, p.21-47, October 1986, Val d'Ajol, France
• CH89: Guy Cousineau and G~rard Huet. The CAM{, Primer. Institut National de Recherche en Informatique et Automatisme, France, 1989.
• 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
• HMT90: Robert Harper, Robin Milner, and Mads ToRe. The definition of Standard ML. The MIT Press, 19!)0.
• HP90a: Robert W. Harper and Benjamin C. Pierce. Extensible records without subsumption. Technical Report CMU-CS-90- 102, Carnegie Mellon University, Pittsburg, Pensylvania, February 1990.
• HP90b: Robert W. Harper and Benjamin C. Pierce. A record calculus based on symmetric concatenation. Technical Report CMU-CS-90- 157, Carnegie Mellon University, Pittsburg, Pensylvania, February 1990.
• 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]
• 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]
• Oho90: Atsushi Ohori. Extending ml polymorphism to record structure. Technical report~ University of Glasgow~ 1990.
• Rém90: Didier l~(~my. Alg~bres To uffues. Application au Typage Polymorphe des Objects Enregistrements dan8 les Langages Fonctionnels. Th~se de doctorat, Universit~ de Paris 7, 1990.
• Rém91a: Didier R~my. Syntactic theories and the algebra of record terms. Technical report~ Inria, Rocquencourt, 1991. To appear. Also in {Remg0a}, chapter 2.
• Rém91b: Didier R~my. Type inference for records in a natural extension of ML. Technical Report 1431, Inria, Rocquencourt, May 1991. Also in {Remg0}, chapter 4.
• Wan87: Mitchell Wand. Complete type inference for simple objects. In Second Symposium on Logic In Computer Science~ 1987.
• Wan88: Mitchell Wand. Corrigendum: Complete type inference for simple objects. In Third Symposium on 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
• Wei89: Pierre Weis. The CAML Reference Manual. Institut National de Recherche en Informatique ct Automatisme, France, 1989.

INDEX TERMS

Primary Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.2 Language Classifications

          Nouns: ML

Additional Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.3 Studies of Program Constructs
          Subjects: Functional constructs; Type structure

General Terms:
Algorithms, Languages