A Dynamic Continuation-Passing Style for Dynamic Delimited Continuations

Abstract

We put a preexisting definitional abstract machine for dynamic delimited continuations in defunctionalized form, and we present the consequences of this adjustment. We first prove the correctness of the adjusted abstract machine. Because it is in defunctionalized form, we can refunctionalize it into a higher-order evaluation function. This evaluation function, which is compositional, is in continuation+state-passing style and threads a trail of delimited continuations and a meta-continuation. Since this style accounts for dynamic delimited continuations, we refer to it as “dynamic continuation-passing style” and we present the corresponding dynamic CPS transformation. We show that the notion of computation induced by dynamic CPS takes the form of a continuation monad with a recursive answer type. This continuation monad suggests a new simulation of dynamic delimited continuations in terms of static ones. Finally, we present new applications of dynamic delimited continuations, including a meta-circular evaluator. The significance of the present work is that the computational artifacts surrounding dynamic CPS are not independent designs: they are mechanical consequences of having put the definitional abstract machine in defunctionalized form.

References

1. Mads Sig Ager, Dariusz Biernacki, Olivier Danvy, and Jan Midtgaard. 2003. A functional correspondence between evaluators and abstract machines. In Proceedings of the 5th ACM SIGPLAN International Conference on Principles and Practice of Declarative Programming (PPDP’03), Dale Miller (Ed.). ACM, 8--19.
2. Zena M. Ariola, Paul Downen, Hugo Herbelin, Keiko Nakata, and Alexis Saurin. 2012. Classical call-by-need sequent calculi: The unity of semantic artifacts. In Functional and Logic Programming, 11th International Symposium (FLOPS’12) (Lecture Notes in Computer Science), Tom Schrijvers and Peter Thiemann (Eds.). Springer, 32--46.
3. Kenichi Asai and Yukiyoshi Kameyama. 2007. Polymorphic delimited continuations. In Programming Languages and Systems -- 5th Asian Symposium (APLAS’07) (Lecture Notes in Computer Science), Zhong Shao (Ed.). Springer, 239--254.
4. Małgorzata Biernacka, Dariusz Biernacki, and Olivier Danvy. 2005. An operational foundation for delimited continuations in the CPS hierarchy. Logical Methods in Computer Science 1, 2:5 (November 2005), 1--39. A preliminary version was presented at the 4rth ACM SIGPLAN Workshop on Continuations (CW’04).
5. Małgorzata Biernacka and Olivier Danvy. 2007. A syntactic correspondence between context-sensitive calculi and abstract machines. Theoretical Computer Science 375, 1--3 (2007), 76--108. Extended version available as the research report BRICS RS-06-18.
6. Dariusz Biernacki. 2005. The Theory and Practice of Programming Languages with Delimited Continuations. Ph.D. Dissertation. BRICS PhD School, Department of Computer Science, Aarhus University, Aarhus, Denmark.
7. Dariusz Biernacki and Olivier Danvy. 2006. A simple proof of a folklore theorem about delimited control. Journal of Functional Programming 16, 3 (2006), 269--280.
8. Dariusz Biernacki, Olivier Danvy, and Chung-chieh Shan. 2006. On the static and dynamic extents of delimited continuations. Science of Computer Programming 60, 3 (2006), 274--297.
9. Hans-J. Boehm (Ed.). 1994. Proceedings of the 21st Annual ACM Symposium on Principles of Programming Languages. ACM.
10. Robert (Corky) Cartwright (Ed.). 1988. Proceedings of the 1988 ACM Conference on Lisp and Functional Programming. ACM.
11. William Clinger, Daniel P. Friedman, and Mitchell Wand. 1985. A scheme for a higher-level semantic algebra. In Algebraic Methods in Semantics, John Reynolds and Maurice Nivat (Eds.). Cambridge University Press, 237--250.
12. Olivier Danvy. 1994. Back to direct style. Science of Computer Programming 22, 3 (1994), 183--195. A preliminary version was presented at the 4th European Symposium on Programming (ESOP’92).
13. Olivier Danvy. 2006. An Analytical Approach to Programs as Data Objects. Ph.D. Dissertation. Department of Computer Science, Aarhus University, Aarhus, Denmark.
14. Olivier Danvy and Andrzej Filinski. 1989. A Functional Abstraction of Typed Contexts. DIKU Rapport 89/12. DIKU, Computer Science Department, University of Copenhagen, Copenhagen, Denmark.
15. Olivier Danvy and Andrzej Filinski. 1990. Abstracting control. In Proceedings of the 1990 ACM Conference on Lisp and Functional Programming. 151--160.
16. Olivier Danvy and Andrzej Filinski. 1992. Representing control, a study of the CPS transformation. Mathematical Structures in Computer Science 2, 4 (1992), 361--391.
17. Olivier Danvy, Jürgen Koslowski, and Karoline Malmkjær. 1991. Compiling Monads. Technical Report CIS-92-3. Kansas State University, Manhattan, Kansas.
18. Olivier Danvy and Julia L. Lawall. 1992. Back to direct style II: First-class continuations. In Proceedings of the 1992 ACM Conference on Lisp and Functional Programming (LISP Pointers, Vol. V, No. 1), William Clinger (Ed.). ACM Press, 299--310.
19. Olivier Danvy and Karoline Malmkjær. 1988. Intensions and extensions in a reflective tower. In Proceedings of the 1988 ACM Conference on Lisp and Functional Programming. ACM, 327--341.
20. Olivier Danvy and Kevin Millikin. 2008. A rational deconstruction of Landin’s SECD machine with the J operator. Logical Methods in Computer Science 4, 4:12 (November 2008), 1--67.
21. Olivier Danvy and Kevin Millikin. 2009. Refunctionalization at work. Science of Computer Programming 74, 8, 534--549. Extended version available as the research report BRICS RS-08-04.
22. Olivier Danvy and Lasse R. Nielsen. 2001. Defunctionalization at work. In Proceedings of the 3rd International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming (PPDP’01), Harald Søndergaard (Ed.). ACM Press, 162--174. Extended version available as the research report BRICS RS-01-23; most influential paper at PPDP 2001.
23. Olivier Danvy and Ulrik P. Schultz. 2000. Lambda-dropping: Transforming recursive equations into programs with block structure. Theoretical Computer Science 248, 1--2 (2000), 243--287. A preliminary version was presented at the 1997 ACM SIGPLAN Symposium on Partial Evaluation and Semantics-Based Program Manipulation (PEPM’97).
24. Paul Downen and Zena M. Ariola. 2012. A systematic approach to delimited control with multiple prompts. In Programming Languages and Systems, 21st European Symposium on Programming (ESOP’12) (Lecture Notes in Computer Science), Helmut Seidl (Ed.). Springer, 234--253.
25. R. Kent Dybvig, Simon Peyton-Jones, and Amr Sabry. 2007. A monadic framework for subcontinuations. Journal of Functional Programming 17, 6 (2007), 687--730.
26. Matthias Felleisen. 1987. Reflections on Landin’s J operator: A partly historical note. Computer Languages 12, 3/4 (1987), 197--207.
27. Matthias Felleisen. 1988. The theory and practice of first-class prompts. In Proceedings of the 15th Annual ACM Symposium on Principles of Programming Languages. ACM, 180--190.
28. Matthias Felleisen and Daniel P. Friedman. 1986. Control operators, the SECD machine, and the λ-calculus. In Formal Description of Programming Concepts III, Martin Wirsing (Ed.). Elsevier Science Publishers B.V. (North-Holland), Amsterdam, 193--217.
29. Matthias Felleisen, Daniel P. Friedman, Bruce Duba, and John Merrill. 1987. Beyond Continuations. Technical Report 216. Computer Science Department, Indiana University, Bloomington, Indiana.
30. Matthias Felleisen, Mitchell Wand, Daniel P. Friedman, and Bruce F. Duba. 1988. Abstract continuations: A mathematical semantics for handling full functional jumps. In Proceedings of the 1988 ACM Conference on Lisp and Functional Programming. ACM, 52--62.
31. Jeanne Ferrante and Peter Mager (Eds.). 1988. Proceedings of the 15th Annual ACM Symposium on Principles of Programming Languages. ACM.
32. Andrzej Filinski. 1994. Representing monads. In Proceedings of the 21st Annual ACM Symposium on Principles of Programming Languages. ACM, 446--457.
33. Andrzej Filinski. 1996. Controlling Effects. Ph.D. Dissertation. School of Computer Science, Carnegie Mellon University, Pittsburgh, Pennsylvania. Technical Report CMU-CS-96-119.
34. Carl Gunter, Didier Rémy, and Jon G. Riecke. 1995. A generalization of exceptions and control in ML-like languages. In Proceedings of the 7th ACM Conference on Functional Programming Languages and Computer Architecture, Simon Peyton Jones (Ed.). ACM Press, 12--23.
35. Robert Harper, Bruce F. Duba, and David MacQueen. 1993. Typing first-class continuations in ML. Journal of Functional Programming 3, 4 (October 1993), 465--484. A preliminary version was presented at the 18th Annual ACM Symposium on Principles of Programming Languages (POPL’91).
36. John Hatcliff and Olivier Danvy. 1994. A generic account of continuation-passing styles. In Proceedings of the 21st Annual ACM Symposium on Principles of Programming Languages. ACM, 458--471.
37. Robert Hieb and R. Kent Dybvig. 1990. Continuations and concurrency. In Proceedings of the 2nd ACM SIGPLAN Symposium on Principles & Practice of Parallel Programming (SIGPLAN Notices, Vol. 25, No. 3). ACM, 128--136.
38. Robert Hieb, R. Kent Dybvig, and Claude W. Anderson, III. 1993. Subcontinuations. Lisp and Symbolic Computation 5, 4 (December 1993), 295--326.
39. Gregory F. Johnson and Dominic Duggan. 1988. Stores and partial continuations as first-class objects in a language and its environment. In Proceedings of the 15th Annual ACM Symposium on Principles of Programming Languages. ACM, 158--168.
40. Yukiyoshi Kameyama. 2004. Axioms for delimited continuations in the CPS hierarchy. In Computer Science Logic, 18th International Workshop (CSL’04), 13th Annual Conference of the EACSL, Proceedings (Lecture Notes in Computer Science), Jerzy Marcinkowski and Andrzej Tarlecki (Eds.), Vol. 3210. Springer, 442--457.
41. Yukiyoshi Kameyama and Masahito Hasegawa. 2003. A sound and complete axiomatization of delimited continuations. In Proceedings of the 2003 ACM SIGPLAN International Conference on Functional Programming (ICFP’03) (SIGPLAN Notices, Vol. 38, No. 9), Colin Runciman and Olin Shivers (Eds.). ACM, 177--188.
42. Yukiyoshi Kameyama and Takuo Yonezawa. 2008. Typed dynamic control operators for delimited continuations. In Functional and Logic Programming, 9th International Symposium (FLOPS’08) (Lecture Notes in Computer Science), Jacques Garrigue and Manuel V. Hermenegildo (Eds.). Springer, 239--254.
43. Richard Kelsey, William Clinger, and Jonathan Rees, editors. 1998. Revised⁵ report on the algorithmic language scheme. Higher-Order and Symbolic Computation 11, 1 (1998), 7--105.
44. Oleg Kiselyov. 2005. How to Remove a Dynamic Prompt: Static and Dynamic Delimited Continuation Operators are Equally Expressible. Technical Report 611. Computer Science Department, Indiana University, Bloomington, Indiana.
45. Marek Materzok. 2014. Control Abstraction for Layered Continuations: Semantics, Types and Implementation. Ph.D. Dissertation. Department of Mathematics and Computer Science, University of Wrocław, Wrocław, Poland.
46. Marek Materzok and Dariusz Biernacki. 2011. Subtyping delimited continuations. In Proceedings of the 2011 ACM SIGPLAN International Conference on Functional Programming (ICFP’11), Manuel M. T. Chakravarty, Olivier Danvy, and Zhenjiang Hu (Eds.). ACM Press, 81--93.
47. Kevin Millikin. 2007. A Structured Approach to the Transformation, Normalization and Execution of Computer Programs. Ph.D. Dissertation. BRICS PhD School, Department of Computer Science, Aarhus University, Aarhus, Denmark.
48. Robert E. Milne and Christopher Strachey. 1976. A Theory of Programming Language Semantics. Chapman and Hall, London, and John Wiley, New York.
49. Eugenio Moggi. 1991. Notions of computation and monads. Information and Computation 93 (1991), 55--92.
50. Luc Moreau and Christian Queinnec. 1994. Partial continuations as the difference of continuations, a duumvirate of control operators. In 6th International Symposium on Programming Language Implementation and Logic Programming (Lecture Notes in Computer Science), Manuel Hermenegildo and Jaan Penjam (Eds.). Springer-Verlag, 182--197.
51. Chethan R. Murthy. 1992. Control operators, hierarchies, and pseudo-classical type systems: A-translation at work. In Proceedings of the 1st ACM SIGPLAN Workshop on Continuations (CW’92) (Technical report STAN-CS-92-1426, Stanford University), Olivier Danvy and Carolyn L. Talcott (Eds.). 49--72.
52. Christian Queinnec and Bernard Serpette. 1991. A dynamic extent control operator for partial continuations. In Proceedings of the 18th Annual ACM Symposium on Principles of Programming Languages, Robert (Corky) Cartwright (Ed.). ACM, 174--184.
53. John C. Reynolds. 1972. Definitional interpreters for higher-order programming languages. In Proceedings of the 25th ACM National Conference. 717--740. Reprinted in Higher-Order and Symbolic Computation 11, 4 (1998), 363--397, with a foreword {Reynolds 1998}.
54. Chung-chieh Shan. 2007. A static simulation of dynamic delimited control. Higher-Order and Symbolic Computation 20, 4 (2007), 371--401. A preliminary version was presented at the 2004 Workshop on Scheme and Functional Programming.
55. Dorai Sitaram and Matthias Felleisen. 1990a. Control delimiters and their hierarchies. Lisp and Symbolic Computation 3, 1 (January 1990), 67--99.
56. Dorai Sitaram and Matthias Felleisen. 1990b. Reasoning with continuations II: Full abstraction for models of control. In Proceedings of the 1990 ACM Conference on LISP and Functional Programming. ACM, 161--175.
57. Philip Wadler. 1992. Comprehending monads. Mathematical Structures in Computer Science 2, 4 (1992), 461--493.
58. Philip Wadler. 1994. Monads and composable continuations. LISP and Symbolic Computation 7, 1 (January 1994), 39--55.
59. Mitchell Wand (Ed.). 1990. Proceedings of the 1990 ACM Conference on Lisp and Functional Programming. ACM Press.
60. Mitchell Wand and Daniel P. Friedman. 1988. The mystery of the tower revealed: A non-reflective description of the reflective tower. Lisp and Symbolic Computation 1, 1 (May 1988), 11--38. A preliminary version was presented at the 1986 ACM Conference on Lisp and Functional Programming (LFP’86).

Index Terms

• Mathematics of computing

  • Continuous mathematics

    • Calculus

      • Lambda calculus

  • Mathematical analysis

    • Calculus

      • Lambda calculus

• Software and its engineering

  • Software notations and tools

    • General programming languages

      • Language types

        • Functional languages

• Theory of computation

  • Semantics and reasoning

    • Program reasoning

      • Program specifications