Didier Rémy
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.
- Car84 Luca Cardelli. A semantics of multiple inheritance. In Semantics of Data Types, volume 173 of Lecture Notes in Computer Science, pages 51-68. Springer Verlag, 1984. Also in Information and Computation, 1988. Google Scholar
Cross Ref
- Car91 Luca Cardelli. Extensible records in a pure calculus of subtyping. Private Communication, 1991.Google Scholar
- 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.Google ScholarCross Ref
- CM89 Luca Cardelli and John C. Mitchell. Operations on records, in Fifth International Conference on Mathematical Foundations of Programming Semantics, 1989. Google ScholarDigital Library
- Cop80 Mario Coppo. An extended polymorphic type system for applicative languages. In MFCS '80, volume 88 of Lecture Notes in Computer Science, pages 194-204. Springer Verlag, 1980. Google Scholar
- 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.Google Scholar
- 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.Google Scholar
- JM88 Lalita A. Jategaonkar and John C. Mitchell. ML with extended pattern matching and subtypes. In Proceed,ngs of the 1988 Conference on LISP and Functional Programming, 1988. Google ScholarDigital Library
- Kir86 Claude Kirchner. Computing unification algorithms. In Proceeding of the first symposium on Logic In Computer Science, pages 206-216, Boston (USA), 1986.Google Scholar
- 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.Google Scholar
- KK89 Claude Kirchner and Franqois Klay. Syntactic theories and unification. CRIN k iNRIA Loraine, Nancy (France), 1989.Google Scholar
- Ler90 Xavier Leroy. The ZINC experiment: an economical implementation of the ML language. Technical Report 117, INRIA-Rocquencourt, 1990.Google Scholar
- MM82 Alberto Martelli and Ugo Montanari. An efficient unification algorithm. ACM Transactions on Programming Languages and Systems, 4(2):258-282, 1982. Google ScholarDigital Library
- OB88 Atsushi Ohori and Peter Buneman. Type inference in a database langage. In A CM Conference on LISP and Functzonal Programmzng, pages 174-183, 1988. Google ScholarDigital Library
- Oho90 Atsushi Ohori. Extending ML poIymorphism to record structure. Technical report, University of Glasgow, 1990.Google Scholar
- 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.Google Scholar
- Rém89 Didier R~my. Records and variants as a natural extension of ML. In Sixteenth Annual Symposium on Principles Of Programming Languages, 1989.Google Scholar
- 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.Google Scholar
- 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.Google Scholar
- Rém92a Didier R~my. Efficient representation of extensible records. In Proceedings of the 1992 ML workshop, 1992.Google Scholar
- 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.Google Scholar
- 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.Google Scholar
- Rém92d Didier R~my. Typing record concatenation for free. In Nineteenth Annual Symposium on Principles Of Programming Languages, 1992. Google ScholarDigital Library
- Wan87 Mitchell Wand. Complete type inference for simple objects. In Second Symposium on Logic in Computer Science, 1987.Google Scholar
- Wan89 Mitchell Wand. Type inference for record concatenation and multiple inheritance. In Fourth Annual Symposium on Logic In Computer Science, pages 92-97, 1989. Google ScholarDigital Library
Index Terms
- Projective ML
Recommendations
Projective ML
LFP '92: Proceedings of the 1992 ACM conference on LISP and functional programmingWe 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 ...
The essence of ML
POPL '88: Proceedings of the 15th ACM SIGPLAN-SIGACT symposium on Principles of programming languagesStandard ML is a useful programming language with polymorphic expressions and a flexible module facility. One notable feature of the expression language is an algorithm which allows type information to be omitted. We study the implicitly-typed ...
A compilation method for ML-style polymorphic record calculi
POPL '92: Proceedings of the 19th ACM SIGPLAN-SIGACT symposium on Principles of programming languagesPolymorphic 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 ...
Comments