Explicit polymorphism and CPS conversion

ABSTRACT

We study the typing properties of CPS conversion for an extension of F&ohgr; with control operators. Two classes of evaluation strategies are considered, each with call-by-name and call-by-value variants. Under the “standard” strategies, constructor abstractions are values, and constructor applications can lead to non-trivial control effects. In contrast, the “ML-like” strategies evaluate beneath constructor abstractions, reflecting the usual interpretation of programs in languages based on implicit polymorphism. Three continuation passing style sub-languages are considered, one on which the standard strategies coincide, one on which the ML-like strategies coincide, and one on which all strategies coincide. Compositional, type-preserving CPS transformation algorithms are given for the standard strategies, resulting in terms on which all evaluation strategies coincide. This has as a corollary the soundness and termination of well-typed programs under the standard evaluation strategies. A similar result is obtained for the ML-like call-by-name strategy. In contrast, such results are obtained for the call-by-name strategy. In contrast, such results are obtained for the call-by value ML-like strategy only for a restricted sub-language in which constructor abstractions are limited to values.

REFERENCES

• 1: M. Abadi , L. Cardelli , B. Pierce , G. Plotkin, Dynamic typing in a statically-typed language, Proceedings of the 16th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.213-227, January 11-13, 1989, Austin, Texas, United States [doi>10.1145/75277.75296]
• 2: Andrew W. Appel, Compiling with continuations, Cambridge University Press, New York, NY, 1992
• 3: A. W. Appel , T. Jim, Continuation-passing, closure-passing style, Proceedings of the 16th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.293-302, January 11-13, 1989, Austin, Texas, United States [doi>10.1145/75277.75303]
• 4: Luca Cardelli. Typeful programming. Technical Report 45, DEC SRC, 1989.
• 5: Eric C. Cooper and I. Gregory Morrisett. Adding threads to Standard ML. Technical Report CMU-CS-90-186, School of Computer Science, Carnegie Mellon University, December 1990.
• 6: Thierry Coquand , Gerard Huet, The calculus of constructions, Information and Computation, v.76 n.2-3, p.95-120, February/March 1988 [doi>10.1016/0890-5401(88)90005-3]
• 7: Luis Manuel Martins Damas. Type Assignment in Programruing Languages. PhD thesis, Edinburgh University, 1985.
• 8: 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]
• 9: Matthias Felleisen, The calculi of lambda-nu-cs conversion: a syntactic theory of control and state in imperative higher-order programming languages, 1987
• 10: Matthias Felleisen and Daniel Friedman. Control opelators, the SECD machine, and the ,X-calculus. In FormalDescription of Programming Concepts IlL North-Holland, 1986.
• 11: Matthias FeUeisen, Daniel Friedman, Eugene Kohlbeckex; and Bruce Duba. Reasoning with continuations. In First Symposium on Logic in Computer Science. IEEE, June 1986.
• 12: Andrzej Filinski, Linear continuations, Proceedings of the 19th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.27-38, January 19-22, 1992, Albuquerque, New Mexico, United States [doi>10.1145/143165.143174]
• 13: Jean Gallier. On girard's "candidats de reductibilit6". In P. Odifreddi, editor, Logic and Computation, volume 31 of The APIC Series, pages 123-203. Academic Press, 1990.
• 14: Jean-Yves Girard. Interpretation Fonctionelle et l~limination des Coupures dans l'Arithn~tique d'Ordre Supdrieure. PhD thesis, Universit6 Paris VII, 1972.
• 15: Michael Gordon, Robin Milner, and Christopher Wadsworth. Edinburgh LCF: A Mechanized Logic of Computation, volume 78 of Lecture Notes in Computer Science. Springer- Verlag, 1979.
• 16: Timothy G. Griffin, A formulae-as-type notion of control, Proceedings of the 17th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.47-58, December 1989, San Francisco, California, United States [doi>10.1145/96709.96714]
• 17: Timothy G. Griffin. Logical interpretations and computational simulations. Tech. memo., AT&T Bell Laboratories, 1992. in preparation.
• 18: Robert Harper, Bruce Duba, and David MacQueen. Typing first-class continuations in ML. Revised and expandedversion of {8}. To appear, Journal of Functional Programming.
• 19: Robert Harper and Mark LiUibridge. Polymorphic type assignment and eps conversion. In Olivier Danvy and Carolyn Talcott, editors, Proceedings of the ACM SIGPLAN Workshop on Continuations CW92, pages 13-22, Stanford, CA 94305, June 1992. Department of Computer Science, Stanford University. Published as technical report STAN-CS-92-1426.
• 20: Robert Harper , John C. Mitchell, On the type structure of standard ML, ACM Transactions on Programming Languages and Systems (TOPLAS), v.15 n.2, p.211-252, April 1993 [doi>10.1145/169701.169696]
• 21: Christopher T Haynes , Daniel P Friedman , Mitchell Wand, Obtaining coroutines with continuations, Computer Languages, v.11 n.3-4, p.143-153, 1986 [doi>10.1016/0096-0551(86)90007-X]
• 22: Gérard Huet, Logical foundations of functional programming, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1990
• 23: David Kranz , Norman Adams , Richard Kelsey , Jonathan Rees , Paul Hudak , James Philbin, ORBIT: an optimizing compiler for scheme, Proceedings of the 1986 SIGPLAN symposium on Compiler construction, p.219-233, June 25-27, 1986, Palo Alto, California, United States
• 24: Xavier leroy. Polymorphism by name. In Twentieth ACM Symposium on Principles of Programming Languages, January 1993.
• 25: 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]
• 26: Zhaolui Luo, Robert Pollack, and Paul Taylor. How to use lego: A preliminary user's manual. Technical Report LFCS- TN-27, Laboratory for the Foundations of Computer Science, Edinburgh University, October 1989.
• 27: Albert R. Meyer , Mitchell Wand, Continuation Semantics in Typed Lambda-Calculi (Summary), Proceedings of the Conference on Logic of Programs, p.219-224, June 17-19, 1985
• 28: Robin Milner. A theory of type polymorphism in programming languages.Journal of Computer~andSystemSciences, 17:348- 375, 1978.
• 29: Robin Milner , Mads Tofte , Robert Harper, The definition of Standard ML, MIT Press, Cambridge, MA, 1990
• 30: J. C. Mitchell , R. Harper, The essence of ML, Proceedings of the 15th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.28-46, January 10-13, 1988, San Diego, California, United States [doi>10.1145/73560.73563]
• 31: John C. Mitchell, Polymorphic type inference and containment, Information and Computation, v.76 n.2-3, p.211-249, February/March 1988 [doi>10.1016/0890-5401(88)90009-0]
• 32: Chetan Ram Murthy, Extracting constructive content from classical proofs, 1990
• 33: C. Paulin-Mohring, Extracting &ohgr;'s programs from proofs in the calculus of constructions, Proceedings of the 16th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.89-104, January 11-13, 1989, Austin, Texas, United States [doi>10.1145/75277.75285]
• 34: Frank Pfenning, On the undecidability of partial polymorphic type reconstruction, Fundamenta Informaticae, v.19 n.1-2, p.185-199, Sept./Oct. 1993
• 35: Frank Pfenning , Peter Lee, LEAP: A Language with Eval And Polymorphism, Proceedings of the International Joint Conference on Theory and Practice of Software Development, Volume 2: Advanced Seminar on Foundations of Innovative Software Development II and Colloquium on Current Issues in Programming Languages, p.345-359, March 13-17, 1989
• 36: Gordon Plotldn. Call-by-name, call-by-value, and the lambda calculus. Theoretical Computer Science, 1:125-159, 1975.
• 37: John H. Reppy, First-Class Synchronous Operations in Standard ML, Cornell University, Ithaca, NY, 1989
• 38: 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]
• 39: John C. Reynolds, Towards a theory of type structure, Programming Symposium, Proceedings Colloque sur la Programmation, p.408-423, April 09-11, 1974
• 40: John C. Reynolds. Types, abstraction, and parametric polymorphism. In R. E. A. Mason, editor, Information Processing '83, pages 513-523. Elsevier Science Publishers B. V., 1983.
• 41: Guy L. Steele, Jr., Rabbit: A Compiler for Scheme, Massachusetts Institute of Technology, Cambridge, MA, 1978
• 42: Joseph E. Stoy, Denotational Semantics: The Scott-Strachey Approach to Programming Language Theory, MIT Press, Cambridge, MA, 1977
• 43: Christopher Strachey and Christopher Wadsworth. A mathematical semantics for handling full jumps. Technical Report Technical Monograph PRG-11, Oxford University Computing Laboratory, 1974.
• 44: Muds ToRe. Operational Semantics and Polymorphic Type Inference. PhD thesis, FMinburgh University, 1988. Available as Edinburgh University Laboratory for Foundations of Computer Science Technical Report ECS--LFCS-88-54.
• 45: 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]
• 46: Andrew K. Wright and Matthias Felleisen. A syntactic approach to type soundness. Technical Report TR91-160, Depaxtment of Computer Science, Rice University, July 1991. To appear, Information and Computation.

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.3 Language Constructs and Features
          Subjects: Control structures; 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; Control primitives

General Terms:
Algorithms, Languages, Theory, Verification