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
+indexed by the reified evaluation context $\EC$ to make it
-convenient to reflect the context again. To characterise delimited
+notationally convenient to reflect the context again. To characterise
-continuations we also need a control delimiter. We will write
+delimited continuations we also need a control delimiter. We will
-$\Delim{M}$ to denote a syntactic marker that delimits some
+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}
+  By case analysis on $\reducesto$ and induction on $\approxa$ using
-  and Lemma~\ref{lem:sdtrans-admin}. We show only the interesting case
+  Lemma~\ref{lem:sdtrans-subst} and Lemma~\ref{lem:sdtrans-admin}.
-  $\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\\
+  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
     %
-  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{-}$}\\
+    =\reducesto^+& \reason{\semlab{Op} ($\ell \notin \BL(\sdtrans{\EC})$), $2\times$\semlab{Let},\semlab{Split},\semlab{App}, Lemma~\ref{lem:sdtrans-subst}}\\
-    &\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
+           \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
+  identical, and thus the result follows immediate by reflexivity of
-  follows that
+  the $\approxa$-relation. Otherwise $N'$ approximates
-  $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
@@ -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
+When extending some programming language $\LLL \subset \LLL'$ with
-programming constructs and features such as exceptions, state,
+some new feature it is desirable to know exactly how the new feature
-backtracking, coroutines, await/async, inversion of control, and so
+impacts the language. At a bare minimum it is useful to know whether
-on.
+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
+Specifically, it may be of interest to know whether the extended
-variety of other programming abstractions.
+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
+% However, in this chapter we will look at even more fundamental
-expressivity differences that would not be bridged even if
+% expressivity differences that would not be bridged even if
-whole-program translations were admitted. These fall under two
+% whole-program translations were admitted. These fall under two
-headings.
+% headings.
+
+% Questions regarding essential expressivity differences fall under two
+% headings.
 %
-\begin{enumerate}
+\begin{description}
-\item \emph{Computability}: Are there operations of a given type
+\item[Programmability] Are there programmable operations that can be
-  that are programmable in $\LLL$ but not expressible at all in $\LLL'$?
+  done more easily in $\LLL'$ than in $\LLL$?
-\item \emph{Complexity}: Are there operations programmable in $\LLL$
+\item[Computability] Are there operations of a given type
-  with some asymptotic runtime bound (e.g.\ `$\BigO(n^2)$') that cannot be
+  that are programmable in $\LLL'$ but not expressible at all in $\LLL$?
-  achieved in $\LLL'$?
+\item[Complexity] Are there operations programmable in $\LLL'$
-\end{enumerate}
+  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
+% If the `operations' we are asking about are ordinary first-order
-functions, that is both their inputs and outputs are of ground type
+% functions, that is both their inputs and outputs are of ground type
-(strings, arbitrary-size integers etc), then the situation is easily
+% (strings, arbitrary-size integers etc), then the situation is easily
-summarised.  At such types, all reasonable languages give rise to the
+% summarised.  At such types, all reasonable languages give rise to the
-same class of programmable functions, namely the Church-Turing
+% same class of programmable functions, namely the Church-Turing
-computable ones.  As for complexity, the runtime of a program is
+% computable ones.  As for complexity, the runtime of a program is
-typically analysed with respect to some cost model for basic
+% typically analysed with respect to some cost model for basic
-instructions (e.g.\ one unit of time per array access).  Although the
+% instructions (e.g.\ one unit of time per array access).  Although the
-realism of such cost models in the asymptotic limit can be questioned
+% 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
+% (see, e.g., \citet[Section~2.6]{Knuth97}), it is broadly taken as read
-that such models are equally applicable whatever programming language
+% that such models are equally applicable whatever programming language
-we are working with, and moreover that all respectable languages can
+% we are working with, and moreover that all respectable languages can
-represent all algorithms of interest; thus, one does not expect the
+% represent all algorithms of interest; thus, one does not expect the
-best achievable asymptotic run-time for a typical algorithm (say in
+% best achievable asymptotic run-time for a typical algorithm (say in
-number theory or graph theory) to be sensitive to the choice of
+% number theory or graph theory) to be sensitive to the choice of
-programming language, except perhaps in marginal cases.
+% programming language, except perhaps in marginal cases.
 
-The situation changes radically, however, if we consider
+% The situation changes radically, however, if we consider
-\emph{higher-order} operations: programmable operations whose inputs
+% \emph{higher-order} operations: programmable operations whose inputs
-may themselves be programmable operations.  Here it turns out that
+% may themselves be programmable operations.  Here it turns out that
-both what is computable and the efficiency with which it can be
+% both what is computable and the efficiency with which it can be
-computed can be highly sensitive to the selection of language features
+% computed can be highly sensitive to the selection of language features
-present. This is in fact true more widely for \emph{abstract data
+% 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
+%   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
+% higher-order value will be represented within the machine as ground
-data, but a program within the language typically has no access to
+% data, but a program within the language typically has no access to
-this internal representation, and can interact with the value only by
+% this internal representation, and can interact with the value only by
-applying it to an argument.
+% 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
+The purpose of this chapter is to give a clear example of an essential
-inherent complexity difference higher up in the expressivity spectrum.
+complexity difference. Specifically, we will show that if we take a
-Specifically, we consider the following \emph{generic count} problem,
+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
+A \naive implementation strategy is simply to apply $P$ to each of the
-language, is simply to apply $P$ to each of the $2^n$ vectors in turn.
+$2^n$ vectors in turn.  However, one can do better with a curious
-A much less obvious, but still purely `functional', approach due to
+approach due to \citet{Berger90}, which achieves the effect of `pruned
-\citet{Berger90} achieves the effect of `pruned search' where the
+search' where the predicate allows it. This should be taken as a
-predicate allows it (serving as a warning that counter-intuitive
+warning that counter-intuitive phenomena can arise in this territory.
-phenomena can arise in this territory).  Nonetheless, under a mild
+Nonetheless, under the mild condition that $P$ must inspect all $n$
-condition on $P$ (namely that it must inspect all $n$ components of
+components of the given vector before returning, both these approaches
-the given vector before returning), both these approaches will have a
+will have a $\Omega(n 2^n)$ runtime.  Moreover, we shall show that in
-$\Omega(n 2^n)$ runtime.  Moreover, we shall show that in a typical
+$\BPCF$, a typical call-by-value language without advanced control
-call-by-value language without advanced control features, one cannot
+features, one cannot improve on this: \emph{any} implementation of
-improve on this: \emph{any} implementation of $\Count_n$ must
+$\Count_n$ must necessarily take time $\Omega(n2^n)$ on \emph{any}
-necessarily take time $\Omega(n2^n)$ on \emph{any} predicate $P$.  On
+predicate $P$.  Conversely, in the extended language $\HPCF$ it
-the other hand, if we extend our language with effect handlers, 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
+The key to enabling the speedup is \emph{backtracking} via multi-shot
-familiar, at least informally, to programmers who have worked with
+resumptions. The idea is to memorise the control state at each
-multi-shot continuations.
+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
+Concretely, suppose for example $n = 3$, and suppose that the predicate
-inspects the components of its argument in the order $0,1,2$.
+$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
+A \naive implementation of $\Count_3$ might start by applying the
-$P$ to $q_0 = (\True,\True,\True)$, and then to
+given predicate $P$ to $q_0 = (\True,\True,\True)$, and then to
-$q_1 = (\True,\True,\False)$.  Clearly there is some duplication here:
+$q_1 = (\True,\True,\False)$.  Note that there is some duplication
-the computations of $P\,q_0$ and $P\,q_1$ will proceed identically up
+here: the computations of $P\,q_0$ and $P\,q_1$ will proceed
-to the point where the value of the final component is requested. What
+identically up to the point where the value of the final component is
-we would like to do, then, is to record the state of the computation
+requested. Ideally, we would record the state of the computation of
-of $P\,q_0$ at just this point, so that we can later resume this
+$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
+order to obtain the value of $P\,q_1$.  Of course, a bespoke search
-internal nodes in the evident binary tree of boolean vectors.) Of
+function implementation would apply this backtracking behaviour in a
-course, this `backup' approach would be standardly applied if one were
+standard manner for some \emph{particular} choice of $P$ (e.g. the
-implementing a bespoke search operation for some \emph{particular}
+$n$-queens problem); but to apply this idea of resuming previous
-choice of $P$ (corresponding, say, to the $n$-queens problem); but to
+subcomputations in the \emph{generic} setting (i.e. uniformly in $P$)
-apply this idea of resuming previous subcomputations in the
+requires some special control feature such as effect handlers with
-\emph{generic} setting (that is, uniformly in $P$) requires some
+multi-shot resumptions.
-special language feature such as effect handlers or multi-shot
-continuations.
 %
-One could also obviate the need for such a feature by choosing to
+Obviously, one can remove the need a special control feature by a
-present the predicate $P$ in some other way, but from our present
+change of type for the predicate $P$, but this such a change shifts
-perspective this would be to move the goalposts: our intention is
+the perspective. The intention is precisely to show that the languages
-precisely to show that our languages differ in an essential way
+differ in an essential way as regards to their power to manipulate
-\emph{as regards their power to manipulate data of type} $(\Nat \to
+data of type $(\Nat \to \Bool) \to \Bool$.
-\Bool) \to \Bool$.
 
-This idea of using first-class control to achieve backtracking has
+The idea of using first-class control achieve backtracking is fairly
-been exploited before and is fairly widely known (see
+well-known in the literature~\cite{KiselyovSFA05}, and there is a
-e.g. \citep{KiselyovSFA05}), and there is a clear programming
+clear programming intuition that this yields a speedup unattainable in
-intuition that this yields a speedup unattainable in languages without
+languages without such control features.
-such control features.  % Our main contribution in this paper is to
+
+% 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.
+\begin{figure}
-{\noindent
   \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.
+% The value terms are standard.
-% Value terms comprise variables ($x$), the unit value ($\Unit$),
+Value terms comprise variables ($x$), the unit value ($\Unit$),
-% natural number literals ($n$), primitive constants ($c$), lambda
+natural number literals ($n$), primitive constants ($c$), lambda
-% abstraction ($\lambda x^A . \, M$), recursion
+abstraction ($\lambda x^A . \, M$), recursion
-% ($\Rec \; f^{A \to B}\, x.M$), pairs ($\Record{V, W}$), left
+($\Rec \; f^{A \to B}\, x.M$), pairs ($\Record{V, W}$), left
-% ($(\Inl~V)^B$) and right $((\Inr~W)^A)$ injections.
+($(\Inl~V)^B$) and right $((\Inr~W)^A)$ injections.
 
 %
-We will occasionally blur the distinction between object and meta
+% We will occasionally blur the distinction between object and meta
-language by writing $A$ for the meta level type of closed value terms
+% language by writing $A$ for the meta level type of closed value terms
-of type $A$.
+% 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