Abstract
The sixth lecture presented the theoretical foundations underlying the effect and effect management mechanisms introduced in the previous lecture. We started with monads, a concept derived from category theory and applied to denotational semantics by Moggi in 1989. They provide an elegant framework for describing many kinds of effects, from mutable states to control operators and non-determinism. The monadic transformation, which generalizes the CPS transformation of the4th lecture, makes it possible to translate any program with monadic effects into a pure functional program. We have studied free monads and their underlying data structure, interaction trees, which allow a monadic program to be executed while leaving the effects uninterpreted ; the semantics of the effects being provided later by a " fold " type traversal of the interaction tree. The theory of algebraic effects, developed by Plotkin, Power, Pretnar and co-authors in the years 2000, goes two notches further : firstly, by specifying the semantics of effects through equations, just as an algebraic structure is characterized by equations involving its operations ; secondly, by realizing this semantics through a composition of effect handlers, each handler being an interaction tree transformer that implements certain effects and leaves others unchanged. Finally, following the approach initiated by Bauer and Pretnar in 2012, we observed that these handlers can be defined within a programming language that includes effect handling as a new control structure.
