Algebraic computational effects
Effects are central to programming languages, and include side-effects, exceptions, input, output, various forms of nondeterminism, nontermination, and continuations. A general theory of effects is therefore desirable. A first was provided by Eugenio Moggi who identified monads as providing a framework for modelling computational effects. Algebraic effects, first considered by John Power and myself, form a subclass where the effects can be modelled by bounded equational theories; the monads are then the corresponding free algebra monads. These effects include all the above examples other than continuations.
The lectures begin with an account of this algebraic approach and how it fits in with Moggi's ideas; they then put the approach to work. The hope behind the algebraic approach is that many topics and applications, normally considered separately for individual effects, can instead be considered more or less uniformly for algebraic effects. As a first example, we will treat operational semantics. As a second, we will consider effect handlers: whereas the algebraic operations can be considered as producing effects, handlers can be considered as consuming them. Applications are varied, ranging from exception handlers to parallelism. The final example has yet to be determined, one possibility is effect type systems and indexed monads, following Wadler, but continuing algebraically.
- G. Plotkin. Algebraic effects. Slides from the EWSCS. 2015 course + exercises
- Lecture 1. Algebraic effects I. [pdf]
- Lecture 2. Type and effect systems. [pdf]
- Lecture 3. Algebraic effects II. [pdf]
- Lecture 4. Effect handlers. [pdf]
- Videos from the lectures.
- E. Moggi. Computational lambda-calculus and monads. In Proc. of 4th Ann. Symp. on Logic in Computer Science, LICS '89, pp. 14-23. IEEE, 1989. [doi link]
- N. Benton, J. Hughes, E. Moggi. Monads and effects. In G. Barthe, P. Dybjer, L. Pinto, J. Saraiva, eds., Advanced lectures from Int. Summer School on Applied Semantics, APPSEM 2000, v. 2395 of Lect. Notes in Comput. Sci., pp. 42-122. Springer, 2001. [doi link]
- E. Robinson. Variations on algebra: monadicity and generalisations of equational theories. Form. Asp. of Comput., v. 13, n. 3-5, pp. 308-326, 2002. [doi link]
- J. G. Riecke. Fully abstract translations between functional languages. Math. Struct. in Comput. Sci., v. 3, n. 4, pp. 387-415, 2009. [doi link]
- C. Roux. Constructive type theory. Notes, 2012. Ch. 1-3.
- L. Aceto, A. Ingólfsdottir, K. G. Larsen, J. Srba. Reactive Systems: Modelling, Specification and Verification. Cambridge Univ. Press, 2007. Ch. 1-7.
Prof. Plotkin is best known for his introduction of structural operational semantics and his work on denotational semantics. He was educated at the University of Glasgow and the University of Edinburgh, and has remained at Edinburgh, where he was a co-founder, with Rod Burstall and Robin Milner, of the Laboratory for Foundations of Computer Science. He was elected a Fellow of the Royal Society in 1992. In 2012 he received the Royal Society's Milner Award.
April 17, 2016 21:54 Europe/Helsinki (GMT +03:00)
local organizers, ewscs15(at)cs.ioc.ee
EWSCS'15 page: http://cs.ioc.ee/ewscs/2015/