Abstract
Regions are a useful tool for the safe and automatic management of resources. Due to their scarcity, resources are often limited in their lifetime which is associated with a certain scope. When control flow leaves the scope, the resources are released. Exceptions can non-locally exit such scopes and it is important that resources are also released in this case.
Continuation-passing style is a useful compiler intermediate language that makes control flow explicit. All calls are tail calls and the runtime stack is not used. It can also serve as an implementation technique for control effects like exceptions. In this case throwing an exception means jumping to a continuation which is not the current one.
How is it possible to offer region-based resource management and exceptions in the same language and translate both to continuation-passing style? In this paper, we answer this question. We present a typed language with resources and exceptions, and its translation to continuation-passing style. The translation can be defined modularly for resources and exceptions – the correct interaction between the two automatically arises from simple composition. We prove that the translation preserves well-typedness and semantics.
Chapter PDF
Similar content being viewed by others
References
Ahman, D., Bauer, A.: Runners in action. In: Müller, P. (ed.) Programming Languages and Systems, pp. 29–55, Springer International Publishing, Cham (2020)
Appel, A.W.: Compiling with Continuations. Cambridge University Press, New York, NY, USA (1992), ISBN 0-521-41695-7
Bertot, Y., Castéran, P.: Interactive Theorem Proving and Program Development, Coq’Art:The Calculus of Inductive Constructions. Springer-Verlag (2004)
Biernacki, D., Piróg, M., Polesiuk, P., Sieczkowski, F.: Abstracting algebraic effects. Proc. ACM Program. Lang. 3(POPL), 6:1–6:28 (Jan 2019)
Biernacki, D., Piróg, M., Polesiuk, P., Sieczkowski, F.: Binders by day, labels by night: Effect instances via lexically scoped handlers. Proc. ACM Program. Lang. 4(POPL) (Dec 2019), https://doi.org/10.1145/3371116
Brachthäuser, J.I., Schuster, P., Ostermann, K.: Effects as capabilities: Effect handlers and lightweight effect polymorphism. Proc. ACM Program. Lang. 4(OOPSLA) (Nov 2020), https://doi.org/10.1145/3428194
Brady, E.: Idris 2: Quantitative type theory in action. Tech. rep., University of St Andrews, Scotland, UK (2020), URL https://www.type-driven.org.uk/edwinb/papers/idris2.pdf
Cong, Y., Osvald, L., Essertel, G.M., Rompf, T.: Compiling with continuations, or without? whatever. Proc. ACM Program. Lang. 3(ICFP), 79:1–79:28 (Jul 2019), https://doi.org/10.1145/3341643
Crary, K., Walker, D., Morrisett, G.: Typed memory management in a calculus of capabilities. In: Proceedings of the 26th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, p. 262–275, POPL ’99, Association for Computing Machinery, New York, NY, USA (1999), https://doi.org/10.1145/292540.292564
Danvy, O.: On evaluation contexts, continuations, and the rest of computation (02 2004)
Danvy, O., Filinski, A.: Abstracting control. In: Proceedings of the Conference on LISP and Functional Programming, pp. 151–160, ACM, New York, NY, USA (1990)
Fluet, M., Morrisett, G.: Monadic regions. In: Proceedings of the Ninth ACM SIGPLAN International Conference on Functional Programming, p. 103–114, ICFP ’04, Association for Computing Machinery, New York, NY, USA (2004), https://doi.org/10.1145/1016850.1016867
Fluet, M., Morrisett, G., Ahmed, A.: Linear regions are all you need. In: Sestoft, P. (ed.) Programming Languages and Systems, pp. 7–21, Springer Berlin Heidelberg, Berlin, Heidelberg (2006)
Grossman, D., Morrisett, G., Jim, T., Hicks, M., Wang, Y., Cheney, J.: Region-based memory management in cyclone. In: Proceedings of the ACM SIGPLAN 2002 Conference on Programming Language Design and Implementation, p. 282–293, PLDI ’02, Association for Computing Machinery, New York, NY, USA (2002), https://doi.org/10.1145/512529.512563
Hillerström, D., Lindley, S., Atkey, B., Sivaramakrishnan, K.: Continuation passing style for effect handlers. In: Formal Structures for Computation and Deduction, LIPIcs, vol. 84, Schloss Dagstuhl–Leibniz-Zentrum für Informatik (2017)
Hillerström, D., Lindley, S., Atkey, R.: Effect handlers via generalised continuations. Journal of Functional Programming 30, e5 (2020), https://doi.org/10.1017/S0956796820000040
Kennedy, A.: Compiling with continuations, continued. In: Proceedings of the International Conference on Functional Programming, pp. 177–190, ACM, New York, NY, USA (2007)
Kiselyov, O., Ishii, H.: Freer monads, more extensible effects. In: Proceedings of the Haskell Symposium, pp. 94–105, ACM, New York, NY, USA (2015)
Kiselyov, O., Shan, C.c.: Lightweight monadic regions. In: Proceedings of the Haskell Symposium, Haskell ’08, ACM, New York, NY, USA (2008)
Launchbury, J., Peyton Jones, S.L.: Lazy functional state threads. In: Proceedings of the ACM SIGPLAN 1994 Conference on Programming Language Design and Implementation, p. 24–35, PLDI ’94, Association for Computing Machinery, New York, NY, USA (1994), https://doi.org/10.1145/178243.178246
Leijen, D.: Algebraic effect handlers with resources and deep finalization. Tech. Rep. MSR-TR-2018-10, Microsoft Research (April 2018)
Levy, P.B., Power, J., Thielecke, H.: Modelling environments in call-by-value programming languages. Information and Computation 185(2), 182–210 (2003)
Moggi, E., Sabry, A.: Monadic encapsulation of effects: a revised approach (extended version). Journal of Functional Programming 11(6), 591–627 (Nov 2001)
Reynolds, J.C.: Definitional interpreters for higher-order programming languages. In: Proceedings of the ACM annual conference, pp. 717–740, ACM, New York, NY, USA (1972)
Schuster, P., Brachthäuser, J.I.: Typing, representing, and abstracting control. In: Proceedings of the Workshop on Type-Driven Development, pp. 14–24, ACM, New York, NY, USA (2018), https://doi.org/10.1145/3240719.3241788
Schuster, P., Brachthäuser, J.I., Ostermann, K.: Compiling effect handlers in capability-passing style. Proc. ACM Program. Lang. 4(ICFP) (Aug 2020), https://doi.org/10.1145/3408975
Schuster, P., Brachthäuser, J.I., Ostermann, K.: Region-based resource management and lexical exception handlers in continuation-passing style (technical report). Tech. rep., University of Tübingen, Germany (01 2022), https://se.informatik.uni-tuebingen.de/publications/schuster22region/
Semmelroth, M., Sabry, A.: Monadic encapsulation in ml. In: Proceedings of the Fourth ACM SIGPLAN International Conference on Functional Programming, p. 8–17, ICFP ’99, Association for Computing Machinery, New York, NY, USA (1999), https://doi.org/10.1145/317636.317777
Thielecke, H.: Comparing control constructs by double-barrelled cps. Higher Order Symbol. Comput. 15(2–3), 141–160 (sep 2002), https://doi.org/10.1023/A:1020887011500
Thielecke, H.: From control effects to typed continuation passing. In: Proceedings of the 30th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, p. 139–149, POPL ’03, Association for Computing Machinery, New York, NY, USA (2003), https://doi.org/10.1145/604131.604144
Timany, A., Stefanesco, L., Krogh-Jespersen, M., Birkedal, L.: A logical relation for monadic encapsulation of state: Proving contextual equivalences in the presence of runst. Proc. ACM Program. Lang. 2(POPL) (Dec 2017), https://doi.org/10.1145/3158152
Tofte, M., Birkedal, L., Elsman, M., Hallenberg, N., Sestoft, P.: Programming with regions in the ml kit (for version 4) (10 2001)
Tofte, M., Talpin, J.P.: Region-based memory management. Inf. Comput. 132(2), 109–176 (Feb 1997), https://doi.org/10.1006/inco.1996.2613
Xie, N., Brachthäuser, J.I., Hillerström, D., Schuster, P., Leijen, D.: Effect handlers, evidently. Proc. ACM Program. Lang. 4(ICFP) (Aug 2020), https://doi.org/10.1145/3408981
Zhang, Y., Myers, A.C.: Abstraction-safe effect handlers via tunneling. Proc. ACM Program. Lang. 3(POPL), 5:1–5:29 (Jan 2019)
Zhang, Y., Salvaneschi, G., Beightol, Q., Liskov, B., Myers, A.C.: Accepting blame for safe tunneled exceptions. In: Proceedings of the Conference on Programming Language Design and Implementation, pp. 281–295, ACM, New York, NY, USA (2016)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Open Access This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.
The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.
Copyright information
© 2022 The Author(s)
About this paper
Cite this paper
Schuster, P., Brachthäuser, J.I., Ostermann, K. (2022). Region-based Resource Management and Lexical Exception Handlers in Continuation-Passing Style. In: Sergey, I. (eds) Programming Languages and Systems. ESOP 2022. Lecture Notes in Computer Science, vol 13240. Springer, Cham. https://doi.org/10.1007/978-3-030-99336-8_18
Download citation
DOI: https://doi.org/10.1007/978-3-030-99336-8_18
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-99335-1
Online ISBN: 978-3-030-99336-8
eBook Packages: Computer ScienceComputer Science (R0)
