Document Open Access Logo

Continuation Passing Style for Effect Handlers

Authors Daniel Hillerström, Sam Lindley, Robert Atkey, K. C. Sivaramakrishnan

PDF
Thumbnail PDF

File

LIPIcs.FSCD.2017.18.pdf
  • Filesize: 0.73 MB
  • 19 pages

Document Identifiers

Author Details

Daniel Hillerström
Sam Lindley
Robert Atkey
K. C. Sivaramakrishnan

Cite AsGet BibTex

Daniel Hillerström, Sam Lindley, Robert Atkey, and K. C. Sivaramakrishnan. Continuation Passing Style for Effect Handlers. In 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 84, pp. 18:1-18:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
https://doi.org/10.4230/LIPIcs.FSCD.2017.18

Abstract

We present Continuation Passing Style (CPS) translations for Plotkin and Pretnar's effect handlers with Hillerström and Lindley's row-typed fine-grain call-by-value calculus of effect handlers as the source language. CPS translations of handlers are interesting theoretically, to explain the semantics of handlers, and also offer a practical implementation technique that does not require special support in the target language's runtime. We begin with a first-order CPS translation into untyped lambda calculus which manages a stack of continuations and handlers as a curried sequence of arguments. We then refine the initial CPS translation first by uncurrying it to yield a properly tail-recursive translation and second by making it higher-order in order to contract administrative redexes at translation time. We prove that the higher-order CPS translation simulates effect handler reduction. We have implemented the higher-order CPS translation as a JavaScript backend for the Links programming language.
Keywords
  • effect handlers
  • delimited control
  • continuation passing style

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. Andrew W. Appel. Compiling with Continuations. Cambridge University Press, 1992. Google Scholar
  2. Andrej Bauer and Matija Pretnar. Programming with algebraic effects and handlers. J. Log. Algebr. Meth. Program., 84(1):108-123, 2015. Google Scholar
  3. Bernard Berthomieu and Camille le Moniès de Sagazan. A calculus of tagged types, with applications to process languages. In Workshop on Types for Program Analysis, 1995. Google Scholar
  4. Edwin Brady. Programming and reasoning with algebraic effects and dependent types. In ICFP, pages 133-144. ACM, 2013. Google Scholar
  5. Ezra Cooper, Sam Lindley, Philip Wadler, and Jeremy Yallop. Links: Web programming without tiers. In FMCO, volume 4709 of LNCS, pages 266-296. Springer, 2006. Google Scholar
  6. Olivier Danvy and Andrzej Filinski. Abstracting control. In LISP and Functional Programming, pages 151-160, 1990. Google Scholar
  7. Olivier Danvy and Lasse R. Nielsen. A first-order one-pass CPS transformation. Theor. Comput. Sci., 308(1-3):239-257, 2003. Google Scholar
  8. Stephen Dolan, Leo White, K. C. Sivaramakrishnan, Jeremy Yallop, and Anil Madhavapeddy. Effective concurrency through algebraic effects. OCaml Workshop, 2015. Google Scholar
  9. Cormac Flanagan, Amr Sabry, Bruce F. Duba, and Matthias Felleisen. The essence of compiling with continuations. In PLDI, pages 237-247. ACM, 1993. Google Scholar
  10. Yannick Forster, Ohad Kammar, Sam Lindley, and Matija Pretnar. On the expressive power of user-defined effects: Effect handlers, monadic reflection, delimited control. Proc. ACM Program. Lang., 1(ICFP), September 2017. Google Scholar
  11. Daniel Hillerström and Sam Lindley. Liberating effects with rows and handlers. In TyDe@ICFP, pages 15-27. ACM, 2016. Google Scholar
  12. Gérard P. Huet. The zipper. J. Funct. Program., 7(5):549-554, 1997. Google Scholar
  13. Ohad Kammar, Sam Lindley, and Nicolas Oury. Handlers in action. In ICFP, pages 145-158. ACM, 2013. Google Scholar
  14. Andrew Kennedy. Compiling with continuations, continued. In ICFP, pages 177-190. ACM, 2007. Google Scholar
  15. Oleg Kiselyov and Hiromi Ishii. Freer monads, more extensible effects. In Haskell, pages 94-105. ACM, 2015. Google Scholar
  16. Oleg Kiselyov and KC Sivaramakrishnan. Eff directly in OCaml. ML Workshop, 2016. Google Scholar
  17. Daan Leijen. Type directed compilation of row-typed algebraic effects. In POPL, pages 486-499. ACM, 2017. Google Scholar
  18. Paul Blain Levy, John Power, and Hayo Thielecke. Modelling environments in call-by-value programming languages. Inf. Comput., 185(2):182-210, 2003. Google Scholar
  19. Sam Lindley and James Cheney. Row-based effect types for database integration. In TLDI, pages 91-102. ACM, 2012. Google Scholar
  20. Sam Lindley, Conor McBride, and Craig McLaughlin. Do be do be do. In POPL, pages 500-514. ACM, 2017. Google Scholar
  21. Marek Materzok and Dariusz Biernacki. Subtyping delimited continuations. In ICFP, pages 81-93. ACM, 2011. Google Scholar
  22. Marek Materzok and Dariusz Biernacki. A dynamic interpretation of the CPS hierarchy. In APLAS, volume 7705 of LNCS, pages 296-311. Springer, 2012. Google Scholar
  23. Eugenio Moggi. Notions of computation and monads. Inf. Comput., 93(1):55-92, 1991. Google Scholar
  24. Gordon D. Plotkin. Call-by-name, call-by-value and the lambda-calculus. Theor. Comput. Sci., 1(2):125-159, 1975. Google Scholar
  25. Gordon D. Plotkin and John Power. Adequacy for algebraic effects. In FoSSaCS, volume 2030 of LNCS, pages 1-24. Springer, 2001. Google Scholar
  26. Gordon D. Plotkin and Matija Pretnar. Handling algebraic effects. Logical Methods in Computer Science, 9(4), 2013. URL: http://dx.doi.org/10.2168/LMCS-9(4:23)2013.
  27. Matija Pretnar. An introduction to algebraic effects and handlers. Electr. Notes Theor. Comput. Sci., 319:19-35, 2015. Invited tutorial paper. Google Scholar
  28. Didier Remy. Syntactic theories and the algebra of record terms. Technical Report RR-1869, INRIA, 1993. Google Scholar
  29. Philip Wadler. The essence of functional programming. In POPL, pages 1-14. ACM, 1992. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact