Yannick Forster
Abstract
We compare the expressive power of three programming abstractions for user-defined computational effects: Plotkin and Pretnar's effect handlers, Filinski's monadic reflection, and delimited control without answer-type-modification. This comparison allows a precise discussion about the relative expressiveness of each programming abstraction. It also demonstrates the sensitivity of the relative expressiveness of user-defined effects to seemingly orthogonal language features.
We present three calculi, one per abstraction, extending Levy's call-by-push-value. For each calculus, we present syntax, operational semantics, a natural type-and-effect system, and, for effect handlers and monadic reflection, a set-theoretic denotational semantics. We establish their basic metatheoretic properties: safety, termination, and, where applicable, soundness and adequacy. Using Felleisen's notion of a macro translation, we show that these abstractions can macro-express each other, and show which translations preserve typeability. We use the adequate finitary set-theoretic denotational semantics for the monadic calculus to show that effect handlers cannot be macro-expressed while preserving typeability either by monadic reflection or by delimited control. Our argument fails with simple changes to the type system such as polymorphism and inductive types. We supplement our development with a mechanised Abella formalisation.
Supplemental Material
Available for Download
This artifact consists of a collection of Abella proofs. The proofs are a part of the GitHub repository https://github.com/matijapretnar/proofs. The formalisation contains proofs for the following theorems: * Theorem 2.1 (MAM safety) * Theorem 3.1 (EFF safety) * Theorem 4.1 (MON safety) * Theorem 5.1 (DEL safety) * Theorem 6.2 (DEL → MON correctness) * Theorem 6.5 (MON → DEL correctness) * Theorem 6.6 (DEL → EFF correctness) * Theorem 6.7 (EFF → DEL correctness) * Theorem 6.8 (MON → EFF correctness) * Theorem 6.9 (EFF → MON correctness)
- Kenichi Asai. 2009. On typing delimited continuations: three new solutions to the printf problem. Higher-Order and Symbolic Computation 22, 3 (2009), 275–291. Google Scholar
Digital Library
- Robert Atkey. 2009. Parameterised notions of computation. J. Funct. Program. 19, 3-4 (2009), 335–376.Google ScholarDigital Library
- M. Barr and C. Wells. 1985. Toposes, triples, and theories. Springer-Verlag. Google ScholarCross Ref
- Andrej Bauer and Matija Pretnar. 2014. An Effect System for Algebraic Effects and Handlers. Logical Methods in Computer Science 10, 4 (2014). Google ScholarCross Ref
- Andrej Bauer and Matija Pretnar. 2015. Programming with algebraic effects and handlers. J. Log. Algebr. Meth. Program. 84, 1 (2015), 108–123. Google ScholarCross Ref
- Edwin Brady. 2013. Programming and reasoning with algebraic effects and dependent types. In ICFP. ACM, 133–144. Google ScholarDigital Library
- Lukas Bulwahn, Alexander Krauss, Florian Haftmann, Levent Erkök, and John Matthews. 2008. Imperative Functional Programming with Isabelle/HOL. In TPHOLs (Lecture Notes in Computer Science), Vol. 5170. Springer, 134–149. Google ScholarDigital Library
- Olivier Danvy. 2006. An Analytical Approach to Programs as Data Objects. DSc dissertation. Department of Computer Science, University of Aarhus.Google Scholar
- Olivier Danvy and Andrzej Filinski. 1989. A Functional Abstraction of Typed Contexts. Technical Report 89/12. DIKU.Google Scholar
- Olivier Danvy and Andrzej Filinski. 1990. Abstracting Control. In LISP and Functional Programming. 151–160. Google ScholarDigital Library
- Christian Doczkal. 2007. Strong Normalization of CBPV. Technical Report. Saarland University.Google Scholar
- Christian Doczkal and Jan Schwinghammer. 2009. Formalizing a Strong Normalization Proof for Moggi’s Computational Metalanguage. In LFMTP. ACM, 57–63. Google ScholarDigital Library
- Matthias Felleisen. 1991. On the Expressive Power of Programming Languages. Sci. Comput. Program. 17, 1-3 (1991), 35–75.Google ScholarDigital Library
- Matthias Felleisen and Daniel P. Friedman. 1987. A Reduction Semantics for Imperative Higher-Order Languages. In PARLE (2) (Lecture Notes in Computer Science), Vol. 259. Springer, 206–223. Google ScholarCross Ref
- Matthias Felleisen, Mitchell Wand, Daniel P. Friedman, and Bruce F. Duba. 1988. Abstract Continuations: A Mathematical Semantics for Handling Full Jumps. In LISP and Functional Programming. 52–62. Google ScholarDigital Library
- Andrzej Filinski. 1994. Representing Monads. In POPL. ACM. Google ScholarDigital Library
- Andrzej Filinski. 1996. Controlling effects. Ph.D. Dissertation. School of Computer Science, Carnegie Mellon University, Pittsburgh, Pennsylvania.Google Scholar
- Andrzej Filinski. 1999. Representing Layered Monads. In POPL. ACM. Google ScholarDigital Library
- Andrzej Filinski. 2010. Monads in Action. SIGPLAN Not. 45, 1 (Jan. 2010), 483–494. Google ScholarDigital Library
- Yannick Forster. 2016. On the expressive power of effect handlers and monadic reflection. Technical Report. University of Cambridge.Google Scholar
- Andrew Gacek. 2008. The Abella Interactive Theorem Prover (System Description). In IJCAR, Vol. 5195. Springer, 154–161.Google ScholarDigital Library
- Andrew Gacek. 2009. A Framework for Specifying, Prototyping, and Reasoning about Computational Systems. Ph.D. Dissertation. University of Minnesota.Google Scholar
- Claudio Hermida. 1993. Fibrations, logical predicates and related topics. Ph.D. Dissertation. University of Edinburgh.Google Scholar
- Daniel Hillerström and Sam Lindley. 2016. Liberating effects with rows and handlers. In TyDe@ICFP. ACM, 15–27. Google ScholarDigital Library
- Daniel Hillerström, Sam Lindley, Robert Atkey, and KC Sivaramakrishnan. 2017. Continuation Passing Style for Effect Handlers. In FSCD (LIPIcs), Vol. 84. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, Article 18.Google Scholar
- Graham Hutton and Erik Meijer. 1998. Monadic Parsing in Haskell. J. Funct. Program. 8, 4 (1998), 437–444. Google ScholarDigital Library
- Ohad Kammar. 2014. An Algebraic Theory of Type-and-Effect Systems. Ph.D. Dissertation. University of Edinburgh.Google Scholar
- Ohad Kammar, Sam Lindley, and Nicolas Oury. 2013. Handlers in action. In ICFP. ACM, 145–158. Google ScholarDigital Library
- Ohad Kammar and Gordon D. Plotkin. 2012. Algebraic foundations for effect-dependent optimisations. In POPL. ACM. Google ScholarDigital Library
- Ohad Kammar and Matija Pretnar. 2017. No value restriction is needed for algebraic effects and handlers. J. Funct. Program. 27 (2017), e7. Google ScholarCross Ref
- Shin-ya Katsumata. 2014. Parametric Effect Monads and Semantics of Effect Systems. SIGPLAN Not. 49, 1 (Jan. 2014), 633–645.Google Scholar
- Oleg Kiselyov. 2016. Parameterized extensible effects and session types (extended abstract). In TyDe@ICFP. ACM, 41–42. Google ScholarDigital Library
- Oleg Kiselyov, Daniel P. Friedman, and Amr A. Sabry. 2005. How to remove a dynamic prompt: static and dynamic delimited continuation operators are equally expressible. Technical Report. 16 pages. Technical Report TR611.Google Scholar
- Oleg Kiselyov, Amr Sabry, and Cameron Swords. 2013. Extensible effects: an alternative to monad transformers. In Haskell. ACM, 59–70. Google ScholarDigital Library
- Oleg Kiselyov and Chung-chieh Shan. 2007. A Substructural Type System for Delimited Continuations. In TLCA. 223–239. Google ScholarCross Ref
- Oleg Kiselyov, Chung-chieh Shan, and Amr Sabry. 2006. Delimited dynamic binding. In ICFP. ACM, 26–37. Google ScholarDigital Library
- Ikuo Kobori, Yukiyoshi Kameyama, and Oleg Kiselyov. 2015. Answer-Type Modification without Tears: Prompt-Passing Style Translation for Typed Delimited-Control Operators. In WoC 2015 (EPTCS), Vol. 212. 36–52.Google Scholar
- James Laird. 2002. Exceptions, Continuations and Macro-expressiveness. In ESOP. 133–146.Google Scholar
- James Laird. 2013. Combining and Relating Control Effects and their Semantics. In COS. 113–129. Google ScholarCross Ref
- J. Laird. 2017. Combining control effects and their models: Game semantics for a hierarchy of static, dynamic and delimited control effects. Annals of Pure and Applied Logic 168, 2 (2017), 470–500. Eighth Games for Logic and Programming Languages Workshop (GaLoP). Google ScholarCross Ref
- Daan Leijen. 2017. Type directed compilation of row-typed algebraic effects. In POPL. ACM, 486–499. Google ScholarDigital Library
- Paul Blain Levy. 2004. Call-By-Push-Value: A Functional/Imperative Synthesis. Semantics Structures in Computation, Vol. 2. Springer.Google ScholarDigital Library
- Sam Lindley, Conor McBride, and Craig McLaughlin. 2017. Do be do be do. In POPL. ACM, 500–514. Google ScholarDigital Library
- Sam Lindley and Ian Stark. 2005. Reducibility and ⊤⊤-Lifting for Computation Types. In TLCA (Lecture Notes in Computer Science), Vol. 3461. Springer, 262–277. Google ScholarDigital Library
- John M. Lucassen and David K. Gifford. 1988. Polymorphic Effect Systems. In POPL. ACM, 47–57. Google ScholarDigital Library
- Francisco Marmolejo and Richard J. Wood. 2010. Monads as extension systems — no iteration is necessary. Theory and Applications of Categories 24, 4 (2010), 84–113.Google Scholar
- Marek Materzok and Dariusz Biernacki. 2012. A Dynamic Interpretation of the CPS Hierarchy. In APLAS (LNCS), Vol. 7705. Springer, 296–311. Google ScholarCross Ref
- Eugenio Moggi. 1989. Computational Lambda-Calculus and Monads. In LICS. IEEE Computer Society, 14–23. Google ScholarCross Ref
- Gordon D. Plotkin and John Power. 2002. Notions of Computation Determine Monads. In FoSSaCS. Springer-Verlag. Google ScholarCross Ref
- Gordon D. Plotkin and John Power. 2003. Algebraic Operations and Generic Effects. Appl. Categ. Structures 11, 1 (2003), 69–94. Google ScholarCross Ref
- Gordon D. Plotkin and Matija Pretnar. 2008. A Logic for Algebraic Effects. In LICS. IEEE Computer Society, 118–129. Google ScholarDigital Library
- Gordon D. Plotkin and Matija Pretnar. 2009. Handlers of Algebraic Effects. In ESOP. Springer-Verlag. Google ScholarDigital Library
- Matija Pretnar. 2014. Inferring Algebraic Effects. Logical Methods in Computer Science 10, 3 (2014). Google ScholarCross Ref
- Matija Pretnar. 2015. An Introduction to Algebraic Effects and Handlers. Invited tutorial paper. Electr. Notes Theor. Comput. Sci. 319 (2015), 19–35. Google ScholarDigital Library
- John C. Reynolds. 2009. Theories of Programming Languages. Cambridge University Press.Google Scholar
- Tom Schrijvers and others. 2016. Monad transformers and modular algebraic effects. Technical Report. University of Leuven.Google Scholar
- Tom Schrijvers, Guido Tack, Pieter Wuille, Horst Samulowitz, and Peter J. Stuckey. 2013. Search combinators. Constraints 18, 2 (2013), 269–305. Google ScholarDigital Library
- Chung-chieh Shan. 2007. A static simulation of dynamic delimited control. Higher-Order and Symbolic Computation 20, 4 (2007), 371–401. Google ScholarDigital Library
- J. Michael Spivey. 1990. A Functional Theory of Exceptions. Sci. Comput. Program. 14, 1 (1990), 25–42. Google ScholarDigital Library
- Wouter Swierstra. 2008. Data types à la carte. J. Funct. Program. 18, 4 (2008), 423–436. Google ScholarDigital Library
- William W Tait. 1967. Intensional interpretations of functionals of finite type I. The journal of symbolic logic 32, 02 (1967), 198–212. Google ScholarCross Ref
- Philip Wadler. 1990. Comprehending Monads. In LISP and Functional Programming. 61–78. Google ScholarDigital Library
- Philip Wadler. 1994. Monads and Composable Continuations. Lisp and Symbolic Computation 7, 1 (1994), 39–56. Google ScholarDigital Library
- Andrew K. Wright and Matthias Felleisen. 1994. A Syntactic Approach to Type Soundness. Inf. Comput. 115, 1 (1994), 38–94. Google ScholarDigital Library
- Beta Ziliani, Derek Dreyer, Neelakantan R. Krishnaswami, Aleksandar Nanevski, and Viktor Vafeiadis. 2015. Mtac: A monad for typed tactic programming in Coq. J. Funct. Program. 25 (2015). Google ScholarCross Ref
Index Terms
- On the expressive power of user-defined effects: effect handlers, monadic reflection, delimited control
Recommendations
Call-by-push-value in Coq: operational, equational, and denotational theory
CPP 2019: Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and ProofsCall-by-push-value (CBPV) is an idealised calculus for functional and imperative programming, introduced as a subsuming paradigm for both call-by-value (CBV) and call-by-name (CBN). We formalise weak and strong operational semantics for (effect-free) ...
An approach to call-by-name delimited continuations
POPL '08We show that a variant of Parigot's λμ-calculus, originally due to de Groote and proved to satisfy Boehm's theorem by Saurin, is canonically interpretable as a call-by-name calculus of delimited control. This observation is expressed using Ariola et al'...
An approach to call-by-name delimited continuations
POPL '08: Proceedings of the 35th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languagesWe show that a variant of Parigot's λμ-calculus, originally due to de Groote and proved to satisfy Boehm's theorem by Saurin, is canonically interpretable as a call-by-name calculus of delimited control. This observation is expressed using Ariola et al'...
Comments