Daniel Hillerström
ABSTRACT
Algebraic effects and effect handlers provide a modular abstraction for effectful programming. They support user-defined effects, as in Haskell, in conjunction with direct-style effectful programming, as in ML. They also present a structured interface to programming with delimited continuations.
In order to be modular, it is necessary for an effect type system to support extensible effects. Row polymorphism is a natural abstraction for modelling extensibility at the level of types. In this paper we argue that the abstraction required to implement extensible effects and their handlers is exactly row polymorphism.
We use the Links functional web programming language as a platform to substantiate this claim. Links is a natural starting point as it uses row polymorphism for polymorphic variants, records, and its built-in effect types. It also has infrastructure for manipulating continuations. Through a small extension to Links we smoothly add support for effect handlers, making essential use of rows in the frontend and first-class continuations in the backend.
We demonstrate the usability of our implementation by modelling the mathematical game of Nim as an abstract computation. We interpret this abstract computation in a variety of ways, illustrating how rows and handlers support modularity and smooth composition of effectful computations.
We present a core calculus of row-polymorphic effects and handlers based on a variant of A-normal form used in the intermediate representation of Links. We give an operational semantics for the calculus and a novel generalisation of the CEK machine that implements the operational semantics, and prove that the two coincide.
- R. Atkey. Parameterised notions of computation. Journal of Functional Programming, 19(3-4):335–376, 2009. Google Scholar
Digital Library
- A. Bauer and M. Pretnar. An effect system for algebraic effects and handlers. Logical Methods in Computer Science, 10(4), 2014.Google Scholar
- A. Bauer and M. Pretnar. Programming with algebraic effects and handlers. Journal of Logical and Algebraic Methods in Programming, 84(1):108–123, 2015.Google ScholarCross Ref
- M. Blume, U. A. Acar, and W. Chae. Exception handlers as extensible cases. In G. Ramalingam, editor, Programming Languages and Systems, 6th Asian Symposium, APLAS 2008, Bangalore, India, December 9-11, 2008. Proceedings, volume 5356 of Lecture Notes in Computer Science, pages 273–289. Springer, 2008. Google ScholarDigital Library
- C. L. Bouton. Nim, a game with a complete mathematical theory. The Annals of Mathematics, 3(1/4):35–39, 1901.Google ScholarCross Ref
- E. Brady. Programming and reasoning with algebraic effects and dependent types. In Morrisett and Uustalu {27}, pages 133–144. Google ScholarDigital Library
- C. Bruggeman, O. Waddell, and R. K. Dybvig. Representing control in the presence of one-shot continuations. In C. N. Fischer, editor, Proceedings of the ACM SIGPLAN’96 Conference on Programming Language Design and Implementation (PLDI), Philadephia, Pennsylvania, May 21-24, 1996, pages 99–107. ACM, 1996. Google ScholarDigital Library
- E. Cooper, S. Lindley, P. Wadler, and J. Yallop. Links: Web programming without tiers. In F. S. de Boer, M. M. Bonsangue, S. Graf, and W. P. de Roever, editors, Formal Methods for Components and Objects, 5th International Symposium, FMCO 2006, Amsterdam, The Netherlands, November 7-10, 2006, Revised Lectures, volume 4709 of Lecture Notes in Computer Science, pages 266–296. Springer, 2006. Google ScholarDigital Library
- S. Dolan, L. White, K. Sivaramakrishnan, J. Yallop, and A. Madhavapeddy. Effective concurrency through algebraic effects. OCaml Workshop, September 2015.Google Scholar
- M. Felleisen and D. P. Friedman. Control operators, the SECDmachine, and the λ-calculus. In The Proceedings of the Conference on Formal Description of Programming Concepts III, Ebberup, Denmark, pages 193–217. Elsevier, 1987.Google Scholar
- C. Flanagan, A. Sabry, B. F. Duba, and M. Felleisen. The essence of compiling with continuations. In Proceedings of the ACM SIGPLAN 1993 Conference on Programming Language Design and Implementation, PLDI ’93, pages 237–247, New York, NY, USA, 1993. ACM. Google ScholarDigital Library
- D. Hillerström. Handlers for algebraic effects in Links. Master’s thesis, The University of Edinburgh, Scotland, 2015.Google Scholar
- D. Hillerström, S. Lindley, and K. Sivaramakrishnan. Compiling Links effect handlers to the OCaml backend. ML Workshop, 2016.Google Scholar
- S. Holmes. Compiling Links server-side code. Bachelor thesis, The University of Edinburgh, 2009.Google Scholar
- O. Kammar, S. Lindley, and N. Oury. Handlers in action. In Morrisett and Uustalu {27}, pages 145–158. Google ScholarDigital Library
- O. Kiselyov and H. Ishii. Freer monads, more extensible effects. In B. Lippmeier, editor, Proceedings of the 8th ACM SIGPLAN Symposium on Haskell, Haskell 2015, Vancouver, BC, Canada, September 3-4, 2015, pages 94–105. ACM, 2015. Google ScholarDigital Library
- O. Kiselyov, A. Sabry, and C. Swords. Extensible effects: an alternative to monad transformers. In C. Shan, editor, Proceedings of the 2013 ACM SIGPLAN Symposium on Haskell, Boston, MA, USA, September 23-24, 2013, pages 59–70. ACM, 2013. Google ScholarDigital Library
- D. Leijen. Koka: Programming with row polymorphic effect types. In P. Levy and N. Krishnaswami, editors, Proceedings 5th Workshop on Mathematically Structured Functional Programming, MSFP, Grenoble, France, April 2014, volume 153 of EPTCS, pages 100–126, 2014.Google Scholar
- X. Leroy and F. Pessaux. Type-based analysis of uncaught exceptions. ACM Transactions on Programming Languages and Systems, 22(2): 340–377, 2000. Google ScholarDigital Library
- P. B. Levy, J. Power, and H. Thielecke. Modelling environments in call-by-value programming languages. Information and Computation, 185(2):182–210, 2003. Google ScholarDigital Library
- S. Liang, P. Hudak, and M. P. Jones. Monad transformers and modular interpreters. In R. K. Cytron and P. Lee, editors, Conference Record of POPL’95: 22nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, San Francisco, California, USA, January 23-25, 1995, pages 333–343. ACM Press, 1995. Google ScholarDigital Library
- S. Lindley and J. Cheney. Row-based effect types for database integration. In B. C. Pierce, editor, Proceedings of TLDI 2012: The Seventh ACM SIGPLAN Workshop on Types in Languages Design and Implementation, Philadelphia, PA, USA, Saturday, January 28, 2012, pages 91–102. ACM, 2012. Google ScholarDigital Library
- S. Lindley, C. McBride, and C. McLaughlin. Do be do be do.Google Scholar
- C. McBride. Shonky, 2016. https://github.com/pigworker/ shonky.Google Scholar
- J. G. Morris. Variations on variants. In B. Lippmeier, editor, Proceedings of the 8th ACM SIGPLAN Symposium on Haskell, Haskell 2015, Vancouver, BC, Canada, 2015, pages 71–81. ACM, 2015. Google ScholarDigital Library
- J. G. Morris and M. P. Jones. Instance chains: type class programming without overlapping instances. In P. Hudak and S. Weirich, editors, Proceeding of the 15th ACM SIGPLAN International Conference on Functional Programming, ICFP 2010, Baltimore, Maryland, USA, September 27-29, 2010, pages 375–386. ACM, 2010. Google ScholarDigital Library
- G. Morrisett and T. Uustalu, editors. ACM SIGPLAN International Conference on Functional Programming, ICFP’13, Boston, MA, USA - September 25 - 27, 2013, 2013. ACM. Google ScholarCross Ref
- D. A. Orchard and T. Petricek. Embedding effect systems in Haskell. In W. Swierstra, editor, Proceedings of the 2014 ACM SIGPLAN symposium on Haskell, Gothenburg, Sweden, September 4-5, 2014, pages 13–24. ACM, 2014. Google ScholarDigital Library
- G. D. Plotkin and J. Power. Adequacy for algebraic effects. In F. Honsell and M. Miculan, editors, Foundations of Software Science and Computation Structures, 4th International Conference, FOSSACS Genova, Italy, April 2-6, 2001, Proceedings, volume 2030 of Lecture Notes in Computer Science, pages 1–24. Springer, 2001. Google ScholarDigital Library
- G. D. Plotkin and M. Pretnar. Handling algebraic effects. Logical Methods in Computer Science, 9(4), 2013.Google Scholar
- M. Pretnar. Inferring algebraic effects. Logical Methods in Computer Science, 10(3), 2014.Google Scholar
- M. Pretnar. An introduction to algebraic effects and handlers. invited tutorial paper. Electronic Notes in Theoretical Computer Science, 319: 19–35, 2015. Google ScholarDigital Library
- D. Rémy. Theoretical aspects of object-oriented programming. chapter Type Inference for Records in Natural Extension of ML, pages 67– 95. MIT Press, Cambridge, MA, USA, 1994.Google Scholar
- W. Swierstra. Data types à la carte. Journal of Functional Programming, 18(4):423–436, 2008. Google ScholarDigital Library
- N. Wu and T. Schrijvers. Fusion for free - efficient algebraic effect handlers. In R. Hinze and J. Voigtländer, editors, Mathematics of Program Construction - 12th International Conference, MPC 2015, Königswinter, Germany, 2015. Proceedings, volume 9129 of Lecture Notes in Computer Science, pages 302–322. Springer, 2015.Google Scholar
- N. Wu, T. Schrijvers, and R. Hinze. Effect handlers in scope. In Proceedings of the 2014 ACM SIGPLAN Symposium on Haskell, Haskell ’14, pages 1–12, New York, NY, USA, 2014. ACM. Google ScholarDigital Library
- B. A. Yorgey, S. Weirich, J. Cretin, S. L. P. Jones, D. Vytiniotis, and J. P. Magalh˜aes. Giving Haskell a promotion. In B. C. Pierce, editor, Proceedings of TLDI 2012: The Seventh ACM SIGPLAN Workshop on Types in Languages Design and Implementation, Philadelphia, PA, USA, Saturday, January 28, 2012, pages 53–66. ACM, 2012. Google ScholarDigital Library
Index Terms
- Liberating effects with rows and handlers
Recommendations
Effects as capabilities: effect handlers and lightweight effect polymorphism
Effect handlers have recently gained popularity amongst programming language researchers. Existing type- and effect systems for effect handlers are often complicated and potentially hinder a wide-spread adoption.
We present the language Effekt with the ...
Effect handlers for the masses
Effect handlers are a program structuring paradigm with rising popularity in the functional programming language community and can express many advanced control flow abstractions. We present the first implementation of effect handlers for Java - an ...
Handlers in action
ICFP '13: Proceedings of the 18th ACM SIGPLAN international conference on Functional programmingPlotkin 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, ...
Comments