The typed polymorphic label-selective λ-calculus

ABSTRACT

Formal calculi of record structures have recently been a focus of active research. However, scarcely anyone has studied formally the dual notion—i.e., argument-passing to functions by keywords, and its harmonization with currying. We have. Recently, we introduced the label-selective &lgr;-calculus, a conservative extension of &lgr;-calculus that uses a labeling of abstractions and applications to perform unordered currying. In other words, it enables some form of commutation between arguments. This improves program legibility, thanks to the presence of labels, and efficiency, thanks to argument commuting. In this paper, we propose a simply typed version of the calculus, then extend it to one with ML-like polymorphic types. For the latter calculus, we establish the existence of principal types and we give an algorithm to compute them. Thanks to the fact that label-selective &lgr;-calculus is a conservative extension of &lgr;-calculus by adding numeric labels to stand for argument positions, its polymorphic typing provides us with a keyword argument-passing extension of ML obviating the need of records. In this context, conventional ML syntax can be seen as a restriction of the more general keyword-oriented syntax limited to using only implicit positions instead of keywords.

REFERENCES

• 1: M. Abadi , P. L. Curien , J. J. Levy, Explicit substitutions, Proceedings of the 17th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.31-46, December 1989, San Francisco, California, United States [doi>10.1145/96709.96712]
• 2: Hassan Ait-Kaci and Jacques Gardgue. Label-selective )~- calculus. PRL Research report 31, Digital Equipment Corporation, Paris Research Laboratory (May 1993).
• 3: Hassan Aït-Kaci , Jacques Garrigue, Label-selective &lgr;-calculus syntax and confluence, Selected papers of the thirteenth conference on Foundations of software technology and theoretical computer science, p.353-383, November 1995, Bombay, India
• 4: Hassan Ait-Kaci and Andreas Podelski. Towards a meaning of LIFE. Journal of Logic Programming, 16(3-4):195-234 (July-August 1993).
• 5: Kim Bruce, Roberto Di Cosmo, and Giuseppe Longo. Provable isomorphisms of types. Technical Report LIENS-90-14, LIENS (July 1990).
• 6: 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]
• 7: 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]
• 8: 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]
• 9: N.G. de Bruijn. Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, lndag. Math., 34:381-392 (1972).
• 10: Pierre Weis et al. The CAML Reference Manual, version 2.6.1. Projet Formel, INRIA-ENS (1990).
• 11: Jean Gallier and Wayne Snyder. Designing unification procedures using transformations: a survey. In Y. N. Moschovakis, editor, Logic from Computer Science, pages 153-215. Springer- Verlag (1989).
• 12: Jacques Gardgue. Label-selective A-calculus. Rapport de D.E.A., Universit6 Paris VII (1992).
• 13: 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]
• 14: John Lamping, A unified system of parameterization for programming languages, Proceedings of the 1988 ACM conference on LISP and functional programming, p.316-326, July 25-27, 1988, Snowbird, Utah, United States [doi>10.1145/62678.62724]
• 15: Hertry Ledgard. ADA : An Introduction, Ada Reference Manual (July 1980). Springer-Verlag (1981).
• 16: Robin Milner. The polyadic r-calculus: A tutorial. LFCS Report ECS-LFCS-91-180, Laboratory for Foundations of Computer Science, Department of Computer Science, University of Edinburgh (October 1991).
• 17: Martin Odersky , Dan Rabin , Paul Hudak, Call by name, assignment, and the lambda calculus, Proceedings of the 20th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.43-56, March 1993, Charleston, South Carolina, United States [doi>10.1145/158511.158521]
• 18: Atsushi Ohori, A compilation method for ML-style polymorphic record calculi, Proceedings of the 19th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.154-165, January 19-22, 1992, Albuquerque, New Mexico, United States [doi>10.1145/143165.143200]
• 19: 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]
• 20: 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]
• 21: Guy L. Steele, Jr., Common LISP: the language, Digital Press, Newton, MA, 1984
• 22: Mitchell Wand. Complete type inference for simple objects. In Proceedings of IEEE Symposium on Logic in Computer Science (1988).

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
      F.4.1 Mathematical Logic
          Subjects: Lambda calculus and related systems

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

General Terms:
Theory, Verification