Dariusz Biernacki
Abstract
Proposed originally by Plotkin and Pretnar, algebraic effects and their handlers are a leading-edge approach to computational effects: exceptions, mutable state, nondeterminism, and such. Appreciated for their elegance and expressiveness, they are now progressing into mainstream functional programming languages. In this paper, we introduce and examine programming language constructs that back adoption of programming with algebraic effects on a larger scale in a modular fashion by providing mechanisms for abstraction. We propose two such mechanisms: existential effects (which hide the details of a particular effect from the user) and local effects (which guarantee that no code coming from the outside can interfere with a given effect). The main technical difficulty arises from the dynamic nature of coupling an effectful operation with the right handler during execution, but, as we show in this paper, a carefully designed type system can ensure that this will not break the abstraction. Our main contribution is a novel calculus for algebraic effects and handlers, called λHEL, equipped with local and existential algebraic effects, in which the dynamic nature of handlers is kept in check by typed runtime coercions. As a proof of concept, we present an experimental programming language based on our calculus, which provides strong abstraction mechanisms via an ML-style module system.
Supplemental Material
- Andrej Bauer and Matija Pretnar. 2014. An Effect System for Algebraic Effects and Handlers. Logical Methods in Computer Science 10, 4:9 (2014), 1–29.Google Scholar
Cross 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
- Malgorzata Biernacka, Dariusz Biernacki, and Olivier Danvy. 2005. An Operational Foundation for Delimited Continuations in the CPS Hierarchy. Logical Methods in Computer Science 1, 2:5 (2005), 1–39.Google ScholarCross Ref
- Dariusz Biernacki, Maciej Piróg, Piotr Polesiuk, and Filip Sieczkowski. 2018. Handle with care: Relational interpretation of algebraic effects and handlers. PACMPL 2, POPL (2018), 8:1–8:30. Google ScholarDigital Library
- Giuseppe Castagna and Andrew D. Gordon (Eds.). 2017. Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, Paris, France, January 18-20, 2017. ACM. Google Scholar
- John Clements and Matthias Felleisen. 2004. A tail-recursive machine with stack inspection. ACM Trans. Program. Lang. Syst. 26, 6 (2004), 1029–1052. Google ScholarDigital Library
- William D. Clinger. 1998. Proper Tail Recursion and Space Efficiency. In Proceedings of the ACM SIGPLAN ’98 Conference on Programming Language Design and Implementation (PLDI), Montreal, Canada, June 17-19, 1998, Jack W. Davidson, Keith D. Cooper, and A. Michael Berman (Eds.). ACM, 174–185. Google ScholarDigital Library
- Guy Cousineau, Pierre-Louis Curien, and Michel Mauny. 1985. The Categorical Abstract Machine. In Functional Programming Languages and Computer Architecture, FPCA 1985, Nancy, France, September 16-19, 1985, Proceedings (Lecture Notes in Computer Science), Jean-Pierre Jouannaud (Ed.), Vol. 201. Springer, 50–64. Google ScholarDigital Library
- R. Kent Dybvig, Simon L. Peyton Jones, and Amr Sabry. 2007. A monadic framework for delimited continuations. J. Funct. Program. 17, 6 (2007), 687–730. Google ScholarDigital Library
- Matthias Felleisen. 1988. The Theory and Practice of First-Class Prompts. In Conference Record of the Fifteenth Annual ACM Symposium on Principles of Programming Languages, San Diego, California, USA, January 10-13, 1988, Jeanne Ferrante and P. Mager (Eds.). ACM Press, 180–190. Google ScholarDigital Library
- Matthias Felleisen and Daniel P. Friedman. 1986. Control Operators, the SECD Machine, and the λ-Calculus. In Formal Description of Programming Concepts III, Martin Wirsing (Ed.). Elsevier Science Publishers B.V. (North-Holland), Amsterdam, 193–217.Google Scholar
- Robert Harper. 2016. Practical Foundations for Programming Languages (2nd ed.). Cambridge University Press, New York, NY, USA. Google ScholarDigital Library
- Daniel Hillerström and Sam Lindley. 2016. Liberating effects with rows and handlers. In Proceedings of the 1st International Workshop on Type-Driven Development, TyDe@ICFP 2016, Nara, Japan, September 18, 2016, James Chapman and Wouter Swierstra (Eds.). ACM, 15–27. Google ScholarDigital Library
- Gerard Huet. 1976. Resolution d’equation dans les langages d’ordre 1, 2, . . . , ω. Ph.D. Dissertation. Université de Paris VII, France.Google Scholar
- Ohad Kammar, Sam Lindley, and Nicolas Oury. 2013. Handlers in action. In ACM SIGPLAN International Conference on Functional Programming, ICFP’13, Boston, MA, USA - September 25 - 27, 2013, Greg Morrisett and Tarmo Uustalu (Eds.). ACM, 145–158. Google ScholarDigital Library
- Kevin Knight. 1989. Unification: A Multidisciplinary Survey. ACM Comput. Surv. 21, 1 (1989), 93–124. Google ScholarDigital Library
- Jean-Louis Krivine. 2007. A call-by-name lambda-calculus machine. Higher-Order and Symbolic Computation 20, 3 (2007), 199–207. Google ScholarDigital Library
- Peter J. Landin. 1964. The Mechanical Evaluation of Expressions. Comput. J. 6, 4 (1964), 308–320.Google ScholarCross Ref
- Daan Leijen. 2014. Koka: Programming with Row Polymorphic Effect Types. In Proceedings 5th Workshop on Mathematically Structured Functional Programming, MSFP@ETAPS 2014, Grenoble, France, 12 April 2014. 100–126.Google ScholarCross Ref
- Daan Leijen. 2017. Type directed compilation of row-typed algebraic effects, See { Castagna and Gordon 2017 }, 486–499. Google ScholarDigital Library
- Daan Leijen. 2018. Algebraic Effect Handlers with Resources and Deep Finalization. Technical Report MSR-TR-2018-10. Microsoft Research.Google Scholar
- Xavier Leroy. 1990. The Zinc experiment: an economical implementation of the ML language. Rapport Technique 117. INRIA Rocquencourt, Le Chesnay, France.Google Scholar
- Sam Lindley, Conor McBride, and Craig McLaughlin. 2017. Do be do be do, See { Castagna and Gordon 2017 }, 500–514. Google ScholarDigital Library
- Simon Marlow and Simon L. Peyton Jones. 2006. Making a fast curry: push/enter vs. eval/apply for higher-order languages. J. Funct. Program. 16, 4-5 (2006), 415–449. Google ScholarDigital Library
- Simon Peyton Jones (Ed.). 2003. Haskell 98 Language and Libraries – The Revised Report. Cambridge University Press, Cambridge, England.Google Scholar
- Simon L. Peyton Jones. 1992. Implementing Lazy Functional Languages on Stock Hardware: The Spineless Tagless G-Machine. J. Funct. Program. 2, 2 (1992), 127–202.Google ScholarCross Ref
- Benjamin C. Pierce. 2002. Types and programming languages. The MIT Press. Google ScholarDigital Library
- Gordon D. Plotkin and A. John Power. 2004. Computational Effects and Operations: An Overview. Electronic Notes in Theoretical Computer Science 73 (2004), 149–163. Google ScholarDigital Library
- Gordon D. Plotkin and John Power. 2001. Semantics for Algebraic Operations. Electr. Notes Theor. Comput. Sci. 45 (2001), 332–345.Google ScholarCross Ref
- Gordon D. Plotkin and John Power. 2002. Notions of Computation Determine Monads. In Foundations of Software Science and Computation Structures, 5th International Conference, FOSSACS 2002. Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2002 Grenoble, France, April 8-12, 2002, Proceedings (Lecture Notes in Computer Science), Mogens Nielsen and Uffe Engberg (Eds.), Vol. 2303. Springer, 342–356. Google ScholarDigital Library
- Gordon D. Plotkin and Matija Pretnar. 2013. Handling Algebraic Effects. Logical Methods in Computer Science 9, 4:23 (2013), 1–36.Google Scholar
- Amr Hany Saleh, Georgios Karachalias, Matija Pretnar, and Tom Schrijvers. 2018. Explicit Effect Subtyping. In Programming Languages and Systems - 27th European Symposium on Programming, ESOP 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Thessaloniki, Greece, April 14-20, 2018, Proceedings (Lecture Notes in Computer Science), Amal Ahmed (Ed.), Vol. 10801. Springer, 327–354.Google ScholarCross Ref
- Mads Tofte and Jean-Pierre Talpin. 1997. Region-based Memory Management. Inf. Comput. 132, 2 (1997), 109–176. 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
Index Terms
- Abstracting algebraic effects
Recommendations
Handle with care: relational interpretation of algebraic effects and handlers
Algebraic effects and handlers have received a lot of attention recently, both from the theoretical point of view and in practical language design. This stems from the fact that algebraic effects give the programmer unprecedented freedom to define, ...
Type checking and typability in domain-free lambda calculi
This paper shows (1) the undecidability of the type checking and the typability problems in the domain-free lambda calculus with negation, product, and existential types, (2) the undecidability of the typability problem in the domain-free polymorphic ...
Type checking and inference for polymorphic and existential types
CATS '09: Proceedings of the Fifteenth Australasian Symposium on Computing: The Australasian Theory - Volume 94This paper proves undecidability of type checking and type inference problems in some variants of typed lambda calculi with polymorphic and existential types. First, type inference in the domain-free polymorphic lambda calculus is proved to be ...
Comments