×

Programming with algebraic effects and handlers. (English) Zbl 1304.68025

Summary: Eff is a programming language based on the algebraic approach to computational effects, in which effects are viewed as algebraic operations and effect handlers as homomorphisms from free algebras. Eff supports first-class effects and handlers through which we may easily define new computational effects, seamlessly combine existing ones, and handle them in novel ways. We give a denotational semantics of Eff and discuss a prototype implementation based on it. Through examples we demonstrate how the standard effects are treated in Eff, and how Eff supports programming techniques that use various forms of delimited continuations, such as backtracking, breadth-first search, selection functionals, cooperative multi-threading, and others.

MSC:

68N15 Theory of programming languages
68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)

Software:

OCaml; Eff; ML
PDFBibTeX XMLCite
Full Text: DOI arXiv

References:

[1] Benton, Nick; Hughes, John; Moggi, Eugenio, Monads and effects, (Applied Semantics, International Summer School. Applied Semantics, International Summer School, APPSEM 2000, Caminha, Portugal, September 9-15, 2000. Applied Semantics, International Summer School. Applied Semantics, International Summer School, APPSEM 2000, Caminha, Portugal, September 9-15, 2000, Advanced Lectures (2002), Springer-Verlag: Springer-Verlag London, UK), 42-122 · Zbl 1065.68064
[2] Danvy, Oliver; Filinski, Andrzej, Representing control: a study of the CPS transformation, Math. Struct. Comput. Sci., 2, 4, 361-391 (1992) · Zbl 0798.68102
[3] Escardó, Martín; Oliva, Paulo, Selection functions, bar recursion and backward induction, Math. Struct. Comput. Sci., 20, 127-168 (2010) · Zbl 1207.03072
[4] Hyland, Martin; Blain Levy, Paul; Plotkin, Gordon; Power, John, Combining algebraic effects with continuations, Theor. Comput. Sci., 375, 1-3, 20-40 (2007) · Zbl 1111.68067
[5] Hyland, Martin; Plotkin, Gordon; Power, John, Combining effects: sum and tensor, Theor. Comput. Sci., 357, 1-3, 70-99 (2006) · Zbl 1096.68088
[6] Leroy, Xavier; Doligez, Damien; Frisch, Alain; Garrigue, Jacques; Rémy, Didier; Vouillon, Jérôme, The OCaml System (Release 3.12): Documentation and User’s Manual (2011), Institut National de Recherche en Informatique et en Automatique
[7] Blain Levy, Paul; Power, John; Thielecke, Hayo, Modelling environments in call-by-value programming languages, Inf. Comput., 185, 182-210 (September 2003)
[8] Milner, Robin, A theory of type polymorphism in programming, J. Comput. Syst. Sci., 17, 348-375 (1978) · Zbl 0388.68003
[9] Milner, Robin; Tofte, Mads; Harper, Robert; MacQueen, David, The Definition of Standard ML (1997), MIT Press
[10] Murdoch, Gabbay J.; Pitts, Andrew M., A new approach to abstract syntax with variable binding, Form. Asp. Comput., 13, 3-5, 341-363 (July 2001)
[11] Plotkin, Gordon; Power, John, Notions of computation determine monads, (5th International Conference on Foundations of Software Science and Computation Structures. 5th International Conference on Foundations of Software Science and Computation Structures, Lecture Notes in Computer Science, vol. 2303 (2002)), 342-356 · Zbl 1077.68676
[12] Plotkin, Gordon; Power, John, Algebraic operations and generic effects, Appl. Categ. Struct., 11, 1, 69-94 (2003) · Zbl 1023.18006
[13] Plotkin, Gordon; Power, John, Tensors of comodels and models for operational semantics, (Bauer, Andrej; Mislove, Michael, Proceedings of the 24th Conference on the Mathematical Foundations of Programming Semantics (MFPS XXIV). Proceedings of the 24th Conference on the Mathematical Foundations of Programming Semantics (MFPS XXIV), Electronic Notes in Theoretical Computer Science, vol. 218 (2008)), 295-311 · Zbl 1286.68303
[14] Plotkin, Gordon; Pretnar, Matija, Handlers of algebraic effects, (Castagna, Giuseppe, Programming Languages and Systems. Programming Languages and Systems, Lecture Notes in Computer Science, vol. 5502 (2009), Springer: Springer Berlin Heidelberg), 80-94 · Zbl 1234.68059
[15] Plotkin, Gordon David; Power, Anthony John, Adequacy for algebraic effects, (4th International Conference on Foundations of Software Science and Computation Structures. 4th International Conference on Foundations of Software Science and Computation Structures, Lecture Notes in Computer Science, vol. 2030 (2001)), 1-24 · Zbl 0986.68055
[16] Plotkin, Gordon David; Power, Anthony John, Logic for computational effects: work in progress, (Workshops in Computing. Workshops in Computing, 6th International Workshop on Formal Methods (2003))
[17] Plotkin, Gordon David; Pretnar, Matija, A logic for algebraic effects, (23rd Symposium on Logic in Computer Science (2008)), 118-129
[18] Power, John; Shkaravska, Olha, From comodels to coalgebras: state and arrays, (Adamek, Jiri; Milius, Stefan, Proceedings of the Workshop on Coalgebraic Methods in Computer Science (CMCS). Proceedings of the Workshop on Coalgebraic Methods in Computer Science (CMCS), Electronic Notes in Theoretical Computer Science, vol. 106 (2004)), 297-314 · Zbl 1271.18006
[19] Pretnar, Matija, The logic and handling of algebraic effects (2010), School of Informatics, University of Edinburgh, PhD thesis · Zbl 1351.68079
[20] Reynolds, John, The meaning of types—from intrinsic to extrinsic semantics (2000), Department of Computer Science, University of Aarhus, Technical report
[21] Wadler, Philip, Monads for functional programming, (Advanced Functional Programming, First International Spring School on Advanced Functional Programming Techniques-Tutorial Text (1995), Springer-Verlag: Springer-Verlag London, UK), 24-52
[22] Wright, Andrew, Simple imperative polymorphism, (LISP and Symbolic Computation (1995)), 343-356
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.