Hostname: page-component-745bb68f8f-kw2vx Total loading time: 0 Render date: 2025-01-12T04:22:25.199Z Has data issue: false hasContentIssue false
  • English
  • Français

On the expressive power of user-defined effects: Effect handlers, monadic reflection, delimited control

Part of: ICFP2017 JFP Research Articles

Published online by Cambridge University Press:  08 October 2019

YANNICK FORSTER ,
OHAD KAMMAR Open the ORCID record for OHAD KAMMAR [Opens in a new window] ,
SAM LINDLEY  and
MATIJA PRETNAR
YANNICK FORSTER
Affiliation:
Department of Computer Science, Saarland University, GermanyComputer Laboratory, University of Cambridge, England (e-mail: [email protected])
OHAD KAMMAR
Affiliation:
School of Informatics, The University of Edinburgh, ScotlandDepartment of Computer Science, Balliol College, University of OxfordComputer Laboratory, University of Cambridge, England (e-mail: [email protected])
SAM LINDLEY
Affiliation:
School of Informatics, The University of Edinburgh, ScotlandDepartment of Computing, Imperial College, London, England (e-mail: [email protected])
MATIJA PRETNAR
Affiliation:
Faculty of Mathematics and Physics, University of Ljubljana, Slovenia (e-mail: [email protected])
Rights & Permissions [Opens in a new window]

Abstract

Core share and HTML view are not available for this content. However, as you have access to this content, a full PDF is available via the ‘Save PDF’ action button.

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. 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.

Type
Regular Paper
Information
Journal of Functional Programming , Volume 29 , 2019 , e15
Copyright
© Cambridge University Press 2019 

References

Asai, K. (2009) On typing delimited continuations: three new solutions to the printf problem. Higher-Order Symb. Comput. 22(3), 275–291.CrossRefGoogle Scholar
Asai, K. & Kameyama, Y. (2007) Polymorphic delimited continuations. In Programming Languages and Systems, Shao, Z. (ed). Berlin, Heidelberg: Springer, pp. 239–254.CrossRefGoogle Scholar
Atkey, R. (2009) Parameterised notions of computation. J. Funct. Program. 19(3–4), 335–376.CrossRefGoogle Scholar
Baelde, D., Chaudhuri, K., Gacek, A., Miller, D., Nadathur, G., Tiu, A. & Wang, Y. (2014) Abella: a system for reasoning about relational specifications. J. Form. Reason. 7(2), 1–89.Google Scholar
Barr, M. & Wells, C. (1985) Toposes, Triples, and Theories. Grundlehren der mathematischen Wissenschaften. Springer-Verlag.CrossRefGoogle Scholar
Bauer, A. & Pretnar, M. (2014) An effect system for algebraic effects and handlers. Log. Methods Comput. Sci. 10(4), 29 pages.CrossRefGoogle Scholar
Bauer, A. & Pretnar, M. (2015) Programming with algebraic effects and handlers. J. Logical Alg. Methods Program. 84(1), 108–123. Special Issue: Domains X, International workshop on Domain Theory and applications, Swansea, er 5–7, 2011.CrossRefGoogle Scholar
Brachthauser, J. & Leijen, D. (2019) Programming with Implicit Values, Functions, and Control (or, Implicit Functions: Dynamic Binding with Lexical Scoping). Technical Report MSR-TR-2019-7. Microsoft.Google Scholar
Brady, E. (2013) Programming and reasoning with algebraic effects and dependent types. In Proceedings of the 18th ACM SIGPLAN International Conference on Functional Programming. ICFP’13. New York, NY, USA: ACM, pp. 133–144.CrossRefGoogle Scholar
Bračevac, O., Amin, N., Salvaneschi, G., Erdweg, S., Eugster, P. & Mezini, M. (2018) Versatile event correlation with algebraic effects. Proc. ACM Program. Lang. 2(ICFP), 67:1–67:31.CrossRefGoogle Scholar
Bulwahn, L., Krauss, A., Haftmann, F., Erkök, L. & Matthews, J. (2008). Imperative functional programming with Isabelle/HOL. In Theorem Proving in Higher Order Logics, Mohamed, O. A., Muñoz, C., & Tahar, S. (eds). Berlin, Heidelberg: Springer, pp. 134–149.CrossRefGoogle Scholar
Danvy, O. (2006) An Analytical Approach to Programs as Data Objects. DSc dissertation, Department of Computer Science, University of Aarhus.Google Scholar
Danvy, O. & Filinski, A. (1989) A Functional Abstraction of Typed Contexts. Technical Report 89/12. DIKU.Google Scholar
Danvy, O. & Filinski, A. (1990) Abstracting control. In Proceedings of the 1990 ACM Conference on LISP and Functional Programming. LFP’90. New York, NY, USA: ACM, pp. 151–160.CrossRefGoogle Scholar
Doczkal, C. (2007) Strong Normalization of CBPV. Technical Report, Saarland University.Google Scholar
Doczkal, C. & Schwinghammer, J. (2009) Formalizing a strong normalization proof for moggi’s computational metalanguage: a case study in Isabelle/HOL-nominal. In Proceedings of the Fourth International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice. LFMTP’09. New York, NY, USA: ACM, pp. 57–63.CrossRefGoogle Scholar
Felleisen, M. (1991) On the expressive power of programming languages. Sci. Comput. Program. 17(1), 35–75.CrossRefGoogle Scholar
Felleisen, M. & Friedman, D. P. (1987) A reduction semantics for imperative higher-order languages. In PARLE Parallel Architectures and Languages Europe, de Bakker, J. W., Nijman, A. J. & Treleaven, P. C. (eds). Berlin, Heidelberg: Springer, pp. 206–223.CrossRefGoogle Scholar
Felleisen, M., Wand, M., Friedman, D. & Duba, B. (1988) Abstract continuations: a mathematical semantics for handling full jumps. In Proceedings of the 1988 ACM Conference on LISP and Functional Programming. LFP’88. New York, NY, USA: ACM, pp. 52–62.CrossRefGoogle Scholar
Filinski, A. (1994) Representing monads. In Proceedings of the 21st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. POPL’94. New York, NY, USA: ACM, pp. 446–457.CrossRefGoogle Scholar
Filinski, A. (1996) Controlling Effects. PhD thesis, School of Computer Science, Carnegie Mellon University, Pittsburgh, Pennsylvania.Google Scholar
Filinski, A. (1999) Representing layered monads. In Proceedings of the 26th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. POPL’99. New York, NY, USA: ACM, pp. 175–188.CrossRefGoogle Scholar
Filinski, A. (2010) Monads in action. In Proceedings of the 37th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. POPL’10. New York, NY, USA: ACM, pp. 483–494.CrossRefGoogle Scholar
Forster, Y. (2016) On the Expressive Power of Effect Handlers and Monadic Reflection. Technical Report, University of Cambridge.Google Scholar
Forster, Y., Kammar, O., Lindley, S. & Pretnar, M. (2017) On the expressive power of user-defined effects: effect handlers, monadic reflection, delimited control. Proc. ACM Program. Lang. 1(ICFP), 13:1–13:29.CrossRefGoogle Scholar
Forster, Y., Schäfer, S., Spies, S. & Stark, K. (2019) Call-by-push-value in Coq: operational, equational, and denotational theory. In Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs. CPP 2019. New York, NY, USA: ACM, pp. 118–131.CrossRefGoogle Scholar
Gacek, A. (2008) The Abella interactive theorem prover (system description). In Automated Reasoning, Armando, A., Baumgartner, P. & Dowek, G. (eds). Berlin, Heidelberg: Springer, pp. 154–161.CrossRefGoogle Scholar
Gacek, A. (2009) A Framework for Specifying, Prototyping, and Reasoning about Computational Systems. PhD thesis, University of Minnesota.Google Scholar
Hermida, C. (1993) Fibrations, Logical Predicates and Related Topics. PhD thesis, University of Edinburgh.Google Scholar
Hillerström, D. & Lindley, S. (2016) Liberating effects with rows and handlers. In Proceedings of the 1st International Workshop on Type-Driven Development. TyDe 2016. New York, NY, USA: ACM, pp. 15–27.CrossRefGoogle Scholar
Hillerström, D., Lindley, S., Atkey, R. & Sivaramakrishnan, K. C. (2017) Continuation Passing style for effect handlers. In 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017), Miller, D. (ed). Leibniz International Proceedings in Informatics (LIPIcs), vol. 84. Dagstuhl, Germany: Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik, pp. 18:1–18:19.Google Scholar
Hutton, G. & Meijer, E. (1998) Monadic parsing in Haskell. J. Funct. Program. 8(4), 437–444.CrossRefGoogle Scholar
Inostroza, P. & van der Storm, T. (2018) JEff: objects for effect. In Proceedings of the 2018 ACM SIGPLAN International Symposium on New Ideas, New Paradigms, and Reflections on Programming and Software. Onward! 2018. New York, NY, USA: ACM, pp. 111–124.CrossRefGoogle Scholar
Kammar, O. (2014) An Algebraic Theory of Type-and-Effect Systems. PhD thesis, University of Edinburgh.Google Scholar
Kammar, O., Lindley, S. & Oury, N. (2013) Handlers in action. In Proceedings of the 18th ACM SIGPLAN International Conference on Functional Programming. ICFP’13. New York, NY, USA: ACM, pp. 145–158.CrossRefGoogle Scholar
Kammar, O. & McDermott, D. (2018) Factorisation systems for logical relations and monadic lifting in type-and-effect system semantics. Electron. Notes Theor. Comput. Sci. 341, 239–260. Proceedings of the Thirty-Fourth Conference on the Mathematical Foundations of Programming Semantics (MFPS XXXIV).CrossRefGoogle Scholar
Kammar, O. & Plotkin, G. D. (2012) Algebraic foundations for effect-dependent optimisations. In Proceedings of the 39th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. POPL’12. New York, NY, USA: ACM, pp. 349–360.CrossRefGoogle Scholar
Kammar, O. & Pretnar, M. (2017) No value restriction is needed for algebraic effects and handlers. J. Funct. Program. 27, e7.CrossRefGoogle Scholar
Katsumata, S. (2014) Parametric effect monads and semantics of effect systems. In Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. POPL’14. New York, NY, USA: ACM, pp. 633–645.CrossRefGoogle Scholar
Kiselyov, O. (2016) Parameterized extensible effects and session types (extended abstract). In Proceedings of the 1st International Workshop on Type-Driven Development. TyDe 2016. New York, NY, USA: ACM, pp. 41–42.CrossRefGoogle Scholar
Kiselyov, O., Friedman, D. P. & Sabry, A. A. (2005) How to Remove a Dynamic Prompt: Static and Dynamic Delimited Continuation Operators are Equally Expressible. Technical Report TR611, Indiana University School of Informatics and Computing.Google Scholar
Kiselyov, O., Sabry, A. & Swords, C. (2013) Extensible effects: an alternative to monad transformers. In Proceedings of the 2013 ACM SIGPLAN Symposium on Haskell. Haskell’13. New York, NY, USA: ACM, pp. 59–70.CrossRefGoogle Scholar
Kiselyov, O. & Shan, C.-c. (2007) A substructural type system for delimited continuations. In Typed Lambda Calculi and Applications, Della Rocca, S. R. (ed). Berlin, Heidelberg: Springer, pp. 223–239.CrossRefGoogle Scholar
Kiselyov, O., Shan, C.-c. & Sabry, A. (2006). Delimited dynamic binding. In Proceedings of the Eleventh ACM SIGPLAN International Conference on Functional Programming. ICFP’06. New York, NY, USA: ACM, pp. 26–37.CrossRefGoogle Scholar
Kiselyov, O. & Sivaramakrishnan, K. C. (2018) Eff directly in OCaml. In Proceedings ML Family Workshop/OCaml Users and Developers workshops, Nara, Japan, September 22–23, 2016, Asai, K. & Shinwell, M. (eds). Electronic Proceedings in Theoretical Computer Science, vol. 285. Open Publishing Association, pp. 23–58.CrossRefGoogle Scholar
Kobori, I., Kameyama, Y. & Kiselyov, O. (2016) Answer-type modification without tears: prompt-passing style translation for typed delimited-control operators. In Proceedings of the Workshop on Continuations, London, UK, April 12, 2015, Danvy, O. & de’Liguoro, U. (eds). Electronic Proceedings in Theoretical Computer Science, vol. 212. Open Publishing Association, pp. 36–52.CrossRefGoogle Scholar
Laird, J. (2002) Exceptions, continuations and macro-expressiveness. In Programming Languages and Systems, Le Métayer, D. (ed). Berlin, Heidelberg: Springer, pp. 133–146.CrossRefGoogle Scholar
Laird, J. (2013) Combining and relating control effects and their semantics. In Proceedings First Workshop on Control Operators and their Semantics, Eindhoven, The Netherlands, June 24–25, 2013, de’Liguoro, U. & Saurin, A. (eds). Electronic Proceedings in Theoretical Computer Science, vol. 127. Open Publishing Association, pp. 113–129.CrossRefGoogle Scholar
Laird, J. (2017) Combining control effects and their models: game semantics for a hierarchy of static, dynamic and delimited control effects. Ann. Pure Appl. Logic 168(2), 470–500. Eighth Games for Logic and Programming Languages Workshop (GaLoP).CrossRefGoogle Scholar
Leijen, D. (2017) Type directed compilation of row-typed algebraic effects. In Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages. POPL 2017. New York, NY, USA: ACM, pp. 486–499.CrossRefGoogle Scholar
Levy, P. B. (2003) Call-by-Push-Value: A Functional/Imperative Synthesis. Semantics Structures in Computation, vol. 2. Dordrecht, Netherlands: Springer.CrossRefGoogle Scholar
Lindley, S., McBride, C. & McLaughlin, C. (2017) Do be do be do. In Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages. POPL 2017. New York, NY, USA: ACM, pp. 500–514.CrossRefGoogle Scholar
Lindley, S. & Stark, I. (2005) Reducibility and ⊺⊺-lifting for computation types. In Typed Lambda Calculi and Applications, Urzyczyn, P. (ed). Berlin, Heidelberg: Springer, pp. 262–277.CrossRefGoogle Scholar
Lucassen, J. M. & Gifford, D. K. (1988) Polymorphic effect systems. In Proceedings of the 15th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. POPL’88. New York, NY, USA: ACM, pp. 47–57.CrossRefGoogle Scholar
Marmolejo, F. & Wood, R. J. (2010) Monads as extension systems—no iteration is necessary. Theory Appl. Categor. 24(4), 84–113.Google Scholar
Materzok, M. & Biernacki, D. (2012) A dynamic interpretation of the CPS hierarchy. In Programming Languages and Systems, Jhala, R. & Igarashi, A. (eds). Berlin, Heidelberg: Springer, pp. 296–311.CrossRefGoogle Scholar
Moggi, E. (1989) Computational lambda-calculus and monads. In Proceedings of the Fourth Annual Symposium on Logic in Computer Science. Piscataway, NJ, USA: IEEE, pp. 14–23.CrossRefGoogle Scholar
Paré, R. (1974) Colimits in topoi. Bull. Amer. Math. Soc. 80(3), 556–561.CrossRefGoogle Scholar
Piróg, M., Polesiuk, P. & Sieczkowski, F. (2019) Typed equivalence of effect handlers and delimited control. In 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019), Geuvers, H. (ed). Leibniz International Proceedings in Informatics (LIPIcs), vol. 131. Dagstuhl, Germany: Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik, pp. 30:1–30:16.Google Scholar
Plotkin, G. & Power, J. (2002) Notions of computation determine monads. In Foundations of Software Science and Computation Structures, Nielsen, M. & Engberg, U. (eds). Berlin, Heidelberg: Springer, pp. 342–356.CrossRefGoogle Scholar
Plotkin, G. & Power, J. (2003) Algebraic operations and generic effects. Appl. Categor. Struct. 11(1), 69–94.CrossRefGoogle Scholar
Plotkin, G. & Pretnar, M. (2008) A logic for algebraic effects. In Proceedings of the 2008 23rd Annual IEEE Symposium on Logic in Computer Science. LICS’08. Washington, DC, USA: IEEE Computer Society, pp. 118–129.CrossRefGoogle Scholar
Plotkin, G. & Pretnar, M. (2009) Handlers of algebraic effects. In Programming Languages and Systems, Castagna, G. (ed). Berlin, Heidelberg: Springer, pp. 80–94.CrossRefGoogle Scholar
Pretnar, M. (2014) Inferring algebraic effects. Logical Methods Comput. Sci. 10(3), 43 pages.CrossRefGoogle Scholar
Pretnar, M. (2015) An introduction to algebraic effects and handlers. invited tutorial paper. Electron. Notes Theoret. Comput. Sci. 319, 19–35. The 31st Conference on the Mathematical Foundations of Programming Semantics (MFPS XXXI).CrossRefGoogle Scholar
Reynolds, J. C. (1998) Theories of Programming Languages. Cambridge University.CrossRefGoogle Scholar
Saleh, A. H., Karachalias, G., Pretnar, M. & Schrijvers, T. (2018). Explicit effect subtyping. In Programming Languages and Systems, Ahmed, A. (ed). Cham: Springer International Publishing, pp. 327–354.CrossRefGoogle Scholar
Schrijvers, T., Piróg, M., Wu, N. & Jaskelioff, M. (to appear) Monad transformers and modular algebraic effects: what binds them together. In Proceedings of the 12th ACM SIGPLAN International Symposium on Haskell. Haskell 2019. New York, NY, USA: ACM.CrossRefGoogle Scholar
Schrijvers, T., Tack, G., Wuille, P., Samulowitz, H. & Stuckey, P. J. (2013) Search combinators. Constraints 18(2), 269–305.CrossRefGoogle Scholar
Shan, C.-c. (2007) A static simulation of dynamic delimited control. Higher-Order Symb. Comput. 20(4), 371–401.CrossRefGoogle Scholar
Sinkovics, Á. & Porkoláb, Z. (2013) Implementing monads for C++ template metaprograms. Sci. Comput. Program. 78(9), 1600–1621.CrossRefGoogle Scholar
Spivey, M. (1990) A functional theory of exceptions. Sci. Comput. Program. 14(1), 25–42.CrossRefGoogle Scholar
Swierstra, W. (2008) Data types à la carte. J. Funct. Program. 18(4), 423–436.CrossRefGoogle Scholar
Tait, W. W. (1967) Intensional interpretations of functionals of finite type I. J. Symb. Logic 32(2), 198–212.CrossRefGoogle Scholar
Wadler, P. (1990) Comprehending monads. In Proceedings of the 1990 ACM Conference on LISP and Functional Programming. LFP’90. New York, NY, USA: ACM, pp. 61–78.CrossRefGoogle Scholar
Wadler, P. (1994) Monads and composable continuations. Lisp Symb. Comput. 7(1), 39–55.CrossRefGoogle Scholar
Wright, A. K. & Felleisen, M. (1994) A syntactic approach to type soundness. Infor. Comput. 115(1), 38–94.CrossRefGoogle Scholar
Zhang, Y. & Myers, A. C. (2019) Abstraction-safe effect handlers via tunneling. Proc. ACM Program. Lang. 3(POPL), 5:1–5:29.CrossRefGoogle Scholar
Ziliani, B., Dreyer, D., Krishnaswami, N. R., Nanevski, A. & Vafeiadis, V. (2015) Mtac: a monad for typed tactic programming in Coq. J. Funct. Program. 25, e12.CrossRefGoogle Scholar
Submit a response

Discussions

No Discussions have been published for this article.