Defining algebraic effect handlers
This post is an incomplete digest of Andrej Bauer’s What is algebraic about algebraic effects and handlers?, which is a note of a tutorial given at a Dagstuhl seminar. My goal is to arrive at a reasonable definition of handlers. (Spoiler: I don’t manage to achieve that goal, although we will see Bauer’s definition.) The technical part of this post will be somewhat compact and lightweight, so that it’s easier for me to come back and take a quick look; for a fuller introduction, Bauer’s note itself is very accessible and highly recommended, and in particular gives a lot of examples.
An algebraic theory prescribes a set of operations and their equational laws saying that applying the operations in two different ways should lead to the same result. For example, the theory of monoids is about two operations, say $0$ and $(+)$, satisfying the usual identity and associativity laws, where for example the left identity law $0 + x = x$ says that applying $(+)$ to $0$ and any element $x$ is the same as just $x$. Such applications of operations can be represented as trees whose leaves are variables and whose internal nodes are operations, or in Haskell syntax,
\begin{eqnarray*} \mathbf{data}\ \mathsf{MTree}\ v &=& \mathsf{Return}\ v \\ &|& \mathsf{Zero} \\ &|& \mathsf{Plus}\ (\mathsf{MTree}\ v)\ (\mathsf{MTree}\ v) \end{eqnarray*}
where the type of the trees is parametrised over the type of variables used. Application of operations is reminiscent of programs/syntax trees, and we can choose a suitable design of trees so as to formulate theories about more familiar programs. For example, stateful programs can be thought of as having two operations $\mathsf{get}$ and $\mathsf{put}$ operating on an implicit state of type $S$, with $\mathsf{get}$ reading the state and $\mathsf{put}$ overwriting the state. To represent stateful programs as trees, we need two generalisations (compared to the monoidal trees): We can think of $\mathsf{get}$ as a node having a potentially infinite number of branches indexed by all the possible states, where each branch is the continuation to be executed upon getting a particular state. As for $\mathsf{put}$, apart from a continuation, we should add to the node an extra field storing the value to be written to the state. So the trees representing stateful programs may be infinitely branching and have internal fields, or more precisely in Haskell syntax,
\begin{eqnarray*} \mathbf{data}\ \mathsf{STree}\ v &=& \mathsf{Return}\ v \\ &|& \mathsf{Get}\ (S \to \mathsf{STree}\ v) \\ &|& \mathsf{Put}\ S\ (\mathsf{STree}\ v) \end{eqnarray*}
We can then formulate laws on stateful programs, for example requiring that getting the state and then immediately putting it back is the same as doing nothing: Get (\s -> Put s cont) should be ‘the same’ as just cont.
The above account mixes syntax/signature and semantics/model, whereas modern logic suggests that we separate the two. Starting with the former: The signature/syntax of an algebraic theory $T$ is specified by a collection of operation symbols, where each symbol $\mathit{op}$ is associated with a parameter set $P$ and an arity set $A$, written $\mathit{op} : P \leadsto A$, and a set of purely formal equations between two trees/terms inductively constructed from some set of variables and the operation symbols. In (casual) Haskell syntax, the trees are defined by
\begin{eqnarray*} \mathbf{data}\ \mathsf{Tree}_T\ v &=& \mathsf{Return}\ v \\ &|& \ldots \\ &|& \mathit{op}\ P\ (A \to \mathsf{Tree}_T\ v) \\ &|& \ldots \end{eqnarray*}
Note that this formulation is general enough to represent both the monoidal and stateful trees: $0 : \mathbf 1 \leadsto \mathbf 0$, $(+) : \mathbf 1 \leadsto \mathbf 2$, $\mathsf{get} : \mathbf 1 \leadsto S$, and $\mathsf{put} : S \leadsto \mathbf 1$, where $\mathbf n \defeq \set{0, \ldots, n-1}$.
Semantically, define a model $M$ of $T$ to be a carrier set $|M|$ and a collection of functions corresponding to every operation symbol $\mathit{op} : P \leadsto A$ in $T$
$$ \sem{\mathit{op}} : P \to (A \to |M|) \to |M| $$
on which the equations of $T$ should be valid: defining (casually)
\begin{eqnarray*} \mathsf{eval} &:& (v \to |M|) \to \mathsf{Tree}_T\ v \to |M| \\ \mathsf{eval}\ \sigma\ (\mathsf{Return}\ v) &=& \sigma\ v \\ \mathsf{eval}\ \sigma\ (\mathit{op}\ p\ \mathit{ts}) &=& \sem{\mathit{op}}\ p\ (\mathsf{eval}\ \sigma \circ \mathit{ts}) \end{eqnarray*}
we require $\mathsf{eval}\ \sigma\ t = \mathsf{eval}\ \sigma\ u$ for every formal equation $t = u$ in $T$ and assignment $\sigma$.
The intuition about theories being programs/syntax trees and their equations is formalised as a term model $\mathsf F_T\ X$ over some (result) type $X$, which contains programs/syntax trees identified up to the equations.
In more detail:
The carrier set $|\mathsf F_T\ X|$ is $\mathsf{Tree}_T\ X\mathop/{(\sim)}$ where $(\sim)$ is the congruent equivalence relation on $\mathsf{Tree}_T\ X$ inductively generated from the (semantic) equations
$\mathsf{eval}\ \sigma\ t = \mathsf{eval}\ \sigma\ u$ for every (formal) equation $t = u$ in $T$ and assignment $\sigma$.
The semantics of the operations of $T$ are just the constructors of $\mathsf{Tree}_T\ X$ operating on the representatives of the equivalence classes; they’re well-defined (on the quotient set) because $(\sim)$ is congruent, and they validate all the formal equations of $T$ because $(\sim)$ includes exactly those equations.
This doesn’t seem to say much, but we may be able to deduce something stronger from the quotient construction: for the theory of state, for example, it can be shown that all the elements in the term model have the normal form Get (\s -> Put (f s) (Return (g s))) for some f : S -> S and g : S -> X, and are isomorphic to the state transformers of type S -> X × S.
The term model is special because it is free, in the sense that it can be mapped to any other model of $T$ in a unique, structure-preserving way, and can thus be thought of as a representation capturing the common structure of all the models. This isn’t surprising though if we recall that the common structure in question is $T$, or more precisely, the equations about applications of operations specified by $T$, which are exactly what the term model represents. Formally, for every model $M$ of $T$ and function $f : X \to |M|$, there exists a unique homomorphism $h : \mathsf F_T\ X \to M$ such that $f = h \circ \mathsf{Return}$, and this $h$ is in fact $\mathsf{eval}\ f$ with its domain quotiented. An important consequence of this definition is that all the homomorphisms of type $\mathsf F_T\ X \to M$ are in one-to-one correspondence with the mappings of type $X \to |M|$. (One way to verify this directly is to check that $\mathsf{eval}$ is both injective and surjective.)
Remark. The choice of making the term model parametrised over $X$ may seem somewhat arbitrary, but it is ‘predicted’ by the general theory of adjunctions in category theory, and thus justified by the prevalence and usefulness (and even ‘inevitability’) of adjunctions. (End of Remark.)
Discussion. In Section 2.1 ‘Computations as free models’ of Bauer’s note, he says
Among all the models of an algebraic theory of computational effects, which one best describe[s] the actual computational effects? If a theory of computational effects truly is adequately described by its signature and equations, then the free model ought to be the desired one.
I was confused by this seemly under-justified identification of computation and the free model — the former is a very rich and diverse concept whereas the latter is just programs and equations, so there seems to be a fairly big gap. But after re-reading Bauer’s words more carefully, I see that his every mention of computation should be qualified by ‘algebraic’, that is, he only talks about computations whose behaviour can be characterised by equations (such as state), and then everything makes sense. This does greatly reduce the strength of his statement though, to the extent that the statement becomes almost tautological. Moreover, I am still concerned about the gap — that is, I am doubtful about how many computational effects are algebraic, in the sense that we can truly understand the effects just through equations. It’s great to be able to give effects an algebraic structure so that we can perform equational reasoning about them, but it probably goes too far (or is still too early) to say that to understand the behaviour of effectful programs all it takes is to understand the equations, except in simple and well-studied cases like state. (End of discussion.)
Bauer then defines handlers as transformations of computations from one theory to another, i.e., of type $\mathsf F_T\ X \to \mathsf F_{T'}\ X'$. My intuition here is that $T$ consists of high-level operations (and $X$ is some abstract type) whereas the operations of $T'$ are low-level micro-instructions (and $X'$ is some primitive type), and a handler’s job is to implement the high-level operations in terms of the low-level micro-instructions. With a leap of faith Bauer postulates that handlers should be homomorphisms on models of $T$. This means that $\mathsf F_{T'}\ X'$ should be a model of $T$ in the first place, that is, for each $\mathit{op} : P \leadsto A$ in $T$ we should give an interpretation
$$ \sem{\mathit{op}} : P \to (A \to |\mathsf F_{T'}\ X'|) \to |\mathsf F_{T'}\ X'| $$
and show that the equations of $T$ hold for these interpretations (using the equations of $T'$). These amount to translating each high-level operation to low-level micro-instructions (assuming that the micro-instructions corresponding to its operands are known) and proving that the laws of the low-level micro-instructions imply those of the high-level operations. Then all it takes to define a homomorphism from $\mathsf F_T\ X$ to $\mathsf F_{T'}\ X'$ is to give a function of type
$$ X \to |\mathsf F_{T'}\ X'| $$
which is used to handle the $\mathsf{Return}$ nodes. In short, Bauer ‘predicts’ handlers to be folds on (equivalence classes of) the trees of type $\mathsf F_T\ X$ based on the ubiquity of homomorphisms, but I find this prediction less acceptable (‘inevitable’) than the one about free models. Besides, the result type of Bauer’s handlers is not what we usually see — for state, for example, the type of the usual handler is something like
$$ \mathsf F_T\ X \to S \to \mathsf F_{T'}\ (X' \times S) $$
where $T$ has the two stateful operations and $T'$ is $T$ without the two operations. We could again require that this should be a homomorphism, and repeat the reasoning above to arrive at a suitable definition, but I still don’t see a way to justify the requirement — indeed, Bauer noted at the end of the note that ‘in practice we often want handlers that break the equations’. Oh well.
