Typo

thesis.bib

@@ -3606,3 +3606,25 @@
   edition = {3rd},
 }
 
+# Undelimited continuations survey
+@unpublished{FelleisenS99,
+  author = {Matthias Felleisen and Amr Sabry},
+  title  = {Continuations in Programming Practice: Introduction and Survey},
+  year   = 1999,
+  month  = aug,
+  note   = {Draft}
+}
+
+# TypeScript
+@inproceedings{BiermanAT14,
+  author    = {Gavin M. Bierman and
+               Mart{\'{\i}}n Abadi and
+               Mads Torgersen},
+  title     = {Understanding TypeScript},
+  booktitle = {{ECOOP}},
+  series    = {{LNCS}},
+  volume    = {8586},
+  pages     = {257--281},
+  publisher = {Springer},
+  year      = {2014}
+}

thesis.tex

@@ -2467,10 +2467,10 @@ $\CC~k.M$ to denote a control operator, or control reifier, which that
 reifies the control state and binds it to $k$ in the computation
 $M$. Here the control state will simply be an evaluation context. We
 will denote continuations by a special value $\cont_{\EC}$, which is
-indexed by the reified evaluation context $\EC$ to make notionally
-convenient to reflect the context again. To characterise delimited
-continuations we also need a control delimiter. We will write
-$\Delim{M}$ to denote a syntactic marker that delimits some
+indexed by the reified evaluation context $\EC$ to make it
+notationally convenient to reflect the context again. To characterise
+delimited continuations we also need a control delimiter. We will
+write $\Delim{M}$ to denote a syntactic marker that delimits some
 computation $M$.
 
 \paragraph{Undelimited continuation} The extent of an undelimited
@@ -14530,77 +14530,34 @@ $N'$ such that $N' \approxa \sdtrans{N}$ and $M' \reducesto^+ N'$.
 \end{theorem}
 %
 \begin{proof}
-  By case analysis on $\reducesto$ using Lemma~\ref{lem:sdtrans-subst}
-  and Lemma~\ref{lem:sdtrans-admin}. We show only the interesting case
-  $\semlab{Op^\dagger}$, which uses Lemma~\ref{lem:sdtrans-admin} to
-  approximate the body of the resumption up to administrative
-  reduction.\smallskip
-
+  By case analysis on $\reducesto$ and induction on $\approxa$ using
+  Lemma~\ref{lem:sdtrans-subst} and Lemma~\ref{lem:sdtrans-admin}.
+  %
   \noindent\textbf{Case} $\ShallowHandle\;\EC[\Do\;\ell~V]\;\With\;H \reducesto
   N_\ell[V/p,\lambda y.\EC[\Return\;y]/r]$ where
   $\ell \notin \BL(\EC)$ and
   $H^\ell = \{\OpCase{\ell}{p}{r} \mapsto N_\ell\}$. \smallskip\\
-  %
-  Pick $M' =
-  \sdtrans{\ShallowHandle\;\EC[\Do\;\ell~V]\;\With\;H}$. Clearly
-  $M' \approxa \sdtrans{M}$. We compute $N'$ via reduction as follows.
-  \begin{derivation}
+  There are three subcases to consider.
+  \begin{enumerate}
+  \item Base step:
+    $M' = \sdtrans{\ShallowHandle\;\EC[\Do\;\ell~V]\;\With\;H}$. We
+    can compute $N'$ by direct calculation starting from $M'$ yielding
+    %
+    \begin{derivation}
     & \sdtrans{\ShallowHandle\;\EC[\Do\;\ell~V]\;\With\;H}\\
-    =& \reason{definition of $\sdtrans{-}$}\\
-    &\bl
-      \Let\;z \revto \Handle\;\sdtrans{\EC}[\Do\;\ell~\sdtrans{V}]\;\With\;\sdtrans{H}\;\In\\
-      \Let\;\Record{f;g} = z\;\In\;g\,\Unit
-     \el\\
-     \reducesto^+& \reason{\semlab{Op} using assumption $\ell \notin \BL(\sdtrans{\EC})$, \semlab{Let}, \semlab{Let}}\\
-   % &\bl
-   %    \Let\;z \revto
-   %     (\bl
-   %       \Let\;r \revto \lambda x.\Let\;z \revto r~x\;\In\;\Let\;\Record{f;g} = z\;\In\;f\,\Unit\;\In\\
-   %       \Return\;\Record{
-   %         \bl
-   %         \lambda\Unit.\Let\;x \revto \Do\;\ell~p\;\In\;r~x;\\
-   %         \lambda\Unit.\sdtrans{N_\ell}})[
-   %           \bl
-   %             \sdtrans{V}/p,\\
-   %             \lambda y.\Handle\;\sdtrans{\EC}[\Return\;y]\;\With\;\sdtrans{H}/r]
-   %           \el
-   %       \el
-   %       \el\\
-   %   \In\;\Let\;\Record{f;g} = z\;\In\;g\,\Unit
-   %   \el\\
-   % \reducesto^+& \reason{\semlab{Let}, \semlab{Let}}\\
-   &\bl
-   \Let\;\Record{f;g} = \Record{
-     \bl
-     \lambda\Unit.\Let\;x \revto \Do\;\ell~\sdtrans{V}\;\In\;r~x;\\
-     \lambda\Unit.\sdtrans{N_\ell}}[\lambda x.
-             \bl
-             \Let\;z \revto (\lambda y.\Handle\;\sdtrans{\EC}[\Return\;y]\;\With\;\sdtrans{H})~x\;\In\\
-             \Let\;\Record{f;g} = z\;\In\;f\,\Unit/r,\sdtrans{V}/p]\;\In\; g\,\Unit
-             \el
-     \el\\
-     \el\\
-  \reducesto^+ &\reason{\semlab{Split}, \semlab{App}}\\
-  &\sdtrans{N_\ell}[\lambda x.
-             \bl
-             \Let\;z \revto (\lambda y.\Handle\;\sdtrans{\EC}[\Return\;y]\;\With\;\sdtrans{H})~x\;\In\\
-             \Let\;\Record{f;g} = z\;\In\;f\,\Unit/r,\sdtrans{V}/p]
-             \el\\
-  =& \reason{by Lemma~\ref{lem:sdtrans-subst}}\\
+    =\reducesto^+& \reason{\semlab{Op} ($\ell \notin \BL(\sdtrans{\EC})$), $2\times$\semlab{Let},\semlab{Split},\semlab{App}, Lemma~\ref{lem:sdtrans-subst}}\\
    &\sdtrans{N_\ell[\lambda x.
              \bl
              \Let\;z \revto (\lambda y.\Handle\;\EC[\Return\;y]\;\With\;H)~x\;\In\\
              \Let\;\Record{f;g} = z\;\In\;f\,\Unit/r,V/p]}
-             \el
+           \el\\
   \end{derivation}
   %
-  We take the above computation term to be our $N'$. If
+  Take the final term to be $N'$. If the resumption
   $r \notin \FV(N_\ell)$ then the two terms $N'$ and
   $\sdtrans{N_\ell[V/p,\lambda y.\EC[\Return\;y]/r]}$ are the
-  identical, and thus by reflexivity of the $\approxa$-relation it
-  follows that
-  $N' \approxa \sdtrans{N_\ell[V/p,\lambda
-    y.\EC[\Return\;y]/r]}$. Otherwise $N'$ approximates
+  identical, and thus the result follows immediate by reflexivity of
+  the $\approxa$-relation. Otherwise $N'$ approximates
   $N_\ell[V/p,\lambda y.\EC[\Return\;y]/r]$ at least up to a use of
   $r$. We need to show that the approximation remains faithful during
   any application of $r$. Specifically, we proceed to show that for
@@ -14629,7 +14586,122 @@ $N'$ such that $N' \approxa \sdtrans{N}$ and $M' \reducesto^+ N'$.
   Defintion~\ref{def:approx-admin} that
   $\EC'[\sdtrans{\EC}[\Return\;W]] \approxa
   \sdtrans{\EC}[\Return\;W]$.
+
+  \item Inductive step: Assume $M' \reducesto M''$ and
+    $M'' \approxa \sdtrans{\ShallowHandle\;\EC[\Do\;\ell~V]\;\With\;H}$. Using a similar argument to above we get that
+    \[
+      \sdtrans{\ShallowHandle\;\EC[\Do\;\ell~V]\;\With\;H}
+      \reducesto^+ \sdtrans{N_\ell[V/p,\lambda y.\EC[\Return\;y]/r]}.
+    \]
+    Take $N' = M''$ then by the first induction hypothesis
+    $M' \reducesto N'$ and by the second induction hypothesis
+    $N' \approxa \sdtrans{N_\ell[V/p,\lambda y.\EC[\Return\;y]/r]}$ as
+    desired.
+  \item Inductive step: Assume $admin(\EC')$ and
+    $M' \approxa \sdtrans{\ShallowHandle\;\EC[\Do\;\ell~V]\;\With\;H}$.
+  \end{enumerate}
 \end{proof}
+% \begin{proof}
+%   By case analysis on $\reducesto$ using Lemma~\ref{lem:sdtrans-subst}
+%   and Lemma~\ref{lem:sdtrans-admin}. We show only the interesting case
+%   $\semlab{Op^\dagger}$, which uses Lemma~\ref{lem:sdtrans-admin} to
+%   approximate the body of the resumption up to administrative
+%   reduction.\smallskip
+
+%   \noindent\textbf{Case} $\ShallowHandle\;\EC[\Do\;\ell~V]\;\With\;H \reducesto
+%   N_\ell[V/p,\lambda y.\EC[\Return\;y]/r]$ where
+%   $\ell \notin \BL(\EC)$ and
+%   $H^\ell = \{\OpCase{\ell}{p}{r} \mapsto N_\ell\}$. \smallskip\\
+%   %
+%   Pick $M' =
+%   \sdtrans{\ShallowHandle\;\EC[\Do\;\ell~V]\;\With\;H}$. Clearly
+%   $M' \approxa \sdtrans{M}$. We compute $N'$ via reduction as follows.
+%   \begin{derivation}
+%     & \sdtrans{\ShallowHandle\;\EC[\Do\;\ell~V]\;\With\;H}\\
+%     =& \reason{definition of $\sdtrans{-}$}\\
+%     &\bl
+%       \Let\;z \revto \Handle\;\sdtrans{\EC}[\Do\;\ell~\sdtrans{V}]\;\With\;\sdtrans{H}\;\In\\
+%       \Let\;\Record{f;g} = z\;\In\;g\,\Unit
+%      \el\\
+%      \reducesto^+& \reason{\semlab{Op} using assumption $\ell \notin \BL(\sdtrans{\EC})$, \semlab{Let}, \semlab{Let}}\\
+%    % &\bl
+%    %    \Let\;z \revto
+%    %     (\bl
+%    %       \Let\;r \revto \lambda x.\Let\;z \revto r~x\;\In\;\Let\;\Record{f;g} = z\;\In\;f\,\Unit\;\In\\
+%    %       \Return\;\Record{
+%    %         \bl
+%    %         \lambda\Unit.\Let\;x \revto \Do\;\ell~p\;\In\;r~x;\\
+%    %         \lambda\Unit.\sdtrans{N_\ell}})[
+%    %           \bl
+%    %             \sdtrans{V}/p,\\
+%    %             \lambda y.\Handle\;\sdtrans{\EC}[\Return\;y]\;\With\;\sdtrans{H}/r]
+%    %           \el
+%    %       \el
+%    %       \el\\
+%    %   \In\;\Let\;\Record{f;g} = z\;\In\;g\,\Unit
+%    %   \el\\
+%    % \reducesto^+& \reason{\semlab{Let}, \semlab{Let}}\\
+%    &\bl
+%    \Let\;\Record{f;g} = \Record{
+%      \bl
+%      \lambda\Unit.\Let\;x \revto \Do\;\ell~\sdtrans{V}\;\In\;r~x;\\
+%      \lambda\Unit.\sdtrans{N_\ell}}[\lambda x.
+%              \bl
+%              \Let\;z \revto (\lambda y.\Handle\;\sdtrans{\EC}[\Return\;y]\;\With\;\sdtrans{H})~x\;\In\\
+%              \Let\;\Record{f;g} = z\;\In\;f\,\Unit/r,\sdtrans{V}/p]\;\In\; g\,\Unit
+%              \el
+%      \el\\
+%      \el\\
+%   \reducesto^+ &\reason{\semlab{Split}, \semlab{App}}\\
+%   &\sdtrans{N_\ell}[\lambda x.
+%              \bl
+%              \Let\;z \revto (\lambda y.\Handle\;\sdtrans{\EC}[\Return\;y]\;\With\;\sdtrans{H})~x\;\In\\
+%              \Let\;\Record{f;g} = z\;\In\;f\,\Unit/r,\sdtrans{V}/p]
+%              \el\\
+%   =& \reason{by Lemma~\ref{lem:sdtrans-subst}}\\
+%    &\sdtrans{N_\ell[\lambda x.
+%              \bl
+%              \Let\;z \revto (\lambda y.\Handle\;\EC[\Return\;y]\;\With\;H)~x\;\In\\
+%              \Let\;\Record{f;g} = z\;\In\;f\,\Unit/r,V/p]}
+%              \el
+%   \end{derivation}
+%   %
+%   We take the above computation term to be our $N'$. If
+%   $r \notin \FV(N_\ell)$ then the two terms $N'$ and
+%   $\sdtrans{N_\ell[V/p,\lambda y.\EC[\Return\;y]/r]}$ are the
+%   identical, and thus by reflexivity of the $\approxa$-relation it
+%   follows that
+%   $N' \approxa \sdtrans{N_\ell[V/p,\lambda
+%     y.\EC[\Return\;y]/r]}$. Otherwise $N'$ approximates
+%   $N_\ell[V/p,\lambda y.\EC[\Return\;y]/r]$ at least up to a use of
+%   $r$. We need to show that the approximation remains faithful during
+%   any application of $r$. Specifically, we proceed to show that for
+%   any value $W \in \ValCat$
+%   %
+%   \[
+%     (\bl
+%      \lambda x.\Let\;z \revto (\lambda y.\Handle\;\sdtrans{\EC}[\Return\;y]\;\With\;\sdtrans{H})~x\;\In\\
+%     \Let\;\Record{f;g} = z \;\In\;f\,\Unit)~W \approxa (\lambda y.\sdtrans{\EC}[\Return\;y])~W.
+%     \el
+%   \]
+%   %
+%   The right hand side reduces to $\sdtrans{\EC}[\Return\;W]$. Two
+%   applications of \semlab{App} on the left hand side yield the term
+%   %
+%   \[
+%     \Let\;z \revto \Handle\;\sdtrans{\EC}[\Return\;W]\;\With\;\sdtrans{H}\;\In\;\Let\;\Record{f;g} = z \;\In\;f\,\Unit.
+%   \]
+%   %
+%   Define
+%   %
+%   $\EC' \defas \Let\;z \revto \Handle\; [\,]\;\With\;\sdtrans{H}\;\In\;\Let\;\Record{f;g} = z \;\In\;f\,\Unit$
+%   %
+%   such that $\EC'$ is an administrative evaluation context by
+%   Lemma~\ref{lem:sdtrans-admin}. Then it follows by
+%   Defintion~\ref{def:approx-admin} that
+%   $\EC'[\sdtrans{\EC}[\Return\;W]] \approxa
+%   \sdtrans{\EC}[\Return\;W]$.
+% \end{proof}
 
 \section{Parameterised handlers as ordinary deep handlers}
 \label{sec:param-desugaring}
@@ -14847,16 +14919,44 @@ the captured context and continuation invocation context to coincide.
 \def\N{{\mathbb N}}
 %
 
-Effect handlers are capable of codifying a wealth of powerful
-programming constructs and features such as exceptions, state,
-backtracking, coroutines, await/async, inversion of control, and so
-on.
+When extending some programming language $\LLL \subset \LLL'$ with
+some new feature it is desirable to know exactly how the new feature
+impacts the language. At a bare minimum it is useful to know whether
+the extended language $\LLL'$ is unsound as a result of inhabiting the
+new feature (although, some languages are designed deliberately to be
+unsound~\cite{BiermanAT14}). More fundamentally, it may be useful for
+theoreticians and practitioners alike to know whether the extended
+language is more expressive than the base language as it may inform
+programming practice.
 %
-Thus, effect handlers are expressive enough to implement a wide
-variety of other programming abstractions.
+Specifically, it may be of interest to know whether the extended
+language $\LLL'$ exhibits any \emph{essential} expressivity when
+compared to the base language $\LLL$. Questions about essential
+expressivity fall under three different headings.
+
+% There are various ways in which we can consider how some new feature
+% impacts the expressiveness of its host language.  For instance,
+% \citet{Felleisen91} considers the question of whether a language
+% $\LLL$ admits a translation into a sublanguage $\LLL'$ in a way which
+% respects not only the behaviour of programs but also aspects of their
+% global or local syntactic structure. If the translation of some
+% $\LLL$-program into $\LLL'$ requires a complete global restructuring,
+% we may say that $\LLL'$ is in some way less expressive than $\LLL$.
+
+
+% Effect handlers are capable of codifying a wealth of powerful
+% programming constructs and features such as exceptions, state,
+% backtracking, coroutines, await/async, inversion of control, and so
+% on.
 %
-We may wonder about the exact nature of this expressiveness, i.e. do
-effect handlers exhibit any \emph{essential} expressivity?
+
+% Partial continuations as the difference of continuations a duumvirate of control operators
+
+% Thus, effect handlers are expressive enough to implement a wide
+% variety of other programming abstractions.
+% %
+% We may wonder about the exact nature of this expressiveness, i.e. do
+% effect handlers exhibit any \emph{essential} expressivity?
 
 % In today's programming languages we find a wealth of powerful
 % constructs and features --- exceptions, higher-order store, dynamic
@@ -14879,51 +14979,56 @@ effect handlers exhibit any \emph{essential} expressivity?
 % Start with talking about the power of backtracking (folklore)
 % giving a precise and robust mathematical characterisation of this phenomenon
 
-However, in this chapter we will look at even more fundamental
-expressivity differences that would not be bridged even if
-whole-program translations were admitted. These fall under two
-headings.
+% However, in this chapter we will look at even more fundamental
+% expressivity differences that would not be bridged even if
+% whole-program translations were admitted. These fall under two
+% headings.
+
+% Questions regarding essential expressivity differences fall under two
+% headings.
 %
-\begin{enumerate}
-\item \emph{Computability}: Are there operations of a given type
-  that are programmable in $\LLL$ but not expressible at all in $\LLL'$?
-\item \emph{Complexity}: Are there operations programmable in $\LLL$
-  with some asymptotic runtime bound (e.g.\ `$\BigO(n^2)$') that cannot be
-  achieved in $\LLL'$?
-\end{enumerate}
+\begin{description}
+\item[Programmability] Are there programmable operations that can be
+  done more easily in $\LLL'$ than in $\LLL$?
+\item[Computability] Are there operations of a given type
+  that are programmable in $\LLL'$ but not expressible at all in $\LLL$?
+\item[Complexity] Are there operations programmable in $\LLL'$
+  with some asymptotic runtime bound (e.g. `$\BigO(n^2)$') that cannot be
+  achieved in $\LLL$?
+\end{description}
 %
 % We may also ask: are there examples of \emph{natural, practically
 %   useful} operations that manifest such differences?  If so, this
 % might be considered as a significant advantage of $\LLL$ over $\LLL'$.
 
-If the `operations' we are asking about are ordinary first-order
-functions, that is both their inputs and outputs are of ground type
-(strings, arbitrary-size integers etc), then the situation is easily
-summarised.  At such types, all reasonable languages give rise to the
-same class of programmable functions, namely the Church-Turing
-computable ones.  As for complexity, the runtime of a program is
-typically analysed with respect to some cost model for basic
-instructions (e.g.\ one unit of time per array access).  Although the
-realism of such cost models in the asymptotic limit can be questioned
-(see, e.g., \citet[Section~2.6]{Knuth97}), it is broadly taken as read
-that such models are equally applicable whatever programming language
-we are working with, and moreover that all respectable languages can
-represent all algorithms of interest; thus, one does not expect the
-best achievable asymptotic run-time for a typical algorithm (say in
-number theory or graph theory) to be sensitive to the choice of
-programming language, except perhaps in marginal cases.
+% If the `operations' we are asking about are ordinary first-order
+% functions, that is both their inputs and outputs are of ground type
+% (strings, arbitrary-size integers etc), then the situation is easily
+% summarised.  At such types, all reasonable languages give rise to the
+% same class of programmable functions, namely the Church-Turing
+% computable ones.  As for complexity, the runtime of a program is
+% typically analysed with respect to some cost model for basic
+% instructions (e.g.\ one unit of time per array access).  Although the
+% realism of such cost models in the asymptotic limit can be questioned
+% (see, e.g., \citet[Section~2.6]{Knuth97}), it is broadly taken as read
+% that such models are equally applicable whatever programming language
+% we are working with, and moreover that all respectable languages can
+% represent all algorithms of interest; thus, one does not expect the
+% best achievable asymptotic run-time for a typical algorithm (say in
+% number theory or graph theory) to be sensitive to the choice of
+% programming language, except perhaps in marginal cases.
 
-The situation changes radically, however, if we consider
-\emph{higher-order} operations: programmable operations whose inputs
-may themselves be programmable operations.  Here it turns out that
-both what is computable and the efficiency with which it can be
-computed can be highly sensitive to the selection of language features
-present. This is in fact true more widely for \emph{abstract data
-  types}, of which higher-order types can be seen as a special case: a
-higher-order value will be represented within the machine as ground
-data, but a program within the language typically has no access to
-this internal representation, and can interact with the value only by
-applying it to an argument.
+% The situation changes radically, however, if we consider
+% \emph{higher-order} operations: programmable operations whose inputs
+% may themselves be programmable operations.  Here it turns out that
+% both what is computable and the efficiency with which it can be
+% computed can be highly sensitive to the selection of language features
+% present. This is in fact true more widely for \emph{abstract data
+%   types}, of which higher-order types can be seen as a special case: a
+% higher-order value will be represented within the machine as ground
+% data, but a program within the language typically has no access to
+% this internal representation, and can interact with the value only by
+% applying it to an argument.
 
 % Most work in this area to date has focused on computability
 % differences. One of the best known examples is the \emph{parallel if}
@@ -14972,31 +15077,39 @@ applying it to an argument.
 % various languages are found to coincide with some well-known
 % complexity classes.
 
-The purpose of this chapter is to give a clear example of such an
-inherent complexity difference higher up in the expressivity spectrum.
-Specifically, we consider the following \emph{generic count} problem,
+The purpose of this chapter is to give a clear example of an essential
+complexity difference. Specifically, we will show that if we take a
+typical PCF-like base language, $\BPCF$, and extend it with effect
+handlers, $\HPCF$, then there exists a class of programs that have
+asymptotically more efficient realisations in $\HPCF$ than possible in
+$\BPCF$, hence establishing that effect handlers enable an asymptotic
+speedup for some programs.
+%
+% The purpose of this chapter is to give a clear example of such an
+% inherent complexity difference higher up in the expressivity spectrum.
+
+To this end, we consider the following \emph{generic count} problem,
 parametric in $n$: given a boolean-valued predicate $P$ on the space
-${\mathbb B}^n$ of boolean vectors of length $n$, return the number of
+$\mathbb{B}^n$ of boolean vectors of length $n$, return the number of
 such vectors $q$ for which $P\,q = \True$.  We shall consider boolean
 vectors of any length to be represented by the type $\Nat \to \Bool$;
 thus for each $n$, we are asking for an implementation of a certain
-third-order operation
+third-order function.
 %
 \[ \Count_n : ((\Nat \to \Bool) \to \Bool) \to \Nat  \]
 %
-A \naive implementation strategy, supported by any reasonable
-language, is simply to apply $P$ to each of the $2^n$ vectors in turn.
-A much less obvious, but still purely `functional', approach due to
-\citet{Berger90} achieves the effect of `pruned search' where the
-predicate allows it (serving as a warning that counter-intuitive
-phenomena can arise in this territory).  Nonetheless, under a mild
-condition on $P$ (namely that it must inspect all $n$ components of
-the given vector before returning), both these approaches will have a
-$\Omega(n 2^n)$ runtime.  Moreover, we shall show that in a typical
-call-by-value language without advanced control features, one cannot
-improve on this: \emph{any} implementation of $\Count_n$ must
-necessarily take time $\Omega(n2^n)$ on \emph{any} predicate $P$.  On
-the other hand, if we extend our language with effect handlers, it
+A \naive implementation strategy is simply to apply $P$ to each of the
+$2^n$ vectors in turn.  However, one can do better with a curious
+approach due to \citet{Berger90}, which achieves the effect of `pruned
+search' where the predicate allows it. This should be taken as a
+warning that counter-intuitive phenomena can arise in this territory.
+Nonetheless, under the mild condition that $P$ must inspect all $n$
+components of the given vector before returning, both these approaches
+will have a $\Omega(n 2^n)$ runtime.  Moreover, we shall show that in
+$\BPCF$, a typical call-by-value language without advanced control
+features, one cannot improve on this: \emph{any} implementation of
+$\Count_n$ must necessarily take time $\Omega(n2^n)$ on \emph{any}
+predicate $P$.  Conversely, in the extended language $\HPCF$ it
 becomes possible to bring the runtime down to $\BigO(2^n)$: an
 asymptotic gain of a factor of $n$.
 
@@ -15013,43 +15126,44 @@ asymptotic gain of a factor of $n$.
 % $\BigO(2^n)$ runtime for generic count with effect handlers also
 % transfers to generic search.
 
-The idea behind the speedup is easily explained and will already be
-familiar, at least informally, to programmers who have worked with
-multi-shot continuations.
+The key to enabling the speedup is \emph{backtracking} via multi-shot
+resumptions. The idea is to memorise the control state at each
+component inspection to make it possible to quickly backtrack to a
+prior inspection and make a different decision as soon as one
+possible result has been computed.
 %
-Suppose for example $n=3$, and suppose that the predicate $P$ always
-inspects the components of its argument in the order $0,1,2$.
+Concretely, suppose for example $n = 3$, and suppose that the predicate
+$P$ always inspects the components of its argument in the order
+$0,1,2$.
 %
-A \naive implementation of $\Count_3$ might start by applying the given
-$P$ to $q_0 = (\True,\True,\True)$, and then to
-$q_1 = (\True,\True,\False)$.  Clearly there is some duplication here:
-the computations of $P\,q_0$ and $P\,q_1$ will proceed identically up
-to the point where the value of the final component is requested. What
-we would like to do, then, is to record the state of the computation
-of $P\,q_0$ at just this point, so that we can later resume this
+A \naive implementation of $\Count_3$ might start by applying the
+given predicate $P$ to $q_0 = (\True,\True,\True)$, and then to
+$q_1 = (\True,\True,\False)$.  Note that there is some duplication
+here: the computations of $P\,q_0$ and $P\,q_1$ will proceed
+identically up to the point where the value of the final component is
+requested. Ideally, we would record the state of the computation of
+$P\,q_0$ at just this point, so that we can later resume this
 computation with $\False$ supplied as the final component value in
-order to obtain the value of $P\,q_1$. (Similarly for all other
-internal nodes in the evident binary tree of boolean vectors.) Of
-course, this `backup' approach would be standardly applied if one were
-implementing a bespoke search operation for some \emph{particular}
-choice of $P$ (corresponding, say, to the $n$-queens problem); but to
-apply this idea of resuming previous subcomputations in the
-\emph{generic} setting (that is, uniformly in $P$) requires some
-special language feature such as effect handlers or multi-shot
-continuations.
+order to obtain the value of $P\,q_1$.  Of course, a bespoke search
+function implementation would apply this backtracking behaviour in a
+standard manner for some \emph{particular} choice of $P$ (e.g. the
+$n$-queens problem); but to apply this idea of resuming previous
+subcomputations in the \emph{generic} setting (i.e. uniformly in $P$)
+requires some special control feature such as effect handlers with
+multi-shot resumptions.
 %
-One could also obviate the need for such a feature by choosing to
-present the predicate $P$ in some other way, but from our present
-perspective this would be to move the goalposts: our intention is
-precisely to show that our languages differ in an essential way
-\emph{as regards their power to manipulate data of type} $(\Nat \to
-\Bool) \to \Bool$.
+Obviously, one can remove the need a special control feature by a
+change of type for the predicate $P$, but this such a change shifts
+the perspective. The intention is precisely to show that the languages
+differ in an essential way as regards to their power to manipulate
+data of type $(\Nat \to \Bool) \to \Bool$.
 
-This idea of using first-class control to achieve backtracking has
-been exploited before and is fairly widely known (see
-e.g. \citep{KiselyovSFA05}), and there is a clear programming
-intuition that this yields a speedup unattainable in languages without
-such control features.  % Our main contribution in this paper is to
+The idea of using first-class control achieve backtracking is fairly
+well-known in the literature~\cite{KiselyovSFA05}, and there is a
+clear programming intuition that this yields a speedup unattainable in
+languages without such control features.
+
+% Our main contribution in this paper is to
 % provide, for the first time, a precise mathematical theorem that pins
 % down this fundamental efficiency difference, thus giving formal
 % substance to this intuition.  Since our goal is to give a realistic
@@ -15148,8 +15262,7 @@ Fine-grain call-by-value is similar to A-normal
 form~\cite{FlanaganSDF93} in that every intermediate computation is
 named, but unlike A-normal form is closed under reduction.
 
-The syntax of $\BPCF$ is as follows.
-{\noindent
+\begin{figure}
   \begin{syntax}
     \slab{Types}          &A,B,C,D\in\TypeCat  &::= & \Nat \mid \One \mid A \to B \mid A \times B \mid A + B \\
     \slab{Type\textrm{ }environments} &\Gamma\in\TyEnvCat &::= & \cdot \mid \Gamma, x:A \\
@@ -15162,7 +15275,12 @@ The syntax of $\BPCF$ is as follows.
                      &     &\mid&\Case \; V \;\{ \Inl \; x \mapsto M; \Inr \; y \mapsto N\}\\
                      &    &\mid& \Return\; V
                            \mid \Let \; x \revto M \; \In \; N \\
-\end{syntax}}%
+\end{syntax}
+\caption{Syntax of $\BPCF$.}\label{fig:bpcf}
+\end{figure}
+%
+Figure~\ref{fig:bpcf} depicts the type syntax, type environment
+syntax, and term syntax of $\BPCF$.
 %
 The ground types are $\Nat$ and $\One$ which classify natural number
 values and the unit value, respectively. The function type $A \to B$
@@ -15172,7 +15290,7 @@ whose first and second components have types $A$ and $B$
 respectively. The sum type $A + B$ classifies tagged values of either
 type $A$ or $B$.
 %
-Type environments $\Gamma$ map term variables to their types.
+Type environments $\Gamma$ map variables to their types.
 
 We let $k$ range over natural numbers and $c$ range over primitive
 operations on natural numbers ($+, -, =$).
@@ -15183,17 +15301,17 @@ For convenience, we also use $f$, $g$, and $h$ for variables of
 function type, $i$ and $j$ for variables of type $\Nat$, and $r$ to
 denote resumptions.
 %
-The value terms are standard.
-% Value terms comprise variables ($x$), the unit value ($\Unit$),
-% natural number literals ($n$), primitive constants ($c$), lambda
-% abstraction ($\lambda x^A . \, M$), recursion
-% ($\Rec \; f^{A \to B}\, x.M$), pairs ($\Record{V, W}$), left
-% ($(\Inl~V)^B$) and right $((\Inr~W)^A)$ injections.
+% The value terms are standard.
+Value terms comprise variables ($x$), the unit value ($\Unit$),
+natural number literals ($n$), primitive constants ($c$), lambda
+abstraction ($\lambda x^A . \, M$), recursion
+($\Rec \; f^{A \to B}\, x.M$), pairs ($\Record{V, W}$), left
+($(\Inl~V)^B$) and right $((\Inr~W)^A)$ injections.
 
 %
-We will occasionally blur the distinction between object and meta
-language by writing $A$ for the meta level type of closed value terms
-of type $A$.
+% We will occasionally blur the distinction between object and meta
+% language by writing $A$ for the meta level type of closed value terms
+% of type $A$.
 %
 All elimination forms are computation terms. Abstraction is eliminated
 using application ($V\,W$).
@@ -18166,7 +18284,12 @@ the various kinds of control phenomena that appear in the literature
 as well as providing an overview of the operational characteristics of
 control operators appearing in the literature. To the best of my
 knowledge this survey is the only of its kind in the present
-literature.
+literature (other studies survey a particular control phenomenon,
+e.g. \citet{FelleisenS99} survey undelimited continuations as provided
+by call/cc in programming practice, \citet{DybvigJS07} classify
+delimited control operators according to their delimiter placement,
+and \citet{Brachthauser20} provides a delimited control perspective on
+effect handlers).
 
 In Part~\ref{p:design} I have presented the design of a ML-like
 programming language equipped an effect-and-type system and a