Polymorphism by name for references and continuations

ABSTRACT

This article investigates an ML-like language with byname semantics for polymorphism: polymorphic objects are not evaluated once for all at generalization time, but re-evaluated at each specialization. Unlike the standard ML semantics, the by-name semantics works well with polymorphic references and polymorphic continuations: the naive typing rules for references and for continuations are sound with respect to this semantics. Polymorphism by name leads to a better integration of these imperative features into the ML type discipline. Practical experience shows that it retains most of the efficiency and predictability of polymorphism by value.

REFERENCES

• 1: Andrew W. Appel, Compiling with continuations, Cambridge University Press, New York, NY, 1992
• 2: L. Cardelli. Typeful programming. In E. J. Neuhold and M. Paul, editors, Formal Description of Programming Concepts, pages 431-507. Springer-Verlag, 1989.
• 3: L. Damas. Type assignment in programming lan. guages. PhD thesis, University of Edinburgh, 1985.
• 4: Bruce Duba , Robert Harper , David MacQueen, Typing first-class continuations in ML, Proceedings of the 18th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.163-173, January 21-23, 1991, Orlando, Florida, United States [doi>10.1145/99583.99608]
• 5: M. Felleisen and D. P. Friedman. Control operators, the SECD machine and the ~-calculus. In Formal Description of Programming Concepts III, pages 131-141. North-Holland, 1986.
• 6: David K. Gifford , John M. Lucassen, Integrating functional and imperative programming, Proceedings of the 1986 ACM conference on LISP and functional programming, p.28-38, August 1986, Cambridge, Massachusetts, United States [doi>10.1145/319838.319848]
• 7: R. Harper and M. Lillibridge. ML with callcc is unsound. Message sent to the sral mailing list, July 1991.
• 8: R. Harper and M. Lillibridge. Polymorphic type assignment and CPS conversion. In 1992 SIC- PLAN Continuations Workshop, 1992.
• 9: Robert Harper , Mark Lillibridge, Explicit polymorphism and CPS conversion, Proceedings of the 20th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.206-219, March 1993, Charleston, South Carolina, United States [doi>10.1145/158511.158630]
• 10: X. Leroy. The ZINC experiment: an economical implementation of the ML language. Technical report 117, INRIA, 1990.
• 11: X. Leroy. Typage polymorphe d'un langage algorithmique. Doctoral dissertation (in French), Universit~ Paris 7, 1992.
• 12: X. Leroy and M. Mauny. The Caml Light system, version 0.5- documentation and user's guide. Technical report L-5, INRIA, 1992.
• 13: Xavier Leroy , Pierre Weis, Polymorphic type inference and assignment, Proceedings of the 18th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.291-302, January 21-23, 1991, Orlando, Florida, United States [doi>10.1145/99583.99622]
• 14: Robin Milner , Mads Tofte, Co-induction in relational semantics, Theoretical Computer Science, v.87 n.1, p.209-220, Sept. 16, 1991 [doi>10.1016/0304-3975(91)90033-X]
• 15: Robin Milner , Mads Tofte , Robert Harper, The definition of Standard ML, MIT Press, Cambridge, MA, 1990
• 16: John C. Mitchell, Type systems for programming languages, Handbook of theoretical computer science (vol. B): formal models and semantics, MIT Press, Cambridge, MA, 1991
• 17: John C. Reynolds, Definitional interpreters for higher-order programming languages, Proceedings of the ACM annual conference, p.717-740, August 01-01, 1972, Boston, Massachusetts, United States [doi>10.1145/800194.805852]
• 18: J.-P. Talpin and P. Jouvelot. The type and effect discipline. In Logic in Computer Science 1992. IEEE Computer Society Press, 1992.
• 19: Mads Tofte, Type inference for polymorphic references, Information and Computation, v.89 n.1, p.1-34, Nov. 1990 [doi>10.1016/0890-5401(90)90018-D]
• 20: Andrew K. Wright, Typing references by effect inference, Symposium proceedings on 4th European symposium on programming, p.473-491, January 1992, Rennes, France
• 21: A. K. Wright and M. Felleisen. A syntactic approach to type soundness. Technical report TR91- 160, Rice University, 1991.

INDEX TERMS

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

Additional Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.1 Formal Definitions and Theory
          Subjects: Semantics
      D.3.2 Language Classifications

          Nouns: ML
      D.3.3 Language Constructs and Features
          Subjects: Procedures, functions, and subroutines

  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.3 Studies of Program Constructs
          Subjects: Functional constructs

General Terms:
Algorithms, Languages, Verification