From control effects to typed continuation passing

ABSTRACT

First-class continuations are a powerful computational effect, allowing the programmer to express any form of jumping. Types and effect systems can be used to reason about continuations, both in the source language and in the target language of the continuation-passing transform. In this paper, we establish the connection between an effect system for first-class continuations and typed versions of continuation-passing style. A region in the effect system determines a local answer type for continuations, such that the continuation transforms of pure expressions are parametrically polymorphic in their answer types. We use this polymorphism to derive transforms that make use of effect information, in particular, a mixed linear/non-linear continuation-passing transform, in which expressions without control effects are passed their continuations linearly.

REFERENCES

• 1: Amal Ahmed , David Walker, The logical approach to stack typing, Proceedings of the 2003 ACM SIGPLAN international workshop on Types in languages design and implementation, January 18-18, 2003, New Orleans, Louisiana, USA
• 2: Andrew W. Appel, Compiling with continuations, Cambridge University Press, New York, NY, 1992
• 3: Anindya Banerjee , Nevin Heintze , Jon G. Riecke, Region Analysis and the Polymorphic Lambda Calculus, Proceedings of the 14th Annual IEEE Symposium on Logic in Computer Science, p.88, July 02-05, 1999
• 4: Josh Berdine , Peter O'hearn , Uday Reddy , Hayo Thielecke, Linear Continuation-Passing, Higher-Order and Symbolic Computation, v.15 n.2-3, p.181-208, September 2002 [doi>10.1023/A:1020891112409]
• 5: Carl Bruggeman , Oscar Waddell , R. Kent Dybvig, Representing control in the presence of one-shot continuations, ACM SIGPLAN Notices, v.31 n.5, p.99-107, May 1996
• 6: Olivier Danvy, Formalizing Implementation Strategies for First-Class Continuations, Proceedings of the 9th European Symposium on Programming Languages and Systems, p.88-103, April 02, 2000
• 7: Olivier Danvy and Andrzej Filinski. Representing control, a study of the CPS transformation. Mathematical Structures in Computer Science, 2(4):361--391, December 1992.
• 8: Olivier Danvy , Lasse R. Nielsen, A First-Order One-Pass CPS Transformation, Proceedings of the 5th International Conference on Foundations of Software Science and Computation Structures, p.98-113, April 08-12, 2002
• 9: 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]
• 10: M. Felleisen, The theory and practice of first-class prompts, Proceedings of the 15th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.180-190, January 10-13, 1988, San Diego, California, United States [doi>10.1145/73560.73576]
• 11: Carsten Führmann, Varieties of Effects, Proceedings of the 5th International Conference on Foundations of Software Science and Computation Structures, p.144-158, April 08-12, 2002
• 12: 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]
• 13: Robert Harper and Mark Lillibridge. Polymorphic type assignment and CPS conversion. In Olivier Danvy and Carolyn Talcott, editors, Proceedings of the ACM SIGPLAN Workshop on Continuations CW'92, pages 13--22. Department of Computer Science, Stanford University, June 1992. Published as technical report STAN--CS--92--1426.
• 14: 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]
• 15: P. Jouvelot , D. K. Gifford, Reasoning about continuations with control effects, Proceedings of the ACM SIGPLAN 1989 Conference on Programming language design and implementation, p.218-226, June 19-23, 1989, Portland, Oregon, United States
• 16: H. Abelson , R. K. Dybvig , C. T. Haynes , G. J. Rozas , N. I. Adams Iv , D. P. Friedman , E. Kohlbecker , G. L. Steele, Jr. , D. H. Bartley , R. Halstead , D. Oxley , G. J. Sussman , G. Brooks , C. Hanson , K. M. Pitman , M. Wand, Revised Report on the Algorithmic Language Scheme, Higher-Order and Symbolic Computation, v.11 n.1, p.7-105, August 1998 [doi>10.1023/A:1010051815785]
• 17: J. M. Lucassen , D. K. Gifford, Polymorphic effect systems, Proceedings of the 15th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.47-57, January 10-13, 1988, San Diego, California, United States [doi>10.1145/73560.73564]
• 18: Saunders Mac Lane. Categories for the Working Mathematician. Springer Verlag, 1971.
• 19: 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
• 20: Robin Milner , Mads Tofte , David Macqueen, The Definition of Standard ML, MIT Press, Cambridge, MA, 1997
• 21: Greg Morrisett , David Walker , Karl Crary , Neal Glew, From system F to typed assembly language, Proceedings of the 25th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.85-97, January 19-21, 1998, San Diego, California, United States [doi>10.1145/268946.268954]
• 22: Lasse R. Nielsen. A selective CPS transformation. In 27th Annual Conference on the Mathematical Foundations of Programming Semantics (MFPS), number 45 in ENTCS. Elsevier, 2001.
• 23: Andrew M. Pitts, Parametric polymorphism and operational equivalence, Mathematical Structures in Computer Science, v.10 n.3, p.321-359, June 2000 [doi>10.1017/S0960129500003066]
• 24: John C. Reynolds. Types, abstraction and parametric polymorphism. In R. E. A. Mason, editor, Information Processing 83, pages 513--523, Amsterdam, 1983. Elsevier Science Publishers B. V. (North-Holland).
• 25: Jon G. Riecke , Hayo Thielecke, Typed Exeptions and Continuations Cannot Macro-Express Each Other, Proceedings of the 26th International Colloquium on Automata, Languages and Programming, p.635-644, July 11-15, 1999
• 26: Guy L. Steele, Jr., Rabbit: A Compiler for Scheme, Massachusetts Institute of Technology, Cambridge, MA, 1978
• 27: Mads Tofte , Jean-Pierre Talpin, Implementation of the typed call-by-value λ-calculus using a stack of regions, Proceedings of the 21st ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.188-201, January 16-19, 1994, Portland, Oregon, United States [doi>10.1145/174675.177855]
• 28: Philip Wadler, Theorems for free!, Proceedings of the fourth international conference on Functional programming languages and computer architecture, p.347-359, September 11-13, 1989, Imperial College, London, United Kingdom [doi>10.1145/99370.99404]

INDEX TERMS

Primary Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.1 Formal Definitions and Theory

Additional Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.3 Language Constructs and Features

General Terms:
Languages, Theory

Keywords:
continuations, control effects, polymorphism, type and effect systems