Type directed compilation of row-typed algebraic effects

ABSTRACT

Algebraic effect handlers, introduced by Plotkin and Power in 2002,

are recently gaining in popularity as a purely functional approach to

modeling effects. In this article, we give a full overview of

practical algebraic effects in the context of a compiled

implementation in the Koka language. In particular, we show how

algebraic effects generalize over common constructs like exception

handling, state, iterators and async-await. We give an effective type

inference algorithm based on extensible effect rows using scoped

labels, and a direct operational semantics. Finally, we show an

efficient compilation scheme to common runtime platforms (like

JavaScript) using a type directed selective CPS translation.

References

1. Kenichi Asai, and Yukiyoshi Kameyama. “Polymorphic Delimited Continuations.” In APLAS’07, 239–254. 2007.
2. Andrej Bauer, and Matija Pretnar. “An Effect System for Algebraic Effects and Handlers.” Logical Methods in Computer Science 10 (4). 2014.
3. Andrej Bauer, and Matija Pretnar. “Programming with Algebraic Effects and Handlers.” J. Log. Algebr. Meth. Program. 84 (1): 108–123. 2015.
4. Gavin Bierman, Claudio Russo, Geoffrey Mainland, Erik Meijer, and Mads Torgersen. “Pause ‘n’ Play: Formalizing Asynchronous C#.” In ECOOP 2012 – Object-Oriented Programming: 26th European Conference, Beijing, China, edited by James Noble, 233–257. Springer.
5. 2012.
6. Edwin Brady. “Programming and Reasoning with Algebraic Effects and Dependent Types.” In Proc. of ICFP’13, 133–144. 2013.
7. .
8. Olivier Danvy, and Andrzej Filinski. A Functional Abstraction of Typed Contexts. 1989.
9. Olivier Danvy, and Andrzej Filinski. “Abstracting Control.” In Proceedings of the 1990 ACM Conference on LISP and Functional Programming, 151–160. LFP ’90. Nice, France. 1990.
11. Olivier Danvy, and John Hatcliff. “CPS-Transformation After Strictness Analysis.” ACM Lett. Program. Lang. Syst. 1 (3). ACM: 195–212. Sep. 1992.
12. Olivier Danvy, Jung-taek Kim, and Kwangkeun Yi. “Assessing the Overhead of ML Exceptions by Selective CPS Transform.” In In Proceedings of the 1998 ACM SIGPLAN Workshop on ML, 103–114. 1998.
13. Olivier Danvy, Kevin Millikin, and Lasse R. Nielsen. “On One-Pass CPS Transformations.” J. Funct. Program. 17 (6): 793–812. Nov. 2007.
14. S Dolan, L White, Sivaramakrishnan K, Yallop J, and A Madhavapeddy. “Effective Concurrency through Algebraic Effects.” In OCaml Workshop. Sep. 2015.
15. Andrzej Filinski. “Representing Layered Monads.” In Proceedings of the 26th ACM Symposium on Principles of Programming Languages, 175–188. ACM Press. 1999.
16. Andrzej Filinski. “Monads in Action.” In Proceedings of the 37th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 483–494. 2010.
17. Ben R. Gaster, and Mark P. Jones. A Polymorphic Type System for Extensible Records and Variants. NOTTCS-TR-96-3. University of Nottingham. 1996.
18. Jean-Yves Girard. “The System F of Variable Types, Fifteen Years Later.” TCS. 1986.
19. Daniel Hillerström, and Sam Lindley. “Liberating Effects with Rows and Handlers.” TyDe 2016. Nara, Japan. 2016.
21. Graham Hutton, and Erik Meijer. Monadic Parser Combinators. NOTTCS-TR-96-4. Dept. of Computer Science, University of Nottingham. 1996. http://www.cs.nott.ac.uk/Dept.{}/Staff/ gmh/monparsing.ps.
22. Ohad Kammar, Sam Lindley, and Nicolas Oury. “Handlers in Action.” In Proceedings of the 18th ACM SIGPLAN International Conference on Functional Programming, 145–158. ICFP ’13. ACM, New York, NY, USA. 2013.
23. Ohad Kammar, and Matija Pretnar. “No Value Restriction Is Needed for Algebraic Effects and Handlers.” CoRR abs/1605.06938. 2016.
24. Oleg Kiselyov, and Hiromi Ishii. “Freer Monads, More Extensible Effects.” In Proceedings of the 2015 ACM SIGPLAN Symposium on Haskell, 94–105. Haskell ’15. Vancouver, BC, Canada. 2015.
26. Oleg Kiselyov, Amr Sabry, and Cameron Swords. “Extensible Effects: An Alternative to Monad Transformers.” In Proceedings of the 2013 ACM SIGPLAN Symposium on Haskell, 59–70. Haskell ’13. Boston, Massachusetts, USA. 2013.
27. Peter J. Landin. A Generalization of Jumps and Labels. UNIVAC systems programming research. 1965.
28. Peter J. Landin. “A Generalization of Jumps and Labels.” Higher-Order and Symbolic Computation 11 (2): 125–143. 1998.
29. reprint from {22}.
30. Daan Leijen. “Extensible Records with Scoped Labels.” In In: Proceedings of the 2005 Symposium on Trends in Functional Programming, 297–312. 2005.
31. Daan Leijen. “Koka: Programming with Row Polymorphic Effect Types.” In MSFP’14, 5th Workshop on Mathematically Structured Functional Programming. 2014.
32. Daan Leijen. “Madoko: Scholarly Documents for the Web.” In Proceedings of the 2015 ACM Symposium on Document Engineering, 129–132. DocEng ’15. ACM, Lausanne, Switzerland. 2015.
34. Daan Leijen. “Koka Overview and Reference.” 2016. http://bit. do/kokabook.
35. Daan Leijen, and Erik Meijer. Parsec: Direct Style Monadic Parser Combinators for the Real World. UU-CS-2001-27. Dept. of Computer Science, Universiteit Utrecht. 2001.
36. Sam Lindley, and James Cheney. “Row-Based Effect Types for Database Integration.” In TLDI’12, 91–102. 2012.
38. Sam Lindley, Connor McBride, and Craig McLaughlin. “Do Be Do Be Do.” In POPL 2017. Paris, France. 2016.
39. Florian Loitsch, Manuel Serrano, and Inria Sophia Antipolis. “Hop Client-Side Compilation.” In Proceedings of the 8th Symposium on Trends on Functional Languages. 2007.
40. Eugenio Moggi. “Notions of Computation and Monads.” Information and Computation 93 (1): 55–92. 1991.
41. Lasse R. Nielsen. “A Selective CPS Transformation.” Electronic Notes in Theoretical Comp. Sc. 45: 311–331. 2001. MFPS 2001, 17th Conf. on the Mathematical Foundations of Prog. Semantics.
42. Simon L. Peyton Jones, and André L. M. Santos. “A Transformation-Based Optimiser for Haskell.” Science of Computer Programming 32 (1): 3–47. 1998.
43. Gordon D. Plotkin, and Matija Pretnar. “Handling Algebraic Effects.” In Logical Methods in Computer Science, volume 9. 4. 2013.
45. Gordon Plotkin, and John Power. “Algebraic Operations and Generic Effects.” Applied Categorical Structures 11 (1): 69–94. 2003.
47. Matija Pretnar. “Inferring Algebraic Effects.” Logical Methods in Computer Science 10 (3). 2014.
48. Didier Rémy. “Type Inference for Records in Natural Extension of ML.” In Theoretical Aspects of Object-Oriented Programming, 67–95. 1994.
49. John Reppy. “Optimizing Nested Loops Using Local CPS Conversion.” Higher-Order and Symbolic Computation 15 (2): 161–180. 2002.
50. Tiark Rompf, Ingo Maier, and Martin Odersky. “Implementing First-Class Polymorphic Delimited Continuations by a Type-Directed Selective CPS-Transform.” In. ICFP. 2009.
51. Chung-chieh Shan. “A Static Simulation of Dynamic Delimited Control.” Higher-Order and Symbolic Computation 20 (4): 371–401. 2007.
53. Martin Sulzmann. Designing Record Systems. YALEU/DCS/RR-1128. Yale University. Apr. 1997.
54. Nikhil Swamy, Nataliya Guts, Daan Leijen, and Michael Hicks. “Lightweight Monadic Programming in ML.” In ICFP. 2011.
56. Wouter Swierstra. “Data Types à La Carte.” Journal of Functional Programming 18 (4): 423–436. Jul. 2008.
58. The EcmaScript committee. “ES6: The EcmaScript 2015 Language Specification.” 2015. http://www.ecma-international. org/ecma-262/6.0/ECMA-262.pdf.
59. The EcmaScript committee. “ES7: The Draft EcmaScript 2017 Language Specification.” 2016.
60. https://tc39.github.io/ecma262.
61. Hayo Thielecke. “Using a Continuation Twice and Its Implications for the Expressive Power of Call/Cc.” Higher Order Symbol. Comput. 12 (1). Kluwer Academic Publishers, Hingham, MA, USA: 47–73. Apr. 1999.
62. Eric Thivierge, and Marc Feeley. “Efficient Compilation of Tail Calls and Continuations to JavaScript.” In Proc. of the 2012 Annual Workshop on Scheme and Funct. Prog., 47–57. 2012.
64. Niki Vazou, and Daan Leijen. “From Monads to Effects and Back.” In 18th Int. Symp. on the Practical Aspects of Declarative Languages, 169–186. 2016.
65. Andrew K. Wright, and Matthias Felleisen. “A Syntactic Approach to Type Soundness.” Inf. Comput. 115 (1): 38–94. Nov. 1994.
67. Nicolas Wu, Tom Schrijvers, and Ralf Hinze. “Effect Handlers in Scope.” In Proceedings of the 2014 ACM SIGPLAN Symposium on Haskell, 1–12. Haskell ’14. ACM, New York, NY, USA. 2014.
69. Danny Yoo, and Shriram Krishnamurthi. “Whalesong: Running Racket in the Browser.” In Proceedings of the 9th Symposium on Dynamic Languages, 97–108. DLS ’13. ACM, Indianapolis, Indiana, USA. 2013.

Index Terms

• Software and its engineering

  • Software notations and tools

    • General programming languages

      • Language features