Delimited control in OCaml, abstractly and concretely. (English) Zbl 1244.68015
Summary: We describe the first implementation of multi-prompt delimited control operators in OCaml that is direct in that it captures only the needed part of the control stack. The implementation is a library that requires no changes to the OCaml compiler or run-time, so it is perfectly compatible with existing OCaml source and binary code. The library has been in fruitful practical use since 2006.
We present the library as an implementation of an abstract machine derived by elaborating the definitional machine.
The abstract view lets us distill a minimalistic API, scAPI, sufficient for implementing multi-prompt delimited control. We argue that a language system that supports exception and stack-overflow handling supports scAPI. With byte- and native-code OCaml systems as two examples, our library illustrates how to use scAPI to implement multi-prompt delimited control in a typed language. The approach is general and has been used to add multi-prompt delimited control to other existing language systems.
We present the library as an implementation of an abstract machine derived by elaborating the definitional machine.
The abstract view lets us distill a minimalistic API, scAPI, sufficient for implementing multi-prompt delimited control. We argue that a language system that supports exception and stack-overflow handling supports scAPI. With byte- and native-code OCaml systems as two examples, our library illustrates how to use scAPI to implement multi-prompt delimited control in a typed language. The approach is general and has been used to add multi-prompt delimited control to other existing language systems.
MSC:
| 68N15 | Theory of programming languages |
Software:
OCamlReferences:
| [1] | O. Kiselyov, Native delimited continuations in (byte-code) OCaml, 2006. http://okmij.org/ftp/Computation/Continuations.html#caml-shift; O. Kiselyov, Native delimited continuations in (byte-code) OCaml, 2006. http://okmij.org/ftp/Computation/Continuations.html#caml-shift |
| [2] | Kiselyov, O.; Shan, C.-c.; Sabry, A., Delimited dynamic binding, (ICFP (2006), ACM), 26-37 · Zbl 1321.68128 |
| [3] | Kiselyov, O.; Shan, C.-c., Embedded probabilistic programming, (Proc. IFIP Working Conf. on DSL. Proc. IFIP Working Conf. on DSL, LNCS, vol. 5658 (2009), Springer), 360-384 |
| [4] | Kiselyov, O.; Shan, C.-c., Monolingual probabilistic programming using generalized coroutines, (Uncertainty in Artificial Intelligence (2009), AUAI Press) |
| [5] | O. Kiselyov, Persistent delimited continuations for CGI programming with nested transactions, in: Continuation Fest 2008, 2008. http://okmij.org/ftp/Computation/Continuations.html#shift-cgi; O. Kiselyov, Persistent delimited continuations for CGI programming with nested transactions, in: Continuation Fest 2008, 2008. http://okmij.org/ftp/Computation/Continuations.html#shift-cgi |
| [6] | Kameyama, Y.; Kiselyov, O.; Shan, C.-c., Shifting the stage: staging with delimited control, (PEPM (2009), ACM), 111-120 · Zbl 1248.68132 |
| [7] | O. Kiselyov, C.-c. Shan, Lifted inference: normalizing loops by evaluation, in: Proc. 2009 Workshop on Normalization by Evaluation, BRICS, 2009.; O. Kiselyov, C.-c. Shan, Lifted inference: normalizing loops by evaluation, in: Proc. 2009 Workshop on Normalization by Evaluation, BRICS, 2009. |
| [8] | Anton, K.; Thiemann, P., Towards deriving type systems and implementations for coroutines, (APLAS. APLAS, LNCS, vol. 6461 (2010), Springer), 63-79 |
| [9] | J. Donham, Mixing monadic and direct-style code with delimited continuations, 2010. http://ambassadortothecomputers.blogspot.com/2010/08/mixing-monadic-and-direct-style-code.html; J. Donham, Mixing monadic and direct-style code with delimited continuations, 2010. http://ambassadortothecomputers.blogspot.com/2010/08/mixing-monadic-and-direct-style-code.html |
| [10] | Kiselyov, O., Delimited control in OCaml, abstractly and concretely: system description, (Proc. FLOPS 2010: 10th International Symposium on Functional and Logic Programming, number 6009. Proc. FLOPS 2010: 10th International Symposium on Functional and Logic Programming, number 6009, LNCS (2010), Springer), 304-320 · Zbl 1244.68015 |
| [11] | Gunter, C. A.; Rémy, D.; Riecke, J. G., A generalization of exceptions and control in ML-like languages, (Functional Programming Languages and Computer Architecture (1995), ACM), 12-23 |
| [12] | Dybvig, R. K.; Peyton Jones, S. L.; Sabry, A., A monadic framework for delimited continuations, Journal of Functional Programming, 17, 687-730 (2007) · Zbl 1130.68038 |
| [13] | Balat, V.; Di Cosmo, R.; Fiore, M. P., Extensional normalisation and type-directed partial evaluation for typed lambda calculus with sums, (POPL (2004), ACM), 64-76 · Zbl 1325.68045 |
| [14] | Hieb, R.; Dybvig, R. K.; Bruggeman, C., Representing control in the presence of first-class continuations, (PLDI (1990), ACM), 66-77 |
| [15] | C.A. Gunter, D. Rémy, J.G. Riecke, Return types for functional continuations, 1998. http://pauillac.inria.fr/ remy/work/cupto/; C.A. Gunter, D. Rémy, J.G. Riecke, Return types for functional continuations, 1998. http://pauillac.inria.fr/ remy/work/cupto/ |
| [16] | Danvy, O.; Filinski, A., Abstracting control, (LFP (1990), ACM), 151-160 |
| [17] | Felleisen, M., The theory and practice of first-class prompts, (POPL (1988), ACM), 180-190 |
| [18] | X. Leroy, The ZINC experiment: an economical implementation of the ML language, Technical Report 117, INRIA, 1990.; X. Leroy, The ZINC experiment: an economical implementation of the ML language, Technical Report 117, INRIA, 1990. |
| [19] | Glew, N., Type dispatch for named hierarchical types, (ICFP (1999), ACM), 172-182 · Zbl 1345.68083 |
| [20] | X. Leroy, The bytecode interpreter. version 1.96, byterun/interp.c in OCaml distribution, 2006.; X. Leroy, The bytecode interpreter. version 1.96, byterun/interp.c in OCaml distribution, 2006. |
| [21] | C. Deleuze, Light weight concurrency in OCaml: continuations, monads, events, and friends, 2010.; C. Deleuze, Light weight concurrency in OCaml: continuations, monads, events, and friends, 2010. |
| [22] | X. Leroy, Ocaml-callcc: call/cc for ocaml, 2005. http://pauillac.inria.fr/ xleroy/software.html#callcc; X. Leroy, Ocaml-callcc: call/cc for ocaml, 2005. http://pauillac.inria.fr/ xleroy/software.html#callcc |
| [23] | Gasbichler, M.; Sperber, M., Final shift for call/cc: direct implementation of shift and reset, (ICFP (2002), ACM), 271-282 |
| [24] | Flatt, M.; Yu, G.; Findler, R. B.; Felleisen, M., Adding delimited and composable control to a production programming environment, (ICFP (2007), ACM), 165-176 |
| [25] | Kumar, S.; Bruggeman, C.; Dybvig, R. K., Threads yield continuations, Lisp and Symbolic Computation, 10, 223-236 (1998) |
| [26] | Filinski, A., Representing monads, (POPL (1994), ACM), 446-457 |
| [27] | Masuko, M.; Asai, K., Direct implementation of shift and reset in the MinCaml compiler, (ACM SIGPLAN Workshop on ML (2009), ACM) |
| [28] | Rompf, T.; Maier, I.; Odersky, M., Implementing first-class polymorphic delimited continuations by a type-directed selective CPS-transform, (ICFP (2009), ACM), 317-328 · Zbl 1302.68187 |
| [29] | Clinger, W. D.; Hartheimer, A. H.; Ost, E. M., Implementation strategies for first-class continuations, Higher-Order and Symbolic Computation, 12, 7-45 (1999) · Zbl 0935.68004 |
| [30] | Sekiguchi, T.; Sakamoto, T.; Yonezawa, A., Portable implementation of continuation operators in imperative languages by exception handling, (Advances in Exception Handling Techniques. Advances in Exception Handling Techniques, LNCS, vol. 2022 (2001), Springer), 217-233 · Zbl 0977.68825 |
| [31] | Pettyjohn, G.; Clements, J.; Marshall, J.; Krishnamurthi, S.; Felleisen, M., Continuations from generalized stack inspection, (ICFP (2005), ACM), 216-227 · Zbl 1302.68047 |
| [32] | D. Biernacki, O. Danvy, K. Millikin, A dynamic continuation-passing style for dynamic delimited continuations, Report RS-05-16, BRICS, Denmark, 2005.; D. Biernacki, O. Danvy, K. Millikin, A dynamic continuation-passing style for dynamic delimited continuations, Report RS-05-16, BRICS, Denmark, 2005. |
| [33] | E. Sumii, An implementation of transparent migration on standard Scheme, in: Proc. Workshop on Scheme and Functional Programming, number 00-368 in Tech. Rep., Dept. Computer Science, Rice University, 2000, pp. 61-63.; E. Sumii, An implementation of transparent migration on standard Scheme, in: Proc. Workshop on Scheme and Functional Programming, number 00-368 in Tech. Rep., Dept. Computer Science, Rice University, 2000, pp. 61-63. |
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.
