From 85757c48fd5c92b65a99d4c437fa5bf87cab815e Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Daniel=20Hillerstr=C3=B6m?= Date: Sat, 22 May 2021 20:08:12 +0100 Subject: [PATCH] Effect handlers primer --- macros.tex | 2 + thesis.tex | 141 +++++++++++++++++++++++++++++++++++++++-------------- 2 files changed, 106 insertions(+), 37 deletions(-) diff --git a/macros.tex b/macros.tex index c1ce4c9..f2f43e8 100644 --- a/macros.tex +++ b/macros.tex @@ -140,6 +140,8 @@ \newcommand{\Cong}{\mathrm{cong}} +\newcommand{\AlgTheory}{\ensuremath{\mathcal{T}}} + %% Handler projections. \newcommand{\mret}{\mathrm{ret}} \newcommand{\mops}{\mathrm{ops}} diff --git a/thesis.tex b/thesis.tex index 2e9a5bd..881a5fc 100644 --- a/thesis.tex +++ b/thesis.tex @@ -808,7 +808,10 @@ emergence of monads as a programming abstraction began when \citet{Moggi89,Moggi91} proposed to use monads as the mathematical foundation for modelling computational effects in denotational semantics. \citeauthor{Moggi91}'s view was that \emph{monads determine - computational effects}. This view was put into practice by + computational effects}. The key property of this view is that pure +values of type $A$ are distinguished from effectful computations of +type $T~A$, where $T$ is the monad representing the effect(s) of the +computation. This view was put into practice by \citet{Wadler92,Wadler95}, who popularised monadic programming in functional programming by demonstrating how monads increase the ease at which programs may be retrofitted with computational effects. @@ -869,10 +872,17 @@ different computational effects. In the following subsections we will see three different instantiations with which we will implement global mutable state. +Monadic programming is a top-down approach to effectful programming, +where the concrete monad structure is taken as a primitive which +controls interactions between effectful operations. +% Monadic programming is a top-down approach to effectful programming, +% where we start with a concrete framework in which we can realise +% effectful operations. +% The monad laws ensure that monads have some algebraic structure, which -programmers can use when reasoning about their monadic programs, and -optimising compilers may take advantage of the structure to emit more -efficient code for monadic programs. +programmers can use when reasoning about their monadic +programs. Similarly, optimising compilers may take advantage of the +structure to emit more efficient code. The success of monads as a programming idiom is difficult to understate as monads have given rise to several popular @@ -1285,13 +1295,13 @@ operations using the state-passing technique. % \[ \bl - \runState : (\UnitType \to \Free\,(\FreeState~S)\,A) \to S \to A \times S\\ + \runState : (\UnitType \to \Free\,(\FreeState~S)\,R) \to S \to R \times S\\ \runState~m~st \defas \Case\;m\,\Unit\;\{ \ba[t]{@{}l@{~}c@{~}l} \return~x &\mapsto& (x, st);\\ - \OpF\,(\Get~k) &\mapsto& \runState~st~(\lambda\Unit.k~st);\\ - \OpF\,(\Put\,\Record{st';k}) &\mapsto& \runState~st'~k + \OpF\,(\Get~k) &\mapsto& \runState\,(\lambda\Unit.k~st)~st;\\ + \OpF\,(\Put\,\Record{st';k}) &\mapsto& \runState~k~st' \}\ea \el \] @@ -1311,8 +1321,8 @@ that this interpretation of get and put satisfies the equations of Definition~\ref{def:state-monad}. % -By instantiating $S = \Int$ we can use this interpreter to run -$\incrEven$. +By instantiating $S = \Int$ and $R = \Bool$ we can use this +interpreter to run $\incrEven$. % \[ \runState~\incrEven~4 \reducesto^+ \Record{\True;5} : \Bool \times \Int @@ -1426,43 +1436,96 @@ $R = \Bool$ and $S = \Int$. \subsubsection{Handling state} % At the start of the 00s decade -\citet{PlotkinP01,PlotkinP02,PlotkinP03} introduced \emph{algebraic - effects}, which is an approach to effectful programming that inverts -\citeauthor{Moggi91}'s view such that \emph{computational effects - determine monads}. In their view a computational effect is given by -a signature of effectful operations and a collection of equations that -govern their behaviour, together they generate a free monad rather -than the other way around. +\citet{PlotkinP01,PlotkinP02,PlotkinP03} introduced algebraic theories +of computational effects, or simply \emph{algebraic effects}, which +inverts \citeauthor{Moggi91}'s view of effects such that +\emph{computational effects determine monads}. In their view a +computational effect is described by an algebraic effect, which +consists of a signature of abstract operations and a collection of +equations that govern their behaviour, together they generate a free +monad rather than the other way around. +% +Algebraic effects provide a bottom-up approach to effectful +programming in which abstract effect operations are taken as +primitive. Using these operations we may build up concrete structures. % In practical programming terms, we may understand an algebraic effect as an abstract interface, whose operations build the underlying free monad. - -By the end of the decade \citet{PlotkinP09,PlotkinP13} introduced -\emph{handlers for algebraic effects}, which interpret computation -trees induced by effectful operations in a similar way to runners of -free monad interpret computation trees. A crucial difference between -handlers and runners is that the handlers are based on first-class -delimited control. % -Practical programming with algebraic effects and their handlers was -popularised by \citet{KammarLO13}, who demonstrated that algebraic -effects and handlers provide a modular basis for effectful -programming. - -%\dhil{Cite \citet{PlotkinP01,PlotkinP02,PlotkinP03,PlotkinP09,PlotkinP13}.} +\begin{definition} + % A \emph{signature} $\Sigma$ is a collection of operation symbols + % $\ell : A \opto B \in \Sigma$. An operation symbol is a syntactic entity. + An algebraic effect is given by a pair + $\AlgTheory = (\Sigma,\mathsf{E})$ consisting of an effect signature + $\Sigma = \{(\ell_i : A \opto B)_i\}_i$ of typed operation symbols + $\ell_i$, whose interactions are govern by set of equations + $\mathsf{E}$. + % + We will not concern ourselves with the mathematical definition of + equation, as in this dissertation we will always fix + $\mathsf{E} = \emptyset$, meaning that the interactive patterns of + operations are unrestricted. As a consequence we will regard an + operation symbol as a syntactic entity subject only to a static + semantics. The type $A \opto B$ denotes the space of operations + whose payload has type $A$ and whose interpretation yields a value + of type $B$. +\end{definition} % -From a programming perspective effect handlers are an operational -extension of \citet{BentonK01} style exception handlers. +As with the free monad, the meaning of an algebraic effect operation +is conferred by some separate interpreter. In the algebraic theory of +computational effects such interpreters are known as handlers for +algebraic effects, or simply \emph{effect handlers}. They were +introduced by \citet{PlotkinP09,PlotkinP13} by the end of the decade. +% +A crucial difference between effect handlers and interpreters of free +monads is that effect handlers use delimited control to realise the +behaviour of computational effects. +% The meaning of an algebraic effect is conferred by a suitable effect +% handler, or in analogy with the free monad a suitable interpreter. Effect handlers were By +% the end of the decade \citet{PlotkinP09,PlotkinP13} introduced +% \emph{handlers for algebraic effects}, which interpret computation +% trees induced by effectful operations in a similar way to runners of +% free monad interpret computation trees. A crucial difference between +% handlers and runners is that the handlers are based on first-class +% delimited control. +% +Practical programming with effect handlers was popularised by +\citet{KammarLO13}, who advocated algebraic effects and their handlers +as a modular basis for effectful programming. + +Effect handlers introduce two dual control constructs. % \[ \ba{@{~}l@{~}r} - \Do\;\ell^{A \opto B}~M^C : B & \Handle\;M^A\;\With\;H^{A \Harrow B} : B \smallskip\\ - \multicolumn{2}{c}{H^{C \Harrow D} ::= \{\Return\;x^C \mapsto M^D\} \mid \{\OpCase{\ell^{A \opto B}}{p^A}{k^{B \to D}} \mapsto M^D\} \uplus H} + \Do\;\ell^{A \opto B}~V^A : B & \Handle\;M^C\;\With\;H^{C \Harrow D} : D \smallskip\\ + \multicolumn{2}{c}{H ::= \{\Return\;x^C \mapsto N^D\} \mid \{\OpCase{\ell^{A \opto B}}{p^A}{k^{B \to D}} \mapsto N^D\} \uplus H^{C \Harrow D}} \ea \] -The operation symbols are declared in a signature -$\ell : A \opto B \in \Sigma$. +% +The $\Do$ construct reifies the control state up to a suitable handler +and packages it up with the operation symbol $\ell$ and its payload +$V$ before transferring control to the suitable handler. As control is +transferred a hole is left in the evaluation context that must be +filled before evaluation can continue. The $\Handle$ construct +delimits $\Do$ invocations within the computation $M$ according to the +handler definition $H$. Handler definitions consist of the union of a +single $\Return$-clause and the disjoint union of zero or more +operation clauses. The $\Return$-clause specifies what to do with the +return value of a computation. An operation clause +$\OpCase{\ell}{p}{k}$ matches on an operation symbol and binds its +payload to $p$ and its continuation $k$. Note that the domain type of +the continuation agrees with the codomain type of the operation +symbol, and the codomain type of the continuation agrees with the +codomain type of the handler definition. Continuation application +fills the hole left by the $\Do$ construct, thus providing a value +interpretation of the invocation. The continuation returns inside the +handler once the $\Return$-clause computation has finished. +% +Operationally, effect handlers may be regarded as an extension of +\citet{BentonK01} style exception handlers. + +We can implement mutable state with effect handlers as follows. % \[ \ba{@{~}l@{\qquad\quad}@{~}r} @@ -1509,12 +1572,16 @@ interpreter is that here the continuation $k$ implicitly reinstalls the handler, whereas in the free state monad interpreter we explicitly reinstalled the handler via a recursive application. % -By fixing $S = \Int$ we can use the above effect handler to run the -delimited control variant of $\incrEven$. +By fixing $S = \Int$ and $A = \Bool$ we can use the above effect +handler to run the delimited control variant of $\incrEven$. % \[ \runState~\incrEven~4 \reducesto^+ \Record{\True;5} : \Bool \times \Int \] +% +Effect handlers come into their own when multiple effects are +combined. Throughout the dissertation we will see multiple examples of +handlers in action (e.g. Chapter~\ref{ch:unary-handlers}). \subsubsection{Effect tracking} \dhil{Cite \citet{GiffordL86}, \citet{LucassenG88}, \citet{TalpinJ92},