A static simulation of dynamic delimited control. (English) Zbl 1128.68010
Summary: We present a Continuation-Passing-Style (CPS) transformation for some dynamic delimited-control operators, including Felleisen’s control and prompt, that extends a standard call-by-value CPS transformation. Based on this new transformation, we show how Danvy and Filinski’s static delimited-control operators shift and reset simulate dynamic operators, allaying in passing some skepticism in the literature about the existence of such a simulation. The new CPS transformation and simulation use recursive delimited continuations to avoid undelimited control and the overhead it incurs in implementation and reasoning.
MSC:
| 68N01 | General topics in the theory of software |
Keywords:
Delimited control operators; Macro expressibility; Continuation-passing style; Shift and reset; Control and promptReferences:
| [1] | Abbott, M., Altenkirch, T., Ghani, N., McBride, C.: Derivatives of containers. In: Hofmann, M. (ed.) TLCA 2003: Proceedings of the 6th International Conference on Typed Lambda Calculi and Applications. Lecture Notes in Computer Science, vol. 2701, pp. 16–30. Springer, Berlin (2003) · Zbl 1039.68078 |
| [2] | Ager, M.S., Biernacki, D., Danvy, O., Midtgaard, J.: A functional correspondence between evaluators and abstract machines. In: Proceedings of the 5th International Conference on Principles and Practice of Declarative Programming, pp. 8–19. ACM Press, New York (2003) |
| [3] | Ager, M.S., Danvy, O., Midtgaard, J.: A functional correspondence between call-by-need evaluators and lazy abstract machines. Inf. Process. Lett. 90(5), 223–232 (2004). Extended version available as BRICS Report RS-04-3 · Zbl 1178.68249 · doi:10.1016/j.ipl.2004.02.012 |
| [4] | Ager, M.S., Danvy, O., Midtgaard, J.: A functional correspondence between monadic evaluators and abstract machines for languages with computational effects. Theor. Comput. Sci. 342(1), 149–172 (2005). Extended version available as BRICS Report RS-04-28 · Zbl 1077.68029 · doi:10.1016/j.tcs.2005.06.008 |
| [5] | Ariola, Z.M., Herbelin, H., Sabry, A.: A type-theoretic foundation of continuations and prompts. In: ICFP’04: Proceedings of the ACM International Conference on Functional Programming, pp. 40–53. ACM Press, New York (2004) · Zbl 1323.68090 |
| [6] | Balat, V., Danvy, O.: Memoization in type-directed partial evaluation. In: Batory, D.S., Consel, C., Taha, W. (eds.) Proceedings of GPCE 2002: 1st ACM Conference on Generative Programming and Component Engineering. Lecture Notes in Computer Science, vol. 2487, pp. 78–92. Springer, Berlin (2002) · Zbl 1028.68667 |
| [7] | Balat, V., Di Cosmo, R., Fiore, M.: Extensional normalisation and type-directed partial evaluation for typed lambda calculus with sums. In: POPL’04: Conference Record of the Annual ACM Symposium on Principles of Programming Languages, pp. 64–76. ACM Press, New York (2004) · Zbl 1325.68045 |
| [8] | Barker, C.: Continuations in natural language. In: Thielecke, H. (ed.) CW’04: Proceedings of the 4th ACM SIGPLAN Continuations Workshop, pp. 1–11. Tech. Rep. CSR-04-1, School of Computer Science, University of Birmingham (2004). |
| [9] | Biernacka, M., Danvy, O.: A syntactic correspondence between context-sensitive calculi and abstract machines. Theor. Comput. Sci. 375(1–3), 76–108 (2007) · Zbl 1111.68065 · doi:10.1016/j.tcs.2006.12.028 |
| [10] | Biernacka, M., Biernacki, D., Danvy, O.: An operational foundation for delimited continuations in the CPS hierarchy. Log. Methods Comput. Sci. 1(2:5) (2005) · Zbl 1125.68050 |
| [11] | Biernacki, D., Danvy, O.: From interpreter to logic engine by defunctionalization. In: Bruynooghe, M. (ed.) LOPSTR 2003: 13th International Symposium on Logic Based Program Synthesis and Transformation. Lecture Notes in Computer Science, vol. 3018, pp. 143–159. Springer, Berlin (2004) · Zbl 1099.68546 |
| [12] | Biernacki, D., Danvy, O.: A simple proof of a folklore theorem about delimited control. J. Funct. Program. 16(3), 269–280 (2006) · Zbl 1092.68021 · doi:10.1017/S0956796805005782 |
| [13] | Biernacki, D., Danvy, O., Millikin, K.: A dynamic continuation-passing style for dynamic delimited continuations. Report RS-05-16, BRICS, Denmark (2005) |
| [14] | Biernacki, D., Danvy, O., Shan, C.-c.: On the dynamic extent of delimited continuations. Inf. Process. Lett. 96(1), 7–17 (2005) · Zbl 1191.68157 · doi:10.1016/j.ipl.2005.04.003 |
| [15] | Biernacki, D., Danvy, O., Shan, C.-c.: On the static and dynamic extents of delimited continuations. Sci. Comput. Program. 60(3), 274–297 (2006) · Zbl 1101.68442 · doi:10.1016/j.scico.2006.01.002 |
| [16] | Clinger, W.D.: Proper tail recursion and space efficiency. In: POPL’98: Conference Record of the Annual ACM Symposium on Principles of Programming Languages, pp. 174–185. ACM Press, New York (1998) |
| [17] | Crary, K., Harper, R., Puri, S.: What is a recursive module? In: PLDI’99: Proceedings of the ACM Conference on Programming Language Design and Implementation. ACM SIGPLAN Notices, vol. 34(5), pp. 50–63. ACM Press, New York (1999) |
| [18] | Danvy, O.: Back to direct style. Sci. Comput. Program. 22(3), 183–195 (1994) · Zbl 0808.68051 · doi:10.1016/0167-6423(94)00003-4 |
| [19] | Danvy, O.: Type-directed partial evaluation. In: POPL’96: Conference Record of the Annual ACM Symposium on Principles of Programming Languages, pp. 242–257. ACM Press, New York (1996) |
| [20] | Danvy, O.: On evaluation contexts, continuations, and the rest of the computation. In: Thielecke, H. (ed.) CW’04: Proceedings of the 4th ACM SIGPLAN Continuations Workshop, Tech. Rep. CSR-04-1, School of Computer Science, University of Birmingham (2004) |
| [21] | Danvy, O.: A rational deconstruction of Landin’s SECD machine. In: Grelck, C., Huch, F., Michaelson, G., Trinder, P.W. (eds.) Implementation and Application of Functional Languages: 16th International Workshop, IFL 2004. Lecture Notes in Computer Science, vol. 3474, pp. 52–71. Springer, Berlin (2005) · Zbl 1119.68330 |
| [22] | Danvy, O., Filinski, A.: A functional abstraction of typed contexts. Tech. Rep. 89/12, DIKU, University of Copenhagen, Denmark. http://www.daimi.au.dk/\(\sim\)danvy/Papers/fatc.ps.gz (1989) |
| [23] | Danvy, O., Filinski, A.: Abstracting control. In: Proceedings of the 1990 ACM Conference on Lisp and Functional Programming, pp. 151–160. ACM Press, New York (1990) |
| [24] | Danvy, O., Filinski, A.: Representing control: a study of the CPS transformation. Math. Struct. Comput. Sci. 2(4), 361–391 (1992) · Zbl 0941.00040 · doi:10.1017/S0960129500001535 |
| [25] | Danvy, O., Lawall, J.L.: Back to direct style II: first-class continuations. In: Clinger, W.D. (ed.) Proceedings of the 1992 ACM Conference on Lisp and Functional Programming. Lisp Pointers, vol. V(1), pp. 299–310. ACM Press, New York (1992) |
| [26] | Danvy, O., Nielsen, L.R.: Defunctionalization at work. In: Proceedings of the 3rd International Conference on Principles and Practice of Declarative Programming, pp. 162–174. ACM Press, New York (2001) |
| [27] | Danvy, O., Yang, Z.: An operational investigation of the CPS hierarchy. In: Swierstra, S.D. (ed.) Programming Languages and Systems: Proceedings of ESOP’99, 8th European Symposium on Programming. Lecture Notes in Computer Science, vol. 1576, pp. 224–242. Springer, Berlin (1999) |
| [28] | Double, C.: Partial continuations. http://www.double.co.nz/scheme/partial-continuations/partial- continuations.html (2004) |
| [29] | Dybjer, P., Filinski, A.: Normalization and partial evaluation. In: Barthe, G., Dybjer, P., Pinto, L., Saraiva, J. (eds.) APPSEM 2000: International Summer School on Applied Semantics, Advanced Lectures. Lecture Notes in Computer Science, vol. 2395, pp. 137–192. Springer, Berlin (2002) · Zbl 1065.68026 |
| [30] | Dybvig, R.K., Peyton Jones, S.L., Sabry, A.: A monadic framework for delimited continuations. Tech. Rep. 615, Computer Science Department, Indiana University (2005) · Zbl 1130.68038 |
| [31] | Felleisen, M.: The calculi of {\(\lambda\)} v -CS conversion: a syntactic theory of control and state in imperative higher-order programming languages. Ph.D. thesis, Computer Science Department, Indiana University. Also as Tech. Rep. 226 (1987) |
| [32] | Felleisen, M.: The theory and practice of first-class prompts. In: POPL’88: Conference Record of the Annual ACM Symposium on Principles of Programming Languages, pp. 180–190. ACM Press, New York (1988) |
| [33] | Felleisen, M.: On the expressive power of programming languages. Sci. Comput. Program. 17(1–3), 35–75 (1991) · Zbl 0745.68033 · doi:10.1016/0167-6423(91)90036-W |
| [34] | Felleisen, M., Friedman, D.P.: Control operators, the SECD machine, and the {\(\lambda\)}-calculus. In: Wirsing, M. (ed.) Formal Description of Programming Concepts III, pp. 193–217. Elsevier, Amsterdam (1987) |
| [35] | Felleisen, M., Friedman, D.P., Duba, B.F., Merrill, J.: Beyond continuations. Tech. Rep. 216, Computer Science Department, Indiana University (1987) |
| [36] | Felleisen, M., Wand, M., Friedman, D.P., Duba, B.F.: Abstract continuations: a mathematical semantics for handling full jumps. In: Proceedings of the 1988 ACM Conference on Lisp and Functional Programming, pp. 52–62. ACM Press, New York (1988) |
| [37] | Filinski, A.: Representing monads. In: POPL’94: Conference Record of the Annual ACM Symposium on Principles of Programming Languages, pp. 446–457. ACM Press, New York (1994) |
| [38] | Filinski, A.: Controlling effects. Ph.D. thesis, School of Computer Science, Carnegie Mellon University. Also as Tech. Rep. CMU-CS-96-119 (1996) |
| [39] | Filinski, A.: Representing layered monads. In: POPL’99: Conference Record of the Annual ACM Symposium on Principles of Programming Languages, pp. 175–188. ACM Press, New York (1999) |
| [40] | Filinski, A.: Normalization by evaluation for the computational lambda-calculus. In: Abramsky, S. (ed.) TLCA 2001: Proceedings of the 5th International Conference on Typed Lambda Calculi and Applications. Lecture Notes in Computer Science, vol. 2044, pp. 151–165. Springer, Berlin (2001) · Zbl 0981.68023 |
| [41] | Friedman, D.P., Haynes, C.T.: Constraining control. In: POPL’85: Conference Record of the Annual ACM Symposium on Principles of Programming Languages, pp. 245–254. ACM Press, New York (1985) |
| [42] | Friedman, D.P., Wand, M., Haynes, C.T.: Essentials of Programming Languages, 2nd edn. MIT Press, Cambridge (2001) · Zbl 0994.68020 |
| [43] | Gapeyev, V., Levin, M.Y., Pierce, B.C.: Recursive subtyping revealed. In: ICFP’00: Proceedings of the ACM International Conference on Functional Programming. ACM SIGPLAN Notices, vol. 35(9), pp. 221–231. ACM Press, New York (2000) · Zbl 1025.68017 |
| [44] | Gasbichler, M., Sperber, M.: Final shift for call/cc: direct implementation of shift and reset. In: ICFP’02: Proceedings of the ACM International Conference on Functional Programming, pp. 271–282. ACM Press, New York (2002) |
| [45] | Graunke, P.T.: Web interactions. Ph.D. thesis, College of Computer Science, Northeastern University (2003) · Zbl 1032.68575 |
| [46] | Grobauer, B., Yang, Z.: The second Futamura projection for type-directed partial evaluation. Higher-Order Symb. Comput. 14(2–3), 173–219 (2001) · Zbl 0994.68042 · doi:10.1023/A:1012992731199 |
| [47] | Gunter, C.A., Rémy, D., Riecke, J.G.: A generalization of exceptions and control in ML-like languages. In: Peyton Jones, S.L. (ed.) Functional Programming Languages and Computer Architecture: 7th Conference, pp. 12–23. ACM Press, New York (1995) |
| [48] | Gunter, C.A., Rémy, D., Riecke, J.G.: Return types for functional continuations. http://pauillac.inria.fr/\(\sim\)remy/work/cupto/ (1998) |
| [49] | Hieb, R., Dybvig, R.K.: Continuations and concurrency. In: Proceedings of the 2nd ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming, pp. 128–136. ACM Press, New York (1990) |
| [50] | Hinze, R., Jeuring, J.: Weaving a web. J. Funct. Program. 11(6), 681–689 (2001) · Zbl 1037.68520 |
| [51] | Huet, G.: The zipper. J. Funct. Program. 7(5), 549–554 (1997) · Zbl 0893.68014 · doi:10.1017/S0956796897002864 |
| [52] | Johnson, G.F., Duggan, D.: Stores and partial continuations as first-class objects in a language and its environment. In: POPL’88: Conference Record of the Annual ACM Symposium on Principles of Programming Languages, pp. 158–168. ACM Press, New York (1988) |
| [53] | Kelsey, R., Clinger, W.D., Rees, J., Abelson, H., Dybvig, R.K., Haynes, C.T., Rozas, G.J., Adams IV, N.I., Friedman, D.P., Kohlbecker, E., Steele, G.L., Bartley, D.H., Halstead, R., Oxley, D., Sussman, G.J., Brooks, G., Hanson, C., Pitman, K.M., Wand, M.: Revised5 report on the algorithmic language Scheme. Higher-Order Symb. Comput. 11(1), 7–105 (1998). Also as ACM SIGPLAN Notices 33(9), 26–76 · Zbl 0965.68008 · doi:10.1023/A:1010051815785 |
| [54] | Kiselyov, O.: General ways to traverse collections. http://okmij.org/ftp/Scheme/enumerators-callcc.html ; http://okmij.org/ftp/Computation/Continuations.html (2004) |
| [55] | Kiselyov, O.: How to remove a dynamic prompt: static and dynamic delimited continuation operators are equally expressible. Tech. Rep. 611, Computer Science Department, Indiana University (2005) |
| [56] | Kiselyov, O.: Two-hole zippers and transactions of various isolation modes. Message to the Haskell mailing list; http://okmij.org/ftp/Haskell/Zipper2.lhs ; http://okmij.org/ftp/Computation/Continuations.html (2005) |
| [57] | Kiselyov, O.: Zipper as a delimited continuation. Message to the Haskell mailing list; http://okmij.org/ftp/Haskell/Zipper1.lhs ; http://okmij.org/ftp/Computation/Continuations.html (2005) |
| [58] | Kiselyov, O.: Native delimited continuations in (byte-code) OCaml. http://okmij.org/ftp/ Computation/Continuations.html#caml-shift (2006) |
| [59] | Kiselyov, O., Shan, C.-c., Friedman, D.P., Sabry, A.: Backtracking, interleaving, and terminating monad transformers (functional pearl). In: ICFP’05: Proceedings of the ACM International Conference on Functional Programming, pp. 192–203. ACM Press, New York (2005) · Zbl 1302.68061 |
| [60] | Kiselyov, O., Shan, C.-C., Sabry, A.: Delimited dynamic binding. In: ICFP ’06: Proceedings of the ACM International Conference on Functional Programming, pp. 26–37. ACM Press, New York (2006) · Zbl 1321.68128 |
| [61] | Krivine, J.-L.: Un interpréteur du lambda-calcul. http://www.pps.jussieu.fr/\(\sim\)krivine/articles/interprt.pdf (1985) |
| [62] | Landin, P.J.: The mechanical evaluation of expressions. Comput. J. 6(4), 308–320 (1964) · Zbl 0122.36106 |
| [63] | Lawall, J.L., Danvy, O.: Continuation-based partial evaluation. In: Proceedings of the 1994 ACM Conference on Lisp and Functional Programming, pp. 227–238. ACM Press, New York (1994) |
| [64] | Meyer, A.R., Wand, M.: Continuation semantics in typed lambda-calculi (summary). In: Parikh, R. (ed.) Logics of Programs. Lecture Notes in Computer Science, vol. 193, pp. 219–224. Springer, Berlin (1985) · Zbl 0565.68028 |
| [65] | Moggi, E.: Notions of computation and monads. Inf. Comput. 93(1), 55–92 (1991) · Zbl 0723.68073 · doi:10.1016/0890-5401(91)90052-4 |
| [66] | Murphy VII, T., Crary, K., Harper, R.: Distributed control flow with classical modal logic. In: Ong, C.-H.L. (ed.) Computer Science Logic: 19th International Workshop, CSL 2005. Lecture Notes in Computer Science, vol. 3634, pp. 51–69. Springer, Berlin (2005) · Zbl 1136.68443 |
| [67] | Murthy, C.R.: Control operators, hierarchies, and pseudo-classical type systems: A-translation at work. In: Danvy O., Talcott C. (eds.) CW’92: Proceedings of the ACM SIGPLAN Workshop on Continuations, pp. 49–71. Tech. Rep. STAN-CS-92-1426, Department of Computer Science, Stanford University. ftp://cstr.stanford.edu/pub/cstr/reports/cs/tr/92/1426 (1992) |
| [68] | Plotkin, G.D.: Call-by-name, call-by-value and the {\(\lambda\)}-calculus. Theor. Comput. Sci. 1(2), 125–159 (1975) · Zbl 0325.68006 · doi:10.1016/0304-3975(75)90017-1 |
| [69] | Queinnec, C.: A library of high-level control operators. Lisp Pointers 6(4), 11–26 (1993) · doi:10.1145/181889.181891 |
| [70] | Queinnec, C.: Continuations and web servers. Higher-Order Symb. Comput. 17(4), 277–295 (2004) · doi:10.1007/s10990-004-4866-z |
| [71] | Queinnec, C., Serpette, B.: A dynamic extent control operator for partial continuations. In: POPL’91: Conference Record of the Annual ACM Symposium on Principles of Programming Languages, pp. 174–184. ACM Press, New York (1991) |
| [72] | Reynolds, J.C.: Definitional interpreters for higher-order programming languages. In: Proceedings of the ACM National Conference, vol. 2, pp. 717–740. ACM Press, New York. Reprinted with a foreword in Higher-Order Symb. Comput. 11(4), 363–397 (1972) |
| [73] | Sabry, A., Felleisen, M.: Reasoning about programs in continuation-passing style. Lisp Symb. Comput. 6(3–4), 289–360 (1993) · doi:10.1007/BF01019462 |
| [74] | Sewell, P., Leifer, J.J., Wansbrough, K., Nardelli, F.Z., Allen-Williams, M., Habouzit, P., Vafeiadis, V.: Acute: high-level programming language design for distributed computation. In: ICFP’05: Proceedings of the ACM International Conference on Functional Programming, pp. 15–26. ACM Press, New York (2005) · Zbl 1302.68071 |
| [75] | Shan, C.-c.: Delimited continuations in natural language: quantification and polarity sensitivity. In: Thielecke H. (ed.) CW’04: Proceedings of the 4th ACM SIGPLAN Continuations Workshop, pp. 55–64. Tech. Rep. CSR-04-1, School of Computer Science, University of Birmingham (2004) |
| [76] | Sitaram, D.: Handling control. In: PLDI’93: Proceedings of the ACM Conference on Programming Language Design and Implementation. ACM SIGPLAN Notices, vol. 28(6), pp. 147–155. ACM Press, New York (1993) |
| [77] | Sitaram, D., Felleisen, M.: Control delimiters and their hierarchies. Lisp Symb. Comput. 3(1), 67–99 (1990) · doi:10.1007/BF01806126 |
| [78] | Steele, G.L., Jr.: RABBIT: a compiler for SCHEME. Master’s thesis, Department of Electrical Engineering and Computer Science, Massachusetts Institute of Technology. Also as Memo 474, Artificial Intelligence Laboratory, Massachusetts Institute of Technology (1978) |
| [79] | Strachey, C., Wadsworth, C.P.: Continuations: a mathematical semantics for handling full jumps. Technical Monograph PRG-11, Programming Research Group, Oxford University Computing Laboratory. Reprinted with a foreword in Higher-Order Symb. Comput. 13(1–2), 135–152 (1974) · Zbl 0951.68078 |
| [80] | Sumii, E.: An implementation of transparent migration on standard Scheme. In: Felleisen M. (ed.) Proceedings of the Workshop on Scheme and Functional Programming, pp. 61–63. Tech. Rep. 00-368, Department of Computer Science, Rice University (2000) |
| [81] | Thielecke, H.: Contrasting exceptions and continuations (2001) |
| [82] | Thiemann, P.: Combinators for program generation. J. Funct. Program. 9(5), 483–525 (1999) · Zbl 0945.68029 · doi:10.1017/S0956796899003469 |
| [83] | Wadler, P.L.: Monads and composable continuations. Lisp Symb. Comput. 7(1), 39–56 (1994) · doi:10.1007/BF01019944 |
| [84] | Wand, M.: Continuation-based program transformation strategies. J. ACM 27(1), 164–180 (1980) · Zbl 0429.68028 · doi:10.1145/322169.322183 |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
