Programming with algebraic effects and handlers is a fairly novel technique of representing computational effects. Rooted in the theoretical work of Plotkin and Power, from which the key notion of algebraicity of the effects stems, this framework offers a more modular way of effectful programming — in particular, a modular way of composing effectful programs.

The distinction between algebraic effects and other models of effectful computation is its separation between "interface" and "implementation": algebraic operations, such as raising an exception or reading/writing a cell of mutable state are treated as mere syntax or pieces of a specification, on their own devoid of interpretation. What Plotkin and Pretnar's insight adds to this view is the notion of a handler — a construct which provides an interpretation for the operation, within its scope. In connection with expressive type-and-effect systems, these constructs allow programmers almost unprecedented freedom to define and manage their own computational effects.

In this talk I would like to discuss some of the choices that one faces while designing a calculus that allows programming with algebraic effects, and show how one of the most important aspects that one needs to pay attention to is parametricity. To this end we develop a model calculus of algebraic effects and handlers with a polymorphic type-and-effect system that allows for both universal and existential quantification over effects (thus providing a somewhat limited model for modules in a setting with algebraic effects and handlers), and a step-indexed relational interpretation of this calculus. We can then use the relational interpretation to show some interesting properties of the calculus, in particular to show contextual equivalence and refinement results.