Effekt: capability-passing style for type- and effect-safe, extensible effect handlers in Scala. (English) Zbl 1442.68024
Summary: Effect handlers are a promising way to structure effectful programs in a modular way. We present the Scala library Effekt, which is centered around capability passing and implemented in terms of a monad for multi-prompt delimited continuations. Effekt is the first library implementation of effect handlers that supports effect safety and effect polymorphism without resorting to type-level programming. We describe a novel way of achieving effect safety using intersection types and path-dependent types. The effect system of our library design fits well into the programming paradigm of capability passing and is inspired by the effect system of
Y. Zhang and A. C. Myers [“Abstraction-safe effect handlers via tunneling”, Proc. ACM Program. Lang. 3, No. POPL, Article No. 5, 29 p. (2019; doi:10.1145/3290318)].
Capabilities carry an abstract type member, which represents an individual effect type and reflects the use of the capability on the type level. We represent effect rows as the contravariant intersection of effect types. Handlers introduce capabilities and remove components of the intersection type. Reusing the existing type system of Scala, we get effect subtyping and effect polymorphism for free.
References:
| [1] | Amin, N. & Tate, R. (2016) Java and Scala’s type systems are unsound: The existential crisis of null pointers. In Proceedings of the Conference on Object-Oriented Programming, Systems, Languages and Applications. New York, NY, USA: ACM, pp. 838-848. |
| [2] | Bauer, A. & Pretnar, M. (2015) Programming with algebraic effects and handlers. J. Log. Alg. Methods Program.84(1), 108-123. · Zbl 1304.68025 |
| [3] | Biernacki, D., Piróg, M., Polesiuk, P., & Sieczkowski, F. (2017) Handle with care: Relational interpretation of algebraic effects and handlers. Proc. ACM Program. Lang. 2(POPL), 8:1-8:30. |
| [4] | Biernacki, D., Piróg, M., Polesiuk, P. & Sieczkowski, F. (2019) Abstracting algebraic effects. Proc. ACM Program. Lang. 3(POPL), 6:1-6:28. |
| [5] | Brachthäuser, J. I. & Schuster, P. (2017) Effekt: Extensible algebraic effects in Scala (short paper). In Proceedings of the International Symposium on Scala. New York, NY, USA: ACM. |
| [6] | Brachthäuser, J. I., Schuster, P. & Ostermann, K. (2018) Effect handlers for the masses. Proc. ACM Program. Lang. 2(OOPSLA), 111:1-111:27. · Zbl 1442.68024 |
| [7] | Carette, J., Kiselyov, O. & Shan, C.-C. (2007) Finally tagless, partially evaluated. In Proceedings of the Asian Symposium on Programming Languages and Systems. LNCS, vol. 4807. Berlin, Heidelberg: Springer, pp. 222-238. · Zbl 1191.68158 |
| [8] | Convent, L., Lindley, S., Mcbride, C. & Mclaughlin, C. (2019) Doo Bee Doo Bee Doo. Technical report. The University of Edinburgh. · Zbl 1442.68026 |
| [9] | Danvy, O. & Filinski, A. (1992) Representing control: A study of the CPS transformation. Math. Struct. Comput. Sci.2(4), 361-391. · Zbl 0798.68102 |
| [10] | Danvy, O. & Filinski, A. (1989) A functional abstraction of typed contexts. Diku rapport 89/12, diku, University of Copenhagen. |
| [11] | Danvy, O. & Filinski, A. (1990) Abstracting control. In Proceedings of the Conference on LISP and Functional Programming. New York, NY, USA: ACM, pp. 151-160. |
| [12] | Dolan, S., Eliopoulos, S., Hillerström, D., Madhavapeddy, A., Sivaramakrishnan, K. C. & White, L. (2017) Concurrent system programming with effect handlers. In Proceedings of the Symposium on Trends in Functional Programming. LNCS, vol. 10788. Springer. |
| [13] | Dolan, S., White, L. & Madhavapeddy, A. (2014) Multicore OCaml. In OCaml Workshop. |
| [14] | Dolan, S., White, L., Sivaramakrishnan, K. C., Yallop, J. & Madhavapeddy, A. (2015) Effective concurrency through algebraic effects. In OCaml Workshop. |
| [15] | Dybvig, R. K., Peyton, J., Simon, L. & Sabry, A. (2007) A monadic framework for delimited continuations. J. Funct. Program.17(6), 687-730. · Zbl 1130.68038 |
| [16] | Felleisen, M. (1988) The theory and practice of first-class prompts. In Proceedings of the Symposium on Principles of Programming Languages. New York, NY, USA: ACM, pp. 180-190. |
| [17] | Forster, Y., Kammar, O., Lindley, S. & Pretnar, M. (2017) On the expressive power of userdefined effects: Effect handlers, monadic reflection, delimited control. Proc. ACM Program. Lang.1(ICFP), 13:1-13:29. |
| [18] | Friedman, D. P., Haynes, C. T. & Kohlbecker, E. (1984) Programming with continuations. In Program Transformation and Programming Environments, Pepper, P. (ed), Berlin, Heidelberg: Springer-Verlag. · Zbl 0547.68014 |
| [19] | Gaster, B. R. & Jones, M. P. (1996) A Polymorphic Type System for Extensible Records and Variants. Technical report NOTTCS-TR-96-3. |
| [20] | Gunter, C. A., Rémy, D. & Riecke, J. G. (1995) A generalization of exceptions and control in ML-like languages. In Proceedings of the Conference on Functional Programming Languages and Computer Architecture. New York, NY, USA: ACM, pp. 12-23. |
| [21] | Haller, P. & Loiko, A. (2016) LaCasa: Lightweight affinity and object capabilities in Scala. In Proceedings of the Conference on Object-Oriented Programming, Systems, Languages and Applications. New York, NY, USA: ACM, pp. 272-291. |
| [22] | Hieb, R. & Dybvig, R. K. (1990) Continuations and concurrency. In Proceedings of the Second ACM SIGPLAN Symposium on Principles & Practice of Parallel Programming. PPOPP’90. New York, NY, USA: ACM, pp. 128-136. |
| [23] | Hieb, R., Dybvig, R. K. & Anderson, Iii, C. W. (1994) Subcontinuations. Lisp Symb. Comput.7(1), 83-110. |
| [24] | Hillerström, D. & Lindley, S. (2016) Liberating effects with rows and handlers. In Proceedings of the Workshop on Type-Driven Development. New York, NY, USA: ACM. |
| [25] | Hillerström, D., Lindley, S., Atkey, B. & Sivaramakrishnan, K. C. (2017) Continuation passing style for effect handlers. In Formal Structures for Computation and Deduction, LIPIcs, vol. 84. Schloss Dagstuhl-Leibniz-Zentrum für Informatik. · Zbl 1441.68017 |
| [26] | Hudak, P. (1998) Modular domain specific languages and tools. In Proceedings of the Conference on Software Reuse. IEEE Computer Society, pp. 134-142. |
| [27] | Inostroza, P. & Van Der Storm, T. (2018). JEff: Objects for effect. In Proceedings of the 2018 ACM SIGPLAN International Symposium on New Ideas, New Paradigms, and Reflections on Programming and Software. Onward! 2018. New York, NY, USA: ACM. |
| [28] | Johnson, G. F. & Duggan, D. (1988). Stores and partial continuations as first-class objects in a language and its environment. In Proceedings of the Symposium on Principles of Programming Languages. New York, NY, USA: ACM, pp. 158-168. |
| [29] | Kammar, O., Lindley, S. & Oury, N. (2013) Handlers in action. In Proceedings of the International Conference on Functional Programming. New York, NY, USA: ACM, pp. 145-158. · Zbl 1323.68126 |
| [30] | Kiselyov, O. & Ishii, H. (2015) Freer monads, more extensible effects. In Proceedings of the Haskell Symposium. New York, NY, USA: ACM, pp. 94-105. |
| [31] | Kiselyov, O. & Shan, C.-C. (2008) Lightweight monadic regions. In Proceedings of the Haskell Symposium. Haskell’08. New York, NY, USA: ACM. |
| [32] | Kiselyov, O. & Sivaramakrishnan, K. C. (2016). Eff directly in OCaml. In ML Workshop. |
| [33] | Kiselyov, O. & Sivaramakrishnan, K. C. (2018) Eff directly in OCaml. In Proceedings of the ML Family Workshop/OCaml Users and Developers Workshops, Asai, K. & Shinwell, M. (eds). Electronic Proceedings in Theoretical Computer Science, vol. 285. Open Publishing Association, pp. 23-58. |
| [34] | Kiselyov, O., Sabry, A. & Swords, C. (2013) Extensible effects: An alternative to monad transformers. In Proceedings of the Haskell Symposium. New York, NY, USA: ACM, pp. 59-70. |
| [35] | Kiselyov, O., Shan, C.-C. & Sabry, A. (2006) Delimited dynamic binding. In Proceedings of the International Conference on Functional Programming. New York, NY, USA: ACM, pp. 26-37. · Zbl 1321.68128 |
| [36] | Kobori, I., Kameyama, Y. & Kiselyov, O. (2016) Answer-type modification without tears: Promptpassing style translation for typed delimited-control operators. arxiv preprint arxiv:1606.06379. |
| [37] | Launchbury, J. & Sabry, A. (1997) Monadic state: Axiomatization and type safety. In Proceedings of the International Conference on Functional Programming. ICFP’97. New York, NY, USA: ACM, pp. 227-238. · Zbl 1369.68107 |
| [38] | Leijen, D. (2014) Koka: Programming with row polymorphic effect types. In Proceedings of the Workshop on Mathematically Structured Functional Programming. · Zbl 1464.68062 |
| [39] | Leijen, D. (2016) Algebraic Effects for Functional Programming. Technical report MSR-TR-2016-29. Microsoft Research technical report. |
| [40] | Leijen, D. (2017a) Implementing algebraic effects in C. In Proceedings of the Asian Symposium on Programming Languages and Systems. Cham, Switzerland: Springer International Publishing, pp. 339-363. |
| [41] | Leijen, D. (2017b). Structured asynchrony with algebraic effects. In Proceedings of the Workshop on Type-Driven Development. New York, NY, USA: ACM, pp. 16-29. |
| [42] | Leijen, D. (2017c). Type directed compilation of row-typed algebraic effects. In Proceedings of the Symposium on Principles of Programming Languages. New York, NY, USA: ACM, pp. 486-499. · Zbl 1380.68097 |
| [43] | Leijen, D. (2018). First class dynamic effect handlers: Or, polymorphic heaps with dynamic effect handlers. In Proceedings of the Workshop on Type-Driven Development. New York, NY, USA: ACM, pp. 51-64. |
| [44] | Liang, S., Hudak, P. & Jones, M. (1995)Monad transformers and modular interpreters. In Proceedings of the Symposium on Principles of Programming Languages. New York, NY, USA: ACM, pp. 333-343. |
| [45] | Lindley, S. (2018) Encapsulating effects. Dagstuhl Reports, 8(4). |
| [46] | Lindley, S., Mcbride, C. & Mclaughlin, C. (2017) Do be do be do. In Proceedings of the Symposium on Principles of Programming Languages. New York, NY, USA: ACM, pp. 500-514. · Zbl 1380.68098 |
| [47] | Liu, F. (2016) A Study of Capability-Based Effect Systems. M.Phil. thesis, École Polytechnique Fédérale de Lausanne, Switzerland. |
| [48] | Materzok, M. & Biernacki, D. (2011) Subtyping delimited continuations. In Proceedings of the International Conference on Functional Programming. New York, NY, USA: ACM, pp. 81-93. · Zbl 1323.68081 |
| [49] | Moggi, E. & Sabry, A. (2001) Monadic encapsulation of effects: A revised approach (extended version). J. Funct. Program.11(6), 591-627. · Zbl 1037.68023 |
| [50] | Odersky, M., Blanvillain, O., Liu, F., Biboudis, A., Miller, H. & Stucki, S. (2017) Simplicitly: Foundations and applications of implicit function types. Proc. ACM Program. Lang.2(POPL), 42:1-42:29. |
| [51] | Odersky, M. & Zenger, M. (2005a) Independently extensible solutions to the expression problem. In Proceedings of the Workshop on Foundations of Object-Oriented Languages. |
| [52] | Odersky, M. & Zenger, M. (2005b) Scalable component abstractions. In Proceedings of the Conference on Object-Oriented Programming, Systems, Languages and Applications. New York, NY, USA: ACM, pp. 41-57. |
| [53] | Oliveira, B. C. d. S., & Cook, W. R. (2012) Extensibility for the masses: Practical extensibility with object algebras. In Proceedings of the European Conference on Object-Oriented Programming. LNCS, vol. 7313. Springer, pp. 2-27. |
| [54] | Osvald, L., Essertel, G., Wu, X., Alayón, L. I. G.& Rompf, T. (2016) Gentrification gone too far? affordable 2nd-class values for fun and (co-) effect. In Proceedings of the Conference on Object-Oriented Programming, Systems, Languages and Applications. New York, NY, USA: ACM, pp. 234-251. |
| [55] | Parreaux, L., Voizard, A., Shaikhha, A. & Koch, C. E. (2017). Unifying analytic and statically-typed quasiquotes. Proc. ACM Program. Lang.2(POPL), 13:1-13:33. |
| [56] | Piróg, M., Polesiuk, P. & Sieczkowski, F. (2019) Typed equivalence of effect handlers and delimited control. In Formal Structures for Computation and Deduction. LIPIcs. Schloss Dagstuhl-Leibniz-Zentrum für Informatik, pp. 30:1-30:16. · Zbl 1524.68061 |
| [57] | Plotkin, G. & Power, J. (2003) Algebraic operations and generic effects. Appl. Categor. Struct.11(1), 69-94. · Zbl 1023.18006 |
| [58] | Plotkin, G. & Pretnar, M. (2009) Handlers of algebraic effects. In European Symposium on Programming. Springer-Verlag, pp. 80-94. · Zbl 1234.68059 |
| [59] | Plotkin, G. D. & Pretnar, M. (2013) Handling algebraic effects. Log. Methods Comput. Sci.9(4), 1-36. · Zbl 1314.68191 |
| [60] | Rapoport, M. & Lhoták, O. (2019). A path to DOT: formalizing fully-path-dependent types. Corr, abs/1904.07298. |
| [61] | Sitaram, D. & Felleisen, M. (1990) Control delimiters and their hierarchies. Lisp Symb. Comput.3(1), 67-99. |
| [62] | Wadler, P. (1998). The expression problem. Note to Java Genericity mailing list. |
| [63] | Wright, A. K. & Felleisen, M. (1994) A syntactic approach to type soundness. Inf. Comput.115(1), 38-94. · Zbl 0938.68559 |
| [64] | Wu, N., Schrijvers, T. & Hinze, R. (2014) Effect handlers in scope. In Proceedings of the Haskell Symposium. Haskell’14. New York, NY, USA: ACM, pp. 1-12. |
| [65] | Zhang, Y. & Myers, A. C. (2019) Abstraction-safe effect handlers via tunneling. Proc. ACM Program. Lang.3(POPL), 5:1-5:29. |
| [66] | Zhang, Y., Salvaneschi, G., Beightol, Q., Liskov, B. & Myers, A. C. (2016) Accepting blame for safe tunneled exceptions. Proceedings of the Conference on Programming Language Design and Implementation. New York, NY, USA: ACM, pp. 281-295. |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
