Adequacy for algebraic effects
John Power – 15 April 2020
Algebraic effects were first identified by Plotto and me in a paper in FOSSACS in 2001, where we proposed a unified treatment of operational semantics for such effects. There had long been operational semantics for each of the effects: the aim was to give a unified account that recognisably related to the extant ones.One notices immediately that one must have algebraic operations, e.g., read, write, nondeterministic "or", lookup and update, in order even to write down programs with effects, and that no monad appears in any program. A few weeks after the paper was published, we realised that, if one adds computationally natural equations to the operations, the monads, which arose in types and in models rather than in programs, are redundant: continuations are not an algebraic effect. This perspective suddenly made clear how to deal with previously intractable aspects of effects. That has sparked immense development that continues to this day.For this talk, I propose to give historical context of the paper, thus outlines of PCF and structural operational semantics, then an outline of what we did and what followed. I do not plan to say much at all about recursion: the point of that part of the paper was that what we did extends to recursion, which of course is vital, and recognisably relates to extant operational semantics there. I hope to give a brief idea of how this led to our work on tensors in regard to state, cf Richard's talk last week.
Back