Projective ML

ABSTRACT

We propose a projective lambda calculus as the basis for operations on records. Projections operate on elevations, that is, records with defaults. This calculus extends lambda calculus while keeping its essential properties. We build projective ML from this calculus by adding the ML Let typing rule to the simply typed projective calculus. We show that projective ML possesses the subject reduction property, which means that well-typed programs can be reduced safely. Elevations are practical data structures that can be compiled efficiently. Moreover, standard records are difinable in terms of projections.

REFERENCES

• Car84: Luca Cardelli, A semantics of multiple inheritance., Proc. of the international symposium on Semantics of data types, p.51-67, July 1984, Sophia-Antipolis, France
• Car91: Luca Cardelli. Extensible records in a pure calculus of subtyping. Private Communication, 1991.
• CG92: M. Coppo and P. Giannini. A complete type inference algorithm for simple intersection types. In Proceedings of European Symposium On Programming, volume 582 of Lecture Notes in Computer Science. Springer Verlag, 1992.
• 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
• Cop80: Mario Coppo, An Extended Polymorphic Type System for Applicative Languages, Proceedings of the 9th Symposium on Mathematical Foundations of Computer Science, p.194-204, September 01-05, 1980
• HP90a: Robert W. Harper and Benjamin C. Pierce. Extensible records without subsumption. Technical Report CMU-CS-90-102, Carnegie Mellon University, Pittsburg, PensyIvania, 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]
• Kir86: Claude Kirchner. Computing unification algorithms. In Proceeding of the first symposium on Logic In Computer Science, pages 206-216, Boston (USA), 1986.
• KJ90: Claude Kirchner and Jean-Pierre Jouannaud. Solving equations in abstract algebras: a rule-based survey of unification. Research Report 561, Universit~ de Paris Sud, Orsay, France, April 1990.
• KK89: Claude Kirchner and Franqois Klay. Syntactic theories and unification. CRIN k iNRIA Loraine, Nancy (France), 1989.
• Ler90: Xavier Leroy. The ZINC experiment: an economical implementation of the ML language. Technical Report 117, INRIA-Rocquencourt, 1990.
• MM82: Alberto Martelli , Ugo Montanari, An Efficient Unification Algorithm, ACM Transactions on Programming Languages and Systems (TOPLAS), v.4 n.2, p.258-282, April 1982 [doi>10.1145/357162.357169]
• 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 poIymorphism to record structure. Technical report, University of Glasgow, 1990.
• Pie91: Benjamin C. Pierce. Programming with intersection types, union types, and polymorphism. Technical Report CMU-CS-91-106, Carnegie Mellon University, Pittsburg, Pensylvania, February 1991.
• Rém89: Didier R~my. Records and variants as a natural extension of ML. In Sixteenth Annual Symposium on Principles Of Programming Languages, 1989.
• Rém90: Didier R~my. Alg~brcs Touffues. Application au Typage Polymorphe des Obyccts Enreg. zstrcmcnts dans los Langages Fonctionncls. Thse de doctorat, Universit~ dc Paris 7, 1990.
• Rém91: Didier R~my. Type inference for records in a natural extension of ML. Technical Report 1431, Inria-Rocquencourt, May 1991. Also in {R~rn90}, chapter 4.
• Rém92a: Didier R~my. Efficient representation of extensible records. In Proceedings of the 1992 ML workshop, 1992.
• Rém92b: Didier R~my. Projective ML. Technical report, BP 105, F-78 153 Le Cha.qnay Codex, BP 105, F-78 153 Le Chesnay Cedex, 1992. To appear.
• Rém92c: Didier Rdmy. Syntactic theories and the algebra of record terms. Technical report, BP 105, F-78 153 Le Chesnay Cedex, BP 105, F- 78 153 Le Chesnay Cedex, 1992. To appear. Also in {R~m90}, chapter 2.
• Rém92d: Didier Rémy, Typing record concatenation for free, Proceedings of the 19th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.166-176, January 19-22, 1992, Albuquerque, New Mexico, United States [doi>10.1145/143165.143202]
• Wan87: Mitchell Wand. Complete type inference for simple objects. In Second Symposium on Logic in Computer Science, 1987.
• 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.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: Type structure
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
      F.4.1 Mathematical Logic
          Subjects: Lambda calculus and related systems

General Terms:
Algorithms, Languages, Verification