Effect handlers.

macros.tex

@@ -326,6 +326,10 @@
 \newcommand{\Option}{\dec{Option}}
 \newcommand{\Some}{\dec{Some}}
 \newcommand{\None}{\dec{None}}
+\newcommand{\Toss}{\dec{Toss}}
+\newcommand{\toss}{\dec{toss}}
+\newcommand{\Heads}{\dec{Heads}}
+\newcommand{\Tails}{\dec{Tails}}
 \newcommand{\Exn}{\dec{Exn}}
 \newcommand{\fail}{\dec{fail}}
 \newcommand{\optionalise}{\dec{optionalise}}

thesis.tex

@@ -865,124 +865,30 @@ just as a delimited abortive continuation is conceivable.
 A composable continuation is also known as a `functional' continuation
 in the literature.
 
-% % \citeauthor{Reynolds93} has written a historical account of the
-% % various early discoveries of continuations~\cite{Reynolds93}.
-
-% In the literature the term ``continuation'' is often accompanied by a
-% qualifier such as full~\cite{JohnsonD88}, partial~\cite{JohnsonD88},
-% abortive, escape, undelimited, delimited, composable, or functional.
-% %
-% Some of these qualifiers are synonyms, and hence redundant, e.g. the
-% terms ``full'' and ``undelimited'' refer to the same notion of
-% continuation, likewise the terms ``partial'' and ``delimited'' mean
-% the same thing, the notions of ``abortive'' and ``escape'' are
-% interchangeable too, and ``composable'' and ``functional'' also refer
-% to the same notion.
-% %
-
-% Thus the peloton of distinct continuation notions can be pruned to
-% ``undelimited'', ``delimited'', ``abortive'', and ``composable''.
-% %
-% The first two notions concern the introduction of continuations, that
-% is how continuations are captured. Dually, the latter two notions
-% concern the elimination of continuations, that is how continuations
-% interact with the enclosing context.
-% %
-% Consequently, it is not meaningful to contrast, say, ``undelimited''
-% with ``abortive'' continuations, because they are orthogonal notions.
-% %
-% A common confusion in the literature is to conflate ``undelimited''
-% continuations with ``abortive'' continuations.
-% % Similarly, often times ``composable'' is taken to imply ``delimited''.
-% However, it is perfectly possible to conceive of a continuation that
-% is undelimited but not abortive.
-% %
-% % An educated guess as to why this confusion occurs in the literature
-% % may be that it is due to the introduction
-
-% To make each notion of continuation concrete I will present its
-% characteristic reduction rule. To facilitate this presentation I will
-% make use of an abstract control operator $\CC$ to perform an abstract
-% capture of continuations, i.e. informally $C\,k.M$ is to be understood
-% as a syntactic construct that captures the continuation and reifies it
-% as a function which it binds to $k$ in the computation $M$. The
-% precise extent of the capture will be given by the characteristic
-% reduction rule. I will also make use of an abstract control delimiter
-% $\Delim{-}$. The term $\Delim{M}$ encloses the computation $M$ in a
-% syntactically identifiable marker. For the intent and purposes of this
-% presentation enclosing a value in a delimiter is an idempotent
-% operation, i.e.  $\Delim{V} \reducesto V$. I will write $\EC$ to
-% denote an evaluation context~\cite{Felleisen87}.
-
-% \paragraph{Undelimited continuation}
-% %
-% \[
-%   \EC[\CC\,k.M] \reducesto \EC[M[(\lambda x.\EC[x])/k]]
-% \]
-% %
-% \begin{derivation}
-%   & 3 * (\CC\,k. 2 + k\,(k\,1))\\
-%   \reducesto& \reason{captures the context $k = 3 * [~]$}\\
-%   & 3 * (2 + k\,(k~1))[(\lambda x. 3 * x)/k]\\
-%   =& \reason{substitution}\\
-%   & 3 * (2 + (\lambda x. 3 * x)((\lambda x. 3 * x)\,1))\\
-%   \reducesto& \reason{$\beta$-reduction}\\
-%   & 3 * (2 + (\lambda x. 3 * x)(3 * 1))\\
-%   \reducesto& \reason{$\beta$-reduction}\\
-%   & 3 * (2 + (\lambda x. 3 * x)\,3)\\
-%   \reducesto^4& \reason{$\beta$-reductions}\\
-%   & 33
-% \end{derivation}
-
-% \paragraph{Delimited continuation}
-% %
-% \[
-%   \Delim{\EC[\CC\,k.M]} \reducesto \Delim{M[(\lambda x.\Delim{\EC[x]})/k]}
-% \]
-% %
-% \[
-%   \Delim{\EC[\CC\,k.M]} \reducesto M[(\lambda x.\Delim{\EC[x]})/k]
-% \]
-
-% \paragraph{Abortive continuation} An abortive continuation discards the current context.Like delimited continuations, an
-% abortive continuation is accompanied by a delimiter. The
-% characteristic property of an abortive continuation is that it
-% discards its invocation context up to its enclosing delimiter.
-% %
-% \[
-%   \EC[k\,V] \reducesto V, \quad \text{where } k = (\lambda x. \keyw{abort}\;x).
-% \]
-% %
-% Consequently, composing an abortive continuation with itself is
-% meaningless, e.g. in $k (k\,V)$ the innermost application erases the
-% outermost application.
-
-% \paragraph{Composable continuation} The defining characteristic of a
-% composable continuation is that it composes the captured context with
-% current context, i.e.
-% %
-% \[
-%   \EC[k\,V] \reducesto \EC[\EC'[V]], \quad \text{where } k = (\lambda x. \EC'[x])
-% \]
-
-% Escape continuations, undelimited continuations, delimited
-% continuations, composable continuations.
-
-% Downward and upward use of continuations.
-
 \section{Controlling continuations}
 \label{sec:controlling-continuations}
 As suggested in the previous section, the design space for
 continuation is rich. This richness is to an extent reflected by the
-considerable amount of control operators that appear in the literature
+large amount of control operators that appear in the literature
 and in practice.
 %
+The purpose of this section is to survey a considerable subset of the
+first-class \emph{sequential} control operators that occur in the
+literature and in practice. Control operators for parallel programming
+will not be considered here.
+%
 Table~\ref{tbl:classify-ctrl} provides a classification of a
 non-exhaustive list of first-class control operators.
 
-It is worth remarking that a \emph{first-class} control operator is
-typically not itself a first-class citizen, rather, it means that the
-reified continuation is a first-class citizen.
+Note that a \emph{first-class} control operator is typically not
+itself a first-class citizen, rather, the label `first-class' means
+that the reified continuation is a first-class object. Control
+operators that reify the current continuation can be made first-class
+by enclosing them in a $\lambda$-abstraction. Obviously, this trick
+does not work for operators that reify the caller continuation.
+
+To study the control operators we will make use of a small base
+language.
 %
 \begin{table}
   \centering
@@ -1028,7 +934,7 @@ reified continuation is a first-class citizen.
 
 \paragraph{A small calculus for control}
 %
-To look at control we will a simply typed fine-grain call-by-value
+To look at control we will use a simply typed fine-grain call-by-value
 calculus. Although, we will sometimes have to discard the types, as
 many of the control operators were invented and studied in a untyped
 setting. The calculus is essentially the same as the one used in
@@ -1063,6 +969,17 @@ primitive $\Continue$.
     {\typ{\Gamma}{V : A} \\ \typ{\Gamma}{W : \Cont\,\Record{A;B}}}
     {\typ{\Gamma}{\Continue~W~V : B}}
 \end{mathpar}
+%
+Although, it is convenient to treat continuation application specially
+for operational inspection, it is rather cumbersome to do so when
+studying encodings of control operators. Therefore, to obtain the best
+of both worlds, the control operators will reify their continuations
+as first-class functions, whose body is $\Continue$-expression. To
+save some ink, we will use the following notation.
+%
+\[
+  \qq{\cont_{\EC}} \defas \lambda x. \Continue~\cont_{\EC}~x
+\]
 
 \subsection{Undelimited control operators}
 %
@@ -1432,9 +1349,13 @@ continuation with the then-current continuation.
 $\FelleisenC$.
 %
 \[
-  \sembr{\FelleisenC} \defas \lambda m.\FelleisenF\,(\lambda k. m\,(\lambda v.\FelleisenF\,(\lambda\_.\Continue~k~v)))
+  \sembr{\FelleisenC} \defas \lambda m.\FelleisenF\,(\lambda k. m\,(\lambda v.\FelleisenF\,(\lambda\_.k~v)))
 \]
 %
+The first application of $\FelleisenF$ has the effect of aborting the
+current continuation, whilst the second application of $\FelleisenF$
+aborts the invocation context.
+
 \citet{FelleisenFDM87} also postulate that $\FelleisenC$ cannot express $\FelleisenF$.
 
 \paragraph{\citeauthor{Landin98}'s J operator}
@@ -1559,11 +1480,16 @@ translate $\J$ to a language with $\JI$ as follows.
   \sembr{\J} \defas (\lambda k.\lambda f.\lambda x.\Continue\;k\,(f\,x))\,(\JI)
 \]
 %
-Strictly speaking in our setting this encoding is not faithful,
-because we do not treat continuations as first-class functions,
-meaning the types are not going to match up. An application of the
-left hand side returns a continuation object, whereas an application
-of the right hand side returns a continuation function.
+The term $\JI$ captures the caller continuation, which gets bound to
+$k$. The shape of the residual term is as expected: when $\sembr{\J}$
+is applied to a function, it returns another function, which when
+applied ultimately invokes the captured continuation.
+%
+% Strictly speaking in our setting this encoding is not faithful,
+% because we do not treat continuations as first-class functions,
+% meaning the types are not going to match up. An application of the
+% left hand side returns a continuation object, whereas an application
+% of the right hand side returns a continuation function.
 
 Let us end by remarking that the J operator is expressive enough to
 encode a familiar control operator like $\Callcc$~\cite{Thielecke98}.
@@ -1576,11 +1502,16 @@ encode a familiar control operator like $\Callcc$~\cite{Thielecke98}.
 syntactically embedded using callcc.
 %
 \[
-  \sembr{\lambda x.M} \defas \lambda x.\Callcc\,(\lambda k.\sembr{M}[\J \mapsto \lambda f.\lambda y. \Continue~k~(f\,y)])
+  \sembr{\lambda x.M} \defas \lambda x.\Callcc\,(\lambda k.\sembr{M}[\J \mapsto \lambda f.\lambda y. k~(f\,y)])
 \]
-% %
-\dhil{I am sort of torn between whether to treat continuations as
-  first-class functions\dots}
+%
+The key point here is that $\lambda$-abstractions are not translated
+homomorphically. The occurrence of $\Callcc$ immediately under the
+binder reifies the current continuation of the function, which is the
+precisely the caller continuation in the body $M$. In $M$ the symbol
+$\J$ is substituted with a function that simulates $\J$ by
+post-composing the captured continuation with the function argument
+provided to $\J$.
 
 \subsection{Delimited control operators}
 %
@@ -1726,6 +1657,10 @@ The prompt remains in place after the reification, and thus any
 subsequent application of $\Control$ will be delimited by the same
 prompt.
 %
+Presenting $\Control$ as a binding form may conceal the fact that it
+is same as $\FelleisenF$. However, the presentation here is close to
+\citeauthor{SitaramF90}'s presentation, which in turn is close to
+actual implementations of $\Control$.
 
 The static semantics of control and prompt were absent in
 \citeauthor{Felleisen88}'s original treatment.
@@ -1801,40 +1736,62 @@ To illustrate $\Prompt$ and $\Control$ in action, let us consider a
 few simple examples.
 %
 \begin{derivation}
-  & 1 + \Prompt~2 + (\Control~k.\Continue~k~(\Continue~k~0))\\
-  \reducesto^+& \reason{Capture $\EC = 2 + [\,]$}\\
-  & 1 + \Prompt~\Continue~\cont_{\EC}~(\Continue~\cont_{\EC]}~0))\,\\
+  & 1 + \Prompt~2 + (\Control~k.3 + k~0) + (\Control~k'.k'~4)\\
+  \reducesto^+& \reason{Capture $\EC = 2 + [\,] + (\Control~k'.k'~4)$}\\
+  & 1 + \Prompt~3+\Continue~\cont_{\EC}~0\\
   \reducesto & \reason{Resume with 0}\\
-  & 1 + \Prompt~\Continue~\cont_{\EC}~(2 + 0)\\
-  \reducesto^+ & \reason{Resume with 2}\\
-  & 1 + \Prompt~2 + 2\\
+  & 1 + \Prompt~3 + (2 + 0) + (\Control~k'.k'~4)\\
+  \reducesto^+ & \reason{Capture $\EC' = 5 + [\,]$}\\
+  & 1 + \Prompt~\Continue~\cont_{\EC'}~4\\
+  \reducesto^+ & \reason{Resume with 4}\\
+  & 1 + \Prompt~5 + 4\\
   \reducesto^+ & \reason{\slab{Value} rule}\\
-  & 1 + 4 \reducesto 5
+  & 1 + 9 \reducesto 10
 \end{derivation}
 %
-The continuation captured by the application of $\Control$ is
+The continuation captured by the either application of $\Control$ is
 oblivious to the continuation $1 + [\,]$ of $\Prompt$. Since the
 captured continuation is composable it returns to its call site. The
-first invocation of the continuation $k$ returns the value 2, which is
-provided as the argument to the second invocation of $k$, resulting in
-the value $4$. The prompt $\Prompt$ gets eliminated when the
-computation constituent of $\Prompt$ has been reduced to the value
-$4$, which is (implicitly) supplied to the continuation of $\Prompt$.
+invocation of the captured continuation $k$ returns the value 0, but
+splices the captured context into the context $3 + [\,]$. The second
+application of $\Control$ captures the new context up to the
+delimiter. The continuation is immediately applied to the value 4,
+which causes the captured context to be reinstated with the value 4
+plugged in. Ultimately the delimited context reduces to the value $9$,
+after which the prompt $\Prompt$ gets eliminated, and the continuation
+of the $\Prompt$ is applied to the value $9$, resulting in the final
+result $10$.
 
 Let us consider a slight variation of the previous example.
 %
 \begin{derivation}
-  & 1 + \Prompt~2 + (\Control~k.\Continue~k~0) + (\Control~k'. 0)\\
-  \reducesto^+& \reason{Capture $\EC = 2 + [\,] + (\Control~k'.0)$}\\
-  & 1 + \Prompt~\Continue~\cont_{\EC}~0\\
+  & 1 + \Prompt~2 + (\Control~k.3 + k~0) + (\Control~k'.4)\\
+  \reducesto^+& \reason{Capture $\EC = 2 + [\,] + (\Control~k'.4)$}\\
+  & 1 + \Prompt~3+\Continue~\cont_{\EC}~0\\
   \reducesto & \reason{Resume with 0}\\
-  & 1 + \Prompt~2 + 0 + (\Control~k'. 0)\\
-  \reducesto^+ & \reason{Capture $\EC' = 2 + [\,]$}\\
-  & 1 + \Prompt~0 \\
-  \reducesto & \reason{\slab{Value} rule}\\
-  & 1 + 0 \reducesto 1
+  & 1 + \Prompt~3 + (2 + 0) + (\Control~k'.4)\\
+  \reducesto^+ & \reason{Capture $\EC' = 5 + [\,]$}\\
+  & 1 + \Prompt~4\\
+  \reducesto^+ & \reason{\slab{Value} rule}\\
+  & 1 + 4 \reducesto 5
 \end{derivation}
 %
+Here the computation constituent of the second application of
+$\Control$ drops the captured continuation, which has the effect of
+erasing the previous computation, ultimately resulting in the value
+$5$ rather than $10$.
+% \begin{derivation}
+%   & 1 + \Prompt~2 + (\Control~k.\Continue~k~0) + (\Control~k'. 0)\\
+%   \reducesto^+& \reason{Capture $\EC = 2 + [\,] + (\Control~k'.0)$}\\
+%   & 1 + \Prompt~\Continue~\cont_{\EC}~0\\
+%   \reducesto & \reason{Resume with 0}\\
+%   & 1 + \Prompt~2 + 0 + (\Control~k'. 0)\\
+%   \reducesto^+ & \reason{Capture $\EC' = 2 + [\,]$}\\
+%   & 1 + \Prompt~0 \\
+%   \reducesto & \reason{\slab{Value} rule}\\
+%   & 1 + 0 \reducesto 1
+% \end{derivation}
+%
 The continuation captured by the first application of $\Control$
 contains another application of $\Control$. The application of the
 continuation immediate reinstates the captured context filling the
@@ -1843,7 +1800,7 @@ second application of $\Control$ captures the remainder of the
 computation of to $\Prompt$. However, the captured context gets
 discarded, because the continuation $k'$ is never invoked.
 %
-\dhil{Multi-prompts: more liberal typing, no interference}
+\dhil{Mention control0/prompt0 and the control hierarchy}
 
 \paragraph{\citeauthor{DanvyF90}'s shift and reset} Shift and reset
 first appeared in a technical report by \citeauthor{DanvyF89} in
@@ -1936,21 +1893,21 @@ perspective, let us revisit the second control/prompt example with
 shift/reset instead.
 %
 \begin{derivation}
-  & 1 + \reset{2 + (\shift\;k.3 + k\,0) + (\shift\;k'.0)}\\
-  \reducesto^+& \reason{Capture $\EC = 2 + [\,] + (\shift\;k.0)$}\\
+  & 1 + \reset{2 + (\shift\;k.3 + k\,0) + (\shift\;k'.4)}\\
+  \reducesto^+& \reason{Capture $\EC = 2 + [\,] + (\shift\;k.4)$}\\
   & 1 + \reset{\Continue~\cont_{\EC}~0}\\
   \reducesto & \reason{Resume with 0}\\
-  & 1 + \reset{3 + \reset{2 + 0 + (\shift\;k'. 0)}}\\
+  & 1 + \reset{3 + \reset{2 + 0 + (\shift\;k'. 4)}}\\
   \reducesto^+ & \reason{Capture $\EC' = 2 + [\,]$}\\
-  & 1 + \reset{3 + \reset{0}} \\
+  & 1 + \reset{3 + \reset{4}} \\
   \reducesto^+ & \reason{\slab{Value} rule}\\
-  & 1 + \reset{3} \reducesto^+ 4 \\
+  & 1 + \reset{7} \reducesto^+ 8 \\
 \end{derivation}
 %
-Contrast this result with the result $1$ obtained when using
+Contrast this result with the result $5$ obtained when using
 control/prompt. In essence the insertion of a new reset after
 resumption has the effect of remembering the local context of the
-first continuation invocation.
+previous continuation invocation.
 
 This difference naturally raises the question whether shift/reset and
 control/prompt are interdefinable or exhibit essential expressivity
@@ -2265,8 +2222,14 @@ Effect handler definitions occupy their own syntactic category.
                         \mid \{ \OpCase{\ell}{p}{k} \mapsto N \} \uplus H\\
 \end{syntax}
 %
-A handler consists of a $\Return$-clause and zero or more operation
-clauses.
+An effect handler consists of a $\Return$-clause and zero or more
+operation clauses. Each operation clause binds the payload of the
+matching operation $\ell$ to $p$ and the continuation of the operation
+invocation to $k$ in $N$.
+
+Effect handlers introduces a new syntactic category of signatures, and
+extends the value types with operation types. Operation and handler
+application both appear as computation forms.
 %
 \begin{syntax}
   &\Sigma \in \mathsf{Sig} &::=& \emptyset \mid \{ \ell : A \opto B \} \uplus \Sigma\\
@@ -2274,33 +2237,68 @@ clauses.
   &M,N \in \CompCat    &::=& \cdots \mid \Do\;\ell\,V \mid \Handle \; M \; \With \; H\\[1ex]
 \end{syntax}
 %
+A signature is a collection of labels with operation types. An
+operation type $A \opto B$ is similar to the function type in that $A$
+denotes the domain (type of the argument) of the operation, and $B$
+denotes the codomain (return type). For simplicity, we will just
+assume a global fixed signature. The form $\Do\;\ell\,V$ is the
+application form for operations. It applies an operation $\ell$ with
+payload $V$. The construct $\Handle\;M\;\With\;H$ handles a
+computation $M$ with handler $H$.
+%
 \begin{mathpar}
+  \inferrule*
+   {{\bl
+       % C = A \eff \{(\ell_i : A_i \opto B_i)_i; R\} \\
+       % D = B \eff \{(\ell_i : P_i)_i;           R\}\\
+       \{\ell_i : A_i \opto B_i\}_i \in \Sigma \\
+       H = \{\Return\;x \mapsto M\} \uplus \{ \OpCase{\ell_i}{p_i}{k_i} \mapsto N_i \}_i \\
+       \el}\\\\
+       \typ{\Gamma, x : A;\Sigma}{M : D}\\\\
+       [\typ{\Gamma,p_i : A_i, k_i : B_i \to D;\Sigma}{N_i : D}]_i
+    }
+    {\typ{\Gamma;\Sigma}{H : C \Harrow D}}
+\end{mathpar}
+\begin{mathpar}
+  \inferrule*
+  {\{ \ell : A \opto B \} \in \Sigma \\ \typ{\Gamma;\Sigma}{V : A}}
+  {\typ{\Gamma;\Sigma}{\Do\;\ell\,V : B}}
+
   \inferrule*
   {
     \typ{\Gamma}{M : C} \\
     \typ{\Gamma}{H : C \Harrow D}
   }
   {\typ{\Gamma;\Sigma}{\Handle \; M \; \With\; H : D}}
-
-
-%\mprset{flushleft}
-  \inferrule*
-   {{\bl
-       % C = A \eff \{(\ell_i : A_i \opto B_i)_i; R\} \\
-       % D = B \eff \{(\ell_i : P_i)_i;           R\}\\
-       \{\ell_i : A_i \opto B_i\}_i \in \Sigma \\
-       H = \{\Return\;x \mapsto M\} \uplus \{ \OpCase{\ell_i}{p_i}{r_i} \mapsto N_i \}_i \\
-       \el}\\\\
-       \typ{\Gamma, x : A;\Sigma}{M : D}\\\\
-       [\typ{\Gamma,p_i : A_i, r_i : B_i \to D;\Sigma}{N_i : D}]_i
-    }
-    {\typ{\Gamma;\Sigma}{H : C \Harrow D}}
 \end{mathpar}
 %
+The first typing rule checks that the operation label of each
+operation clause is declared in the signature $\Sigma$. The signature
+provides the necessary information to construct the type of the
+payload parameters $p_i$ and the continuations $k_i$. Note that the
+domain of each continuation $k_i$ is compatible with the codomain of
+$\ell_i$, and the codomain of $k_i$ is compatible with the codomain of
+the handler.
+%
+The second and third typing rules are application of operations and
+handlers, respectively. The rule for operation application simply
+inspects the signature to check that the operation is declared, and
+that the type of the payload is compatible with the declared type.
+
+This particular presentation is nominal, because operations are
+declared up front. Nominal typing is the only sound option in the
+absence of an effect system (unless we restrict operations to work
+over a fixed type, say, an integer). In
+Chapter~\ref{ch:unary-handlers} we see a different presentation based
+on structural typing.
+
+The dynamic semantics of effect handlers are similar to that of
+$\fcontrol$, though, the $\slab{Value}$ rule is more interesting.
+%
 \begin{reductions}
   \slab{Value}    & \Handle\; V \;\With\;H   &\reducesto& M[V/x], \text{ where } \{\Return\;x \mapsto M\} \in H\\
   \slab{Capture}  & \Handle\;\EC[\Do\;\ell~V] \;\With\; H &\reducesto& M[V/p,\qq{\cont_{\Record{\EC;H}}}/k],\\
-  \multicolumn{4}{l}{\hfill\bl\text{where $\ell$ is not handled in $\EC$}\\\text{and }\{\ell~p~k \mapsto M\} \in H\el}\\
+  \multicolumn{4}{l}{\hfill\bl\text{where $\ell$ is not handled in $\EC$}\\\text{and }\{\OpCase{\ell}{p}{k} \mapsto M\} \in H\el}\\
   \slab{Resume}   & \Continue~\cont_{\Record{\EC;H}}~V &\reducesto& \Handle\;\EC[V]\;\With\;H\\
 \end{reductions}
 %
@@ -2325,7 +2323,105 @@ akin to fold over computation trees induced by effectful
 operations. The recursion is evident from $\slab{Resume}$ rule, as
 continuation invocation causes the same handler to be reinstalled
 along with the captured context.
+
+A classic example of handlers in action is handling of
+nondeterminism. Let us fix a signature with two operations.
 %
+\[
+  \Sigma \defas \{\Fail : \UnitType \opto \Zero; \Choose : \UnitType \opto \Bool\}
+\]
+%
+The $\Fail$ operation is essentially an exception as its codomain is
+the empty type, meaning that its continuation can never be
+invoked. The $\Choose$ operation returns a boolean.
+
+We will define a handler for each operation.
+%
+\[
+  \ba{@{~}l@{~}l}
+     H^{A}_{f} : A \Harrow \Option~A\\
+     H_{f} \defas \{ \Return\; x \mapsto \Some~x; &\OpCase{\Fail}{\Unit}{k} \mapsto \None \}\\
+     H^B_{c} : B \Harrow \List~B\\
+     H_{c} \defas \{ \Return\; x \mapsto [x]; &\OpCase{\Choose}{\Unit}{k} \mapsto k~\True \concat k~\False \}
+   \ea
+\]
+%
+The handler $H_f$ handles an invocation of $\Fail$ by dropping the
+continuation and simply returning $\None$ (due to the lack
+polymorphism, the definitions are parameterised by types $A$ and $B$
+respectively. We may consider them as universal type variables). The
+$\Return$-case of $H_f$ tags its argument with $\Some$.
+%
+The $H_c$ definition handles an invocation of $\Choose$ by first
+invoking the continuation $k$ with $\True$ and subsequently with
+$\False$. The two results are ultimately concatenated. The
+$\Return$-case lifts its argument into a singleton list.
+%
+Now, let us define a simple nondeterministic coin tossing computation
+with failure (by convention let us interpret $\True$ as heads and
+$\False$ as tails).
+%
+\[
+  \bl
+    \toss : \UnitType \to \Bool\\
+    \toss~\Unit \defas
+                  \ba[t]{@{~}l}
+                    \If\;\Do\;\Choose~\Unit\\
+                    \Then\;\Do\;\Choose~\Unit\\
+                    \Else\;\Absurd\;\Do\;\Fail
+                  \ea
+  \el
+\]
+%
+The computation $\toss$ first performs $\Choose$ in order to
+branch. If it returns $\True$ then a second instance of $\Choose$ is
+performed. Otherwise, it raises the $\Fail$ exception.
+%
+If we apply $\toss$ outside of $H_c$ and $H_f$ then the computation
+gets stuck as either $\Choose$ or $\Fail$, or both, would be
+unhandled. Thus, we have to run the computation in the context of both
+handlers. However, we have a choice to make as we can compose the
+handlers in either order. Let us first explore the composition, where
+$H_c$ is the outermost handler. Thus instantiate $H_c$ at type
+$\Option~\Bool$ and $H_f$ at type $\Bool$.
+%
+\begin{derivation}
+  & \Handle\;(\Handle\;\toss~\Unit\;\With\; H_f)\;\With\;H_c\\
+  \reducesto & \reason{$\beta$-reduction, $\EC = \If\;[\,]\;\Then \cdots$}\\
+  & \Handle\;(\Handle\; \EC[\Do\;\Choose~\Unit] \;\With\; H_f)\;\With\;H_c\\
+  \reducesto & \reason{\slab{Capture}, $\{\OpCase{\Choose}{\Unit}{k} \mapsto \cdots\} \in H_c$, $\EC' = (\Handle\;\EC\;\cdots)$}\\
+  & k~\True \concat k~\False, \qquad \text{where $k = \qq{\cont_{\Record{\EC';H_c}}}$}\\
+  \reducesto^+ & \reason{\slab{Resume} with $\True$}\\
+  & (\Handle\;(\Handle\;\EC[\True] \;\With\;H_f)\;\With\;H_c) \concat k~\False\\
+  \reducesto & \reason{$\beta$-reduction}\\
+  & (\Handle\;(\Handle\; \Do\;\Choose~\Unit \;\With\; H_f)\;\With\;H_c) \concat k~\False\\
+  \reducesto & \reason{\slab{Capture}, $\{\OpCase{\Choose}{\Unit}{k'} \mapsto \cdots\} \in H_c$, $\EC'' = (\Handle\;[\,]\;\cdots)$}\\
+  & (k'~\True \concat k'~\False) \concat k~\False, \qquad \text{where $k' = \qq{\cont_{\Record{\EC'';H_c}}}$}\\
+  \reducesto& \reason{\slab{Resume} with $\True$}\\
+  &((\Handle\;(\Handle\; \True \;\With\; H_f)\;\With\;H_c) \concat k'~\False) \concat k~\False\\
+  \reducesto& \reason{\slab{Value}, $\{\Return\;x \mapsto \cdots\} \in H_f$}\\
+  &((\Handle\;\Some~\True\;\With\;H_c) \concat k'~\False) \concat k~\False\\
+   \reducesto& \reason{\slab{Value}, $\{\Return\;x \mapsto \cdots\} \in H_c$}\\
+  & ([\Some~\True] \concat k'~\False) \concat k~\False\\
+  \reducesto^+& \reason{\slab{Resume} with $\False$, \slab{Value}, \slab{Value}}\\
+  & [\Some~\True] \concat [\Some~\False] \concat k~\False\\
+  \reducesto^+& \reason{\slab{Resume} with $\False$}\\
+  & [\Some~\True, \Some~\False] \concat (\Handle\;(\Handle\; \Absurd\;\Do\;\Fail~\Unit \;\With\; H_f)\;\With\;H_c)\\
+  \reducesto& \reason{\slab{Capture}, $\{\OpCase{\Fail}{\Unit}{k} \mapsto \cdots\} \in H_f$}\\
+  & [\Some~\True, \Some~\False] \concat (\Handle\; \None\; \With\; H_c)\\
+  \reducesto& \reason{\slab{Value}, $\{\Return\;x \mapsto \cdots\} \in H_c$}\\
+  & [\Some~\True, \Some~\False] \concat [\None] \reducesto [\Some~\True,\Some~\False,\None]
+\end{derivation}
+%
+Note how the invocation of $\Choose$ passes through $H_f$, because
+$H_f$ does not handle the operation. This is a key characteristic of
+handlers, and it is called \emph{effect forwarding}. Any handler will
+implicitly forward every operation that it does not handle.
+
+Suppose we were to swap the order of $H_c$ and $H_f$, then the
+computation would yield $\None$, because the invocation of $\Fail$
+would transfer control to $H_f$, which is the now the outermost
+handler, and it would drop the continuation and simply return $\None$.
 
 The alternative to deep handlers is known as \emph{shallow}
 handlers. They do not embody a particular recursion scheme, rather,
@@ -2333,7 +2429,8 @@ they correspond to case splits to over computation trees.
 %
 To distinguish between applications of deep and shallow handlers, we
 will mark the latter with a dagger superscript, i.e.
-$\ShallowHandle\; - \;\With\;-$.
+$\ShallowHandle\; - \;\With\;-$. Syntactically deep and shallow
+handler definitions are identical, however, their typing differ.
 %
 \begin{mathpar}
 %\mprset{flushleft}
@@ -2342,28 +2439,45 @@ $\ShallowHandle\; - \;\With\;-$.
        % C = A \eff \{(\ell_i : A_i \opto B_i)_i; R\} \\
        % D = B \eff \{(\ell_i : P_i)_i;           R\}\\
        \{\ell_i : A_i \opto B_i\}_i \in \Sigma \\
-       H = \{\Return\;x \mapsto M\} \uplus \{ \OpCase{\ell_i}{p_i}{r_i} \mapsto N_i \}_i \\
+       H = \{\Return\;x \mapsto M\} \uplus \{ \OpCase{\ell_i}{p_i}{k_i} \mapsto N_i \}_i \\
        \el}\\\\
        \typ{\Gamma, x : A;\Sigma}{M : D}\\\\
-       [\typ{\Gamma,p_i : A_i, r_i : B_i \to C;\Sigma}{N_i : D}]_i
+       [\typ{\Gamma,p_i : A_i, k_i : B_i \to C;\Sigma}{N_i : D}]_i
     }
     {\typ{\Gamma;\Sigma}{H : C \Harrow D}}
 \end{mathpar}
 %
+The difference is in the typing of the continuation $k_i$. The
+codomains of continuations must now be compatible with the return type
+$C$ of the handled computation. The typing suggests that an invocation
+of $k_i$ does not reinstall the handler. The dynamic semantics reveal
+that a shallow handler does not reify its own definition.
+%
 \begin{reductions}
   \slab{Capture}  & \ShallowHandle\;\EC[\Do\;\ell~V] \;\With\; H &\reducesto& M[V/p,\qq{\cont_{\EC}}/k],\\
   \multicolumn{4}{l}{\hfill\bl\text{where $\ell$ is not handled in $\EC$}\\\text{and }\{\ell~p~k \mapsto M\} \in H\el}\\
   \slab{Resume}   & \Continue~\cont_{\EC}~V &\reducesto& \EC[V]\\
 \end{reductions}
 %
-\begin{reductions}
-  \slab{Capture}  & \Handle\;\EC[\Do\;\ell~V] \;\With\; H &\reducesto& M[V/p,\qq{\cont_{\EC}}/k],\\
-  \multicolumn{4}{l}{\hfill\bl\text{where $\ell$ is not handled in $\EC$}\\\text{and }\{\ell~p~k \mapsto M\} \in H\el}\\
-  \slab{Resume}   & \Continue~\cont_{\EC}~V &\reducesto& \EC[V]\\
-\end{reductions}
+The $\slab{Capture}$ reifies the continuation up to the handler, and
+thus the $\slab{Resume}$ rule can only reinstate the captured
+continuation without the handler.
+%
+\dhil{Revisit the toss example with shallow handlers}
+% \begin{reductions}
+%   \slab{Capture}  & \Handle\;\EC[\Do\;\ell~V] \;\With\; H &\reducesto& M[V/p,\qq{\cont_{\EC}}/k],\\
+%   \multicolumn{4}{l}{\hfill\bl\text{where $\ell$ is not handled in $\EC$}\\\text{and }\{\ell~p~k \mapsto M\} \in H\el}\\
+%   \slab{Resume}   & \Continue~\cont_{\EC}~V &\reducesto& \EC[V]\\
+% \end{reductions}
 %
 
-Deep handlers can be used to simulate shift0 and reset0.
+Chapter~\ref{ch:unary-handlers} contains further examples of deep and
+shallow handlers in action.
+%
+\dhil{Consider whether to present the below encodings\dots}
+%
+Deep handlers can be used to simulate shift0 and
+reset0~\cite{KammarLO13}.
 %
 \begin{equations}
   \sembr{\shiftz~k.M} &\defas& \Do\;\dec{Shift0}~(\lambda k.M)\\
@@ -2371,13 +2485,14 @@ Deep handlers can be used to simulate shift0 and reset0.
               \ba[t]{@{~}l}\Handle\;m\,\Unit\;\With\\
                   ~\ba{@{~}l@{~}c@{~}l}
                       \Return\;x &\mapsto& x\\
-                      \OpCase{\dec{Shift0}}{f}{k} &\mapsto& f\,(\lambda x. \Continue~k~x)
+                      \OpCase{\dec{Shift0}}{f}{k} &\mapsto& f\,k
                    \ea
               \ea
 \end{equations}
 %
 
-Shallow handlers can be used to simulate control0 and prompt0.
+Shallow handlers can be used to simulate control0 and
+prompt0~\cite{KammarLO13}.
 %
 \begin{equations}
   \sembr{\Controlz~k.M} &\defas& \Do\;\dec{Control0}~(\lambda k.M)\\
@@ -2390,7 +2505,7 @@ Shallow handlers can be used to simulate control0 and prompt0.
               \ba[t]{@{~}l}\ShallowHandle\;m\,\Unit\;\With\\
                   ~\ba{@{~}l@{~}c@{~}l}
                       \Return\;x &\mapsto& x\\
-                      \OpCase{\dec{Control0}}{f}{k} &\mapsto& prompt0\,(\lambda\Unit.f\,(\lambda x. \Continue~k~x))
+                      \OpCase{\dec{Control0}}{f}{k} &\mapsto& prompt0\,(\lambda\Unit.f\,k)
                    \ea
               \ea
           \el
@@ -2401,6 +2516,8 @@ Shallow handlers can be used to simulate control0 and prompt0.
 
 \paragraph{\citeauthor{Longley09}'s catch-with-continue}
 %
+\dhil{TODO}
+%
 \begin{mathpar}
   \inferrule*
     {\typ{\Gamma, f : A \to B}{M : C \times D} \\ \Ground\;C}