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.
- Kenichi Asai, and Yukiyoshi Kameyama. “Polymorphic Delimited Continuations.” In APLAS’07, 239–254. 2007. Google ScholarDigital Library
- Andrej Bauer, and Matija Pretnar. “An Effect System for Algebraic Effects and Handlers.” Logical Methods in Computer Science 10 (4). 2014.Google ScholarCross Ref
- Andrej Bauer, and Matija Pretnar. “Programming with Algebraic Effects and Handlers.” J. Log. Algebr. Meth. Program. 84 (1): 108–123. 2015.Google ScholarCross Ref
- 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. Google ScholarDigital Library
- 2012.Google Scholar
- Edwin Brady. “Programming and Reasoning with Algebraic Effects and Dependent Types.” In Proc. of ICFP’13, 133–144. 2013. Google ScholarDigital Library
- .Google Scholar
- Olivier Danvy, and Andrzej Filinski. A Functional Abstraction of Typed Contexts. 1989.Google Scholar
- 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. Google ScholarDigital Library
- Google ScholarDigital Library
- Olivier Danvy, and John Hatcliff. “CPS-Transformation After Strictness Analysis.” ACM Lett. Program. Lang. Syst. 1 (3). ACM: 195–212. Sep. 1992. Google Scholar
- 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.Google ScholarDigital Library
- Olivier Danvy, Kevin Millikin, and Lasse R. Nielsen. “On One-Pass CPS Transformations.” J. Funct. Program. 17 (6): 793–812. Nov. 2007. Google Scholar
- S Dolan, L White, Sivaramakrishnan K, Yallop J, and A Madhavapeddy. “Effective Concurrency through Algebraic Effects.” In OCaml Workshop. Sep. 2015.Google ScholarDigital Library
- Andrzej Filinski. “Representing Layered Monads.” In Proceedings of the 26th ACM Symposium on Principles of Programming Languages, 175–188. ACM Press. 1999. Google ScholarDigital Library
- Andrzej Filinski. “Monads in Action.” In Proceedings of the 37th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 483–494. 2010. Google Scholar
- Ben R. Gaster, and Mark P. Jones. A Polymorphic Type System for Extensible Records and Variants. NOTTCS-TR-96-3. University of Nottingham. 1996.Google ScholarDigital Library
- Jean-Yves Girard. “The System F of Variable Types, Fifteen Years Later.” TCS. 1986. Google ScholarDigital Library
- Daniel Hillerström, and Sam Lindley. “Liberating Effects with Rows and Handlers.” TyDe 2016. Nara, Japan. 2016. Google Scholar
- Google ScholarDigital Library
- 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.Google Scholar
- 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. Google ScholarDigital Library
- Ohad Kammar, and Matija Pretnar. “No Value Restriction Is Needed for Algebraic Effects and Handlers.” CoRR abs/1605.06938. 2016.Google ScholarDigital Library
- 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. Google Scholar
- Google ScholarDigital Library
- 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. Google Scholar
- Peter J. Landin. A Generalization of Jumps and Labels. UNIVAC systems programming research. 1965.Google Scholar
- Peter J. Landin. “A Generalization of Jumps and Labels.” Higher-Order and Symbolic Computation 11 (2): 125–143. 1998. Google Scholar
- reprint from {22}.Google ScholarDigital Library
- Daan Leijen. “Extensible Records with Scoped Labels.” In In: Proceedings of the 2005 Symposium on Trends in Functional Programming, 297–312. 2005.Google Scholar
- Daan Leijen. “Koka: Programming with Row Polymorphic Effect Types.” In MSFP’14, 5th Workshop on Mathematically Structured Functional Programming. 2014.Google Scholar
- 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. Google ScholarDigital Library
- Google ScholarDigital Library
- Daan Leijen. “Koka Overview and Reference.” 2016. http://bit. do/kokabook.Google Scholar
- 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.Google ScholarDigital Library
- Sam Lindley, and James Cheney. “Row-Based Effect Types for Database Integration.” In TLDI’12, 91–102. 2012. Google ScholarCross Ref
- Google ScholarDigital Library
- Sam Lindley, Connor McBride, and Craig McLaughlin. “Do Be Do Be Do.” In POPL 2017. Paris, France. 2016. Google ScholarCross Ref
- Florian Loitsch, Manuel Serrano, and Inria Sophia Antipolis. “Hop Client-Side Compilation.” In Proceedings of the 8th Symposium on Trends on Functional Languages. 2007.Google ScholarCross Ref
- Eugenio Moggi. “Notions of Computation and Monads.” Information and Computation 93 (1): 55–92. 1991. Google ScholarCross Ref
- 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.Google ScholarDigital Library
- Simon L. Peyton Jones, and André L. M. Santos. “A Transformation-Based Optimiser for Haskell.” Science of Computer Programming 32 (1): 3–47. 1998. Google ScholarDigital Library
- Gordon D. Plotkin, and Matija Pretnar. “Handling Algebraic Effects.” In Logical Methods in Computer Science, volume 9. 4. 2013.Google ScholarDigital Library
- Google ScholarDigital Library
- Gordon Plotkin, and John Power. “Algebraic Operations and Generic Effects.” Applied Categorical Structures 11 (1): 69–94. 2003.Google Scholar
- Google ScholarDigital Library
- Matija Pretnar. “Inferring Algebraic Effects.” Logical Methods in Computer Science 10 (3). 2014.Google ScholarDigital Library
- Didier Rémy. “Type Inference for Records in Natural Extension of ML.” In Theoretical Aspects of Object-Oriented Programming, 67–95. 1994.Google Scholar
- John Reppy. “Optimizing Nested Loops Using Local CPS Conversion.” Higher-Order and Symbolic Computation 15 (2): 161–180. 2002. Google Scholar
- Tiark Rompf, Ingo Maier, and Martin Odersky. “Implementing First-Class Polymorphic Delimited Continuations by a Type-Directed Selective CPS-Transform.” In. ICFP. 2009. Google Scholar
- Chung-chieh Shan. “A Static Simulation of Dynamic Delimited Control.” Higher-Order and Symbolic Computation 20 (4): 371–401. 2007. Google ScholarDigital Library
- Google ScholarDigital Library
- Martin Sulzmann. Designing Record Systems. YALEU/DCS/RR-1128. Yale University. Apr. 1997.Google ScholarCross Ref
- Nikhil Swamy, Nataliya Guts, Daan Leijen, and Michael Hicks. “Lightweight Monadic Programming in ML.” In ICFP. 2011. Google ScholarDigital Library
- Google ScholarDigital Library
- Wouter Swierstra. “Data Types à La Carte.” Journal of Functional Programming 18 (4): 423–436. Jul. 2008. Google ScholarDigital Library
- Google Scholar
- The EcmaScript committee. “ES6: The EcmaScript 2015 Language Specification.” 2015. http://www.ecma-international. org/ecma-262/6.0/ECMA-262.pdf.Google Scholar
- The EcmaScript committee. “ES7: The Draft EcmaScript 2017 Language Specification.” 2016.Google Scholar
- https://tc39.github.io/ecma262.Google Scholar
- 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. Google Scholar
- 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. Google Scholar
- Google Scholar
- 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.Google Scholar
- Andrew K. Wright, and Matthias Felleisen. “A Syntactic Approach to Type Soundness.” Inf. Comput. 115 (1): 38–94. Nov. 1994. Google Scholar
- Google Scholar
- 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. Google Scholar
- Google Scholar
- 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. Google Scholar
Index Terms
- Type directed compilation of row-typed algebraic effects
Recommendations
Type directed compilation of row-typed algebraic effects
POPL '17Algebraic 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 ...
An Intrinsically Typed Compiler for Algebraic Effect Handlers
PEPM 2024: Proceedings of the 2024 ACM SIGPLAN International Workshop on Partial Evaluation and Program ManipulationA type-preserving compiler converts a well-typed input program into a well-typed output program. Previous studies have developed type-preserving compilers for various source languages, including the simply-typed lambda calculus and calculi with control ...
The impact of optional type information on jit compilation of dynamically typed languages
DLS '11: Proceedings of the 7th symposium on Dynamic languagesOptionally typed languages enable direct performance comparisons between untyped and type annotated source code. We present a comprehensive performance evaluation of two different JIT compilers in the context of ActionScript, a production-quality ...
Comments