Handlers in action

Abstract

Plotkin and Pretnar's handlers for algebraic effects occupy a sweet spot in the design space of abstractions for effectful computation. By separating effect signatures from their implementation, algebraic effects provide a high degree of modularity, allowing programmers to express effectful programs independently of the concrete interpretation of their effects. A handler is an interpretation of the effects of an algebraic computation. The handler abstraction adapts well to multiple settings: pure or impure, strict or lazy, static types or dynamic types. This is a position paper whose main aim is to popularise the handler abstraction. We give a gentle introduction to its use, a collection of illustrative examples, and a straightforward operational semantics. We describe our Haskell implementation of handlers in detail, outline the ideas behind our OCaml, SML, and Racket implementations, and present experimental results comparing handlers with existing code.

References

1. Z. M. Ariola, H. Herbelin, and A. Sabry. A type-theoretic foundation of delimited continuations. phHigher-Order and Symbolic Computation, 22 (3): 233--273, 2009.
2. A. Bauer and M. Pretnar. Programming with algebraic effects and handlers. phCoRR, abs/1203.1539, 2012.
3. N. Benton and A. Kennedy. Exceptional syntax. phJ. Funct. Program., 11 (4): 395--410, 2001.
4. N. Benton, J. Hughes, and E. Moggi. Monads and effects. In phAPPSEM 2000. Springer-Verlag, 2002.
5. M. Blume, U. A. Acar, and W. Chae. Exception handlers as extensible cases. In phAPLAS. Springer-Verlag, 2008.
6. E. Brady. Programming and reasoning with algebraic effects and dependent types. In phICFP. ACM, 2013.
7. B. C. d. S. Oliveira, T. Schrijvers, and W. R. Cook. MRI: Modular reasoning about interference in incremental programming. phJ. Funct. Program., 22 (6): 797--852, 2012.
8. O. Danvy and A. Filinski. Abstracting control. In phLFP. ACM, 1990.
9. M. Felleisen. The theory and practice of first-class prompts. In phPOPL. ACM, 1988.
10. A. Filinski. Representing layered monads. In phPOPL. ACM, 1999.
11. A. Filinski. Monads in action. In phPOPL. ACM, 2010.
12. A. Gill. The mtl package (2.1.2), 2012.\ http://hackage.haskell.org/package/mtl.
13. G. Gonzalez. pipes-2.5: Faster and slimmer, 2012.\ http://www.haskellforall.com/2012/10/pipes-25-faster-and-slimmer.html.
14. G. Gonzalez. The pipes package (3.2.0), 2013.\ http://hackage.haskell.org/package/pipes.
15. M. Hyland, G. D. Plotkin, and J. Power. Combining effects: Sum and tensor. phTheoret. Comput. Sci., pages 70--99, 2006.
16. M. Jaskelioff. Monatron: An extensible monad transformer library. In phIFL. Springer-Verlag, 2008.
17. M. Jaskelioff and E. Moggi. Monad transformers as monoid transformers. phTheoret. Comput. Sci., 411 (51--52), 2010.
18. M. P. Jones. Functional programming with overloading and higher-order polymorphism. In phAdvanced Functional Programming, 1995.
19. O. Kammar and G. D. Plotkin. Algebraic foundations for effect-dependent optimisations. In phPOPL. ACM, 2012.
20. S. Katsumata. Relating computational effects by $\top\top$-lifting. phInf. Comput., 222, 2013.
21. O. Kiselyov. Iteratees. In phFLOPS. Springer-Verlag, 2012.
22. O. Kiselyov and C.-c. Shan. Embedded probabilistic programming. In phDSL. Springer-Verlag, 2009.
23. X. Leroy and F. Pessaux. Type-based analysis of uncaught exceptions. phACM Trans. Program. Lang. Syst., pages 340--377, 2000.
24. P. B. Levy. phCall-By-Push-Value: A Functional/Imperative Synthesis, volume 2 of phSemantics Structures in Computation. Springer, 2004.
25. S. Liang, P. Hudak, and M. P. Jones. Monad transformers and modular interpreters. In phPOPL. ACM, 1995.
26. S. Lindley. Extensional rewriting with sums. In phTLCA. Springer-Verlag, 2007.
27. S. Lindley and J. Cheney. Row-based effect types for database integration. In phTLDI. ACM, 2012.
28. G. Mainland. Why it's nice to be quoted: quasiquoting for Haskell. In phHaskell. ACM, 2007.
29. C. McBride. Frank (0.3), 2012.\ http://hackage.haskell.org/package/Frank.
30. E. Moggi. Computational lambda-calculus and monads. In phLICS. IEEE Computer Society, 1989.
31. B. O'Sullivan. The criterion package (0.8.0.0), 2013.\ http://hackage.haskell.org/package/criterion.
32. A. S. Patricia Johann and J. Voigtl\"ander. A generic operational metatheory for algebraic effects. In phLICS. IEEE Computer Society, 2010.
33. G. D. Plotkin and J. Power. Adequacy for algebraic effects. In phFoSSaCS. Springer-Verlag, 2001.
34. G. D. Plotkin and J. Power. Notions of computation determine monads. In phFoSSaCS. Springer-Verlag, 2002.
35. G. D. Plotkin and J. Power. Algebraic operations and generic effects. phAppl. Categ. Structures, 11 (1): 69--94, 2003.
36. G. D. Plotkin and M. Pretnar. Handlers of algebraic effects. In phESOP. Springer-Verlag, 2009.
37. (1993)}Remy93D. Rémy. Type inference for records in a natural extension of ML. In C. A. Gunter and J. C. Mitchell, editors, phTheoretical Aspects Of Object-Oriented Programming. Types, Semantics and Language Design. MIT Press, 1993.
38. T. Schrijvers and B. C. d. S. Oliveira. Monads, zippers and views: virtualizing the monad stack. In phICFP. ACM, 2011.
39. C.-c. Shan. A static simulation of dynamic delimited control. phHigher-Order and Symbolic Computation, 20 (4): 371--401, 2007.
40. T. Sheard and S. L. P. Jones. Template meta-programming for Haskell. phSIGPLAN Notices, 37 (12): 60--75, 2002.
41. S. Staton. Two cotensors in one: Presentations of algebraic theories for local state and fresh names. phElectr. Notes Theor. Comput. Sci., 249: 471--490, 2009.
42. N. Swamy, N. Guts, D. Leijen, and M. Hicks. Lightweight monadic programming in ML. In phICFP. ACM, 2011.
43. W. Swierstra. Data types à la carte. phJ. Funct. Program., 18 (4): 423--436, 2008.
44. S. Visscher. The effects package (0.2.2), 2012.\ http://hackage.haskell.org/package/effects.
45. er(2008)}Voigtlander08J. Voigtl\"ander. Asymptotic improvement of computations over free monads. In phMPC. Springer-Verlag, 2008.
46. P. Wadler. Monads for functional programming. In phAdvanced Functional Programming. Springer-Verlag, 1995.

Index Terms

• Software and its engineering

  • Software notations and tools

    • Formal language definitions

    • General programming languages

      • Language types

        • Functional languages

• Theory of computation

  • Formal languages and automata theory