Change control into a computation form.

macros.tex

@@ -435,16 +435,22 @@
 \newcommand{\Catchcont}{\keyw{catchcont}}
 \newcommand{\Control}{\keyw{control}}
 \newcommand{\Prompt}{\#}
+\newcommand{\Controlz}{\keyw{control0}}
+\newcommand{\Promptz}{\#_0}
 \newcommand{\Escape}{\keyw{escape}}
 \newcommand{\shift}{\keyw{shift}}
+\newcommand{\shiftz}{\keyw{shift0}}
 \def\sigh#1{%
 \pmb{\left\langle\vphantom{#1}\right.}%
 #1%
 \pmb{\left.\vphantom{#1}\right\rangle}}
 \newcommand{\reset}[1]{\pmb{\langle} #1 \pmb{\rangle}}
+\newcommand{\resetz}[1]{\pmb{\langle} #1 \pmb{\rangle}_0}
 \newcommand{\fcontrol}{\keyw{fcontrol}}
 \newcommand{\fprompt}{\%}
 \newcommand{\splitter}{\keyw{splitter}}
+\newcommand{\abort}{\keyw{abort}}
+\newcommand{\calldc}{\keyw{calldc}}
 \newcommand{\J}{\keyw{J}}
 \newcommand{\JI}{\keyw{J}\,\keyw{I}}
 \newcommand{\FelleisenC}{\ensuremath{\keyw{C}}}

thesis.bib

@@ -2207,4 +2207,42 @@
   number    = {3},
   pages     = {348--375},
   year      = {1978}
+}
+
+# Substructural type system for shift0/reset0
+@inproceedings{KiselyovS07,
+  author    = {Oleg Kiselyov and
+               Chung{-}chieh Shan},
+  title     = {A Substructural Type System for Delimited Continuations},
+  booktitle = {{TLCA}},
+  series    = {Lecture Notes in Computer Science},
+  volume    = {4583},
+  pages     = {223--239},
+  publisher = {Springer},
+  year      = {2007}
+}
+
+# Exception handling with success continuations
+@article{BentonK01,
+  author    = {Nick Benton and
+               Andrew Kennedy},
+  title     = {Exceptional Syntax Journal of Functional Programming},
+  journal   = {J. Funct. Program.},
+  volume    = {11},
+  number    = {4},
+  pages     = {395--410},
+  year      = {2001}
+}
+
+# Typed multi prompts
+@article{DybvigJS07,
+  author    = {R. Kent Dybvig and
+               Simon L. Peyton Jones and
+               Amr Sabry},
+  title     = {A monadic framework for delimited continuations},
+  journal   = {J. Funct. Program.},
+  volume    = {17},
+  number    = {6},
+  pages     = {687--730},
+  year      = {2007}
 }

thesis.tex

@@ -1393,54 +1393,64 @@ connections to shell prompts, and how they act as barriers between the
 user and operating system.
 %
 
-A prompt is a computation form, whilst control is a value.
+In this presentation both control and prompt appear as computation
+forms.
 %
 \begin{syntax}
-    &V,W \in \ValCat  &::=& \cdots \mid \Control\\
+     &M,W \in \CompCat &::=& \cdots \mid \Control~k.M \mid \Prompt~M
-    &M,W \in \CompCat &::=& \cdots \mid \Prompt~M
 \end{syntax}
 %
-A prompt is written using the sharp ($\Prompt$) symbol. An application
+The $\Control~k.M$ expression reifies the context up to the nearest,
-of $\Control$ reifies the current continuation up to the nearest,
+dynamically determined, enclosing prompt and binds it to $k$ inside of
-dynamically determined, enclosing $\Prompt$.
+$M$. A prompt is written using the sharp ($\Prompt$) symbol.
 %
 The prompt remains in place after the reification, and thus any
 subsequent application of $\Control$ will be delimited by the same
 prompt.
 %
-\citeauthor{Felleisen88}'s original treatment of control and prompt
-was untyped. Typing them, particularly using a simple type system,
-affect their expressivity, because the type of the continuation object
-produced by $\Control$ must be compatible with the type of its nearest
-enclosing prompt -- this type is often called the \emph{answer} type
-(this terminology is adopted from typed continuation passing style
-transforms, where the codomain of every function is transformed to
-yield the type of whatever answer the entire program
-yields~\cite{MeyerW85}).
-%
-\dhil{Give intuition for why soundness requires the answer type to be fixed.}
-%
 
-In the static semantics we extend the typing judgement relation to
+The static semantics of control and prompt were absent in
-contain an up front fixed answer type $A$.
+\citeauthor{Felleisen88}'s original treatment.
 %
-\begin{mathpar}
+\dhil{Mention Yonezawa and Kameyama's type system.}
-  \inferrule*
+%
-    {\typ{\Gamma;A}{M : A}}
+\citet{DybvigJS07} gave a typed embedding of multi-prompts in
-    {\typ{\Gamma;A}{\Prompt~M : A}}
+Haskell. In the multi-prompt setting the prompts are named and an
+instance of $\Control$ is indexed by the prompt name of its designated
+delimiter.
 
-  \inferrule*
+% Typing them, particularly using a simple type system,
-    {~}
+% affect their expressivity, because the type of the continuation object
-    {\typ{\Gamma;A}{\Control : (\Cont\,\Record{A;A} \to A) \to A}}
+% produced by $\Control$ must be compatible with the type of its nearest
-\end{mathpar}
+% enclosing prompt -- this type is often called the \emph{answer} type
-%
+% (this terminology is adopted from typed continuation passing style
-A prompt has the same type as its computation constituent, which in
+% transforms, where the codomain of every function is transformed to
-turn must have the same type as fixed answer type.
+% yield the type of whatever answer the entire program
-%
+% yields~\cite{MeyerW85}).
-Similarly, the type of $\Control$ is governed by the fixed answer
+% %
-type. Discarding the answer type reveals that $\Control$ has the same
+% \dhil{Give intuition for why soundness requires the answer type to be fixed.}
-typing judgement as $\FelleisenF$.
+% %
-%
+
+% In the static semantics we extend the typing judgement relation to
+% contain an up front fixed answer type $A$.
+% %
+% \begin{mathpar}
+%   \inferrule*
+%     {\typ{\Gamma;A}{M : A}}
+%     {\typ{\Gamma;A}{\Prompt~M : A}}
+
+%   \inferrule*
+%     {~}
+%     {\typ{\Gamma;A}{\Control : (\Cont\,\Record{A;A} \to A) \to A}}
+% \end{mathpar}
+% %
+% A prompt has the same type as its computation constituent, which in
+% turn must have the same type as fixed answer type.
+% %
+% Similarly, the type of $\Control$ is governed by the fixed answer
+% type. Discarding the answer type reveals that $\Control$ has the same
+% typing judgement as $\FelleisenF$.
+% %
 
 The dynamic semantics for control and prompt consist of three rules:
 1) handle return through a prompt, 2) continuation capture, and 3)
@@ -1450,7 +1460,7 @@ continuation invocation.
   \slab{Value} &
      \Prompt~V &\reducesto& V\\
   \slab{Capture} &
-     \Prompt~\EC[\Control~V] &\reducesto& \Prompt~(V~\qq{\cont_{\EC}}), \text{ where $\EC$ contains no \Prompt}\\
+     \Prompt~\EC[\Control~k.M] &\reducesto& \Prompt~M[\qq{\cont_{\EC}}/k], \text{ where $\EC$ contains no \Prompt}\\
   \slab{Resume} & \Continue~\cont_{\EC}~V &\reducesto& \EC[V]
 \end{reductions}
 %
@@ -1473,13 +1483,11 @@ To illustrate $\Prompt$ and $\Control$ in action, let us consider a
 few simple examples.
 %
 \begin{derivation}
-  & 1 + \Prompt~2 + \Control\,(\lambda k.\Continue~k~(\Continue~k~0))\\
+  & 1 + \Prompt~2 + (\Control~k.\Continue~k~(\Continue~k~0))\\
   \reducesto^+& \reason{Capture $\EC = 2 + [\,]$}\\
-  & 1 + \Prompt~(\lambda k.\Continue~k~(\Continue~k~0))\,\cont_{2 + [\,]}\\
+  & 1 + \Prompt~\Continue~\cont_{\EC}~(\Continue~\cont_{\EC]}~0))\,\\
-  \reducesto  & \reason{$\beta$-reduction}\\
-  & 1 + \Prompt~\Continue~\cont_{2+[\,]}~(\Continue~\cont_{2 + [\,]}~0)\\
   \reducesto & \reason{Resume with 0}\\
-  & 1 + \Prompt~\Continue~\cont_{2+[\,]}~(2 + 0)\\
+  & 1 + \Prompt~\Continue~\cont_{\EC}~(2 + 0)\\
   \reducesto^+ & \reason{Resume with 2}\\
   & 1 + \Prompt~2 + 2\\
   \reducesto^+ & \reason{\slab{Value} rule}\\
@@ -1498,11 +1506,11 @@ $4$, which is (implicitly) supplied to the continuation of $\Prompt$.
 Let us consider a slight variation of the previous example.
 %
 \begin{derivation}
-  & 1 + \Prompt~2 + \Control\,(\lambda k.\Continue~k~0) + \Control\,(\lambda k'. 0)\\
+  & 1 + \Prompt~2 + (\Control~k.\Continue~k~0) + (\Control~k'. 0)\\
-  \reducesto^+& \reason{Capture $\EC = 2 + [\,] + \Control\,(\lambda 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\,(\lambda k'. 0)\\
+  & 1 + \Prompt~2 + 0 + (\Control~k'. 0)\\
   \reducesto^+ & \reason{Capture $\EC' = 2 + [\,]$}\\
   & 1 + \Prompt~0 \\
   \reducesto & \reason{\slab{Value} rule}\\
@@ -1584,9 +1592,11 @@ Answer type modification is a powerful feature that can be used to
 type embedded languages, an illustrious application of this is
 \citeauthor{Danvy98}'s typed $\dec{printf}$~\cite{Danvy98}. A
 polymorphic extension of answer type modification has been
-investigated by \citet{AsaiK07}, whilst \citet{KoboriKK16}
+investigated by \citet{AsaiK07}, \citet{KiselyovS07} developed a
-demonstrated how to translate from a source language with answer type
+substructural type system with answer type modification, whilst
-modification into a system without using typed multi-prompts.
+\citet{KoboriKK16} demonstrated how to translate from a source
+language with answer type modification into a system without using
+typed multi-prompts.
 
 Differences between shift/reset and control/prompt manifests in the
 dynamic semantics as well.
@@ -1647,13 +1657,128 @@ and state~\cite{Filinski94}.
 % \end{reductions}
 %
 
-\paragraph{\citeauthor{QueinnecS91}'s splitter}
+\paragraph{\citeauthor{QueinnecS91}'s splitter} The `splitter' control
+operator reconciles abortive undelimited control and composable
+delimited control. It was introduced by \citet{QueinnecS91} in
+1991. The name `splitter' is derived from it operational behaviour, as
+an application of `splitter' marks evaluation context in order for it
+to be split into two parts, where the context outside the mark
+represents the rest of computation, and the context inside the mark
+may be reified into a delimited continuation. The operator supports
+two operations `abort' and `calldc' to control the splitting of
+evaluation contexts. The former has the effect of escaping to the
+outer context, whilst the latter reifies the inner context as a
+delimited continuation (the operation name is short for ``call with
+delimited continuation'').
+
+Splitter and the two operations abort and calldc are value forms.
+%
+\[
+  V,W ::= \cdots \mid \splitter \mid \abort \mid \calldc
+\]
+%
+In their treatise of splitter, \citeauthor{QueinnecS91} gave three
+different presentations of splitter. The presentation that I have
+opted for here is close to their second presentation, which is in
+terms of multi-prompt continuations. This variation of splitter admits
+a pleasant static semantics too. Thus, we further extend the syntactic
+categories with the machinery for first-class prompts.
+%
+\begin{syntax}
+  & A,B &::=& \cdots \mid \prompttype~A \smallskip\\
+  & V,W &::=& \cdots \mid p\\
+  & M,N &::=& \cdots \mid \Prompt_V~M
+\end{syntax}
+%
+The type $\prompttype~A$ classifies prompts whose answer type is
+$A$. Prompt names are first-class values and denoted by $p$. The
+computation $\Prompt_V~M$ denotes a computation $M$ delimited by a
+parameterised prompt, whose value parameter $V$ is supposed to be a
+prompt name.
+%
+The static semantics of $\splitter$, $\abort$, and $\calldc$ are as
+follows.
+%
+\begin{mathpar}
+  \inferrule*
+  {~}
+  {\typ{\Gamma}{\splitter : (\prompttype~A \to A) \to A}}
+
+  \inferrule*
+  {~}
+  {\typ{\Gamma}{\abort : \prompttype~A \times (\UnitType \to A) \to B}}
+
+  \inferrule*
+  {~}
+  {\typ{\Gamma}{\calldc : \prompttype~A \times ((B \to A) \to B) \to B}}
+\end{mathpar}
+%
+In this presentation, the operator and the two operations all amount
+to special higher-order function symbols. The argument to $\splitter$
+is parameterised by a prompt name. This name is injected by
+$\splitter$ upon application. The operations $\abort$ and $\calldc$
+both accept as their first argument the name of the delimiting
+prompt. The second argument of $\abort$ is a thunk, whilst the second
+argument of $\calldc$ is a higher-order function, which accepts a
+continuation as its argument.
+
+For the sake of completeness the prompt primitives are typed as
+follows.
+%
+\begin{mathpar}
+  \inferrule*
+  {~}
+  {\typ{\Gamma,p:\prompttype~A}{p : \prompttype~A}}
+
+  \inferrule*
+  {\typ{\Gamma}{V : \prompttype~A} \\ \typ{\Gamma}{M : A}}
+  {\typ{\Gamma}{\Prompt_V~M : A}}
+\end{mathpar}
+%
+The dynamic semantics of this presentation require a bit of
+generativity in order to generate fresh prompt names. Therefore the
+reduction relation is extended with an additional component to keep
+track of which prompt names have already been allocated.
+%
 \begin{reductions}
-  \slab{Throw}   & \splitter~throw~calldc.\EC[\,throw~V] &\reducesto& V~\Unit\\
+  \slab{AppSplitter} & \splitter~V,\rho &\reducesto& \Prompt_p~V\,p,\rho \uplus \{p\}\\
-  \slab{Capture} &
+  \slab{Value}    & \Prompt_p~V,\rho &\reducesto& V,\rho\\
-     \splitter~throw~calldc.\EC[calldc~V] &\reducesto& V~\cont_{\EC} \\
+  \slab{Abort}    & \Prompt_p~\EC[\abort~\Record{p;V}],\rho &\reducesto& V\,\Unit,\rho,\quad \text{where $\EC$ contains no $\Prompt_p$}\\
-  \slab{Resume}  & \Continue~\cont_{\EC}~V &\reducesto& \EC[V]
+  \slab{Capture}  & \Prompt_p~\EC[\calldc~V] &\reducesto& V~\qq{\cont_{\EC}},\rho\\
+  \slab{Resume}   & \Continue~\cont_{\EC}~V,\rho &\reducesto& \EC[V],\rho
 \end{reductions}
+%
+We see by the $\slab{AppSplitter}$ rule that an application of
+$\splitter$ generates a fresh named prompt, whose name is applied on
+the function argument.
+%
+The $\slab{Value}$ rule is completely standard.
+%
+The $\slab{Abort}$ rule show that an invocation of $\abort$ causes the
+current evaluation context $\EC$ up to and including the nearest
+enclosing prompt.
+%
+The next rule $\slab{Capture}$ show that $\calldc$ captures and aborts
+the context up to the nearest enclosing prompt. The captured context
+is applied on the function argument of $\calldc$. As part of the
+operation the prompt is removed. % Thus, $\calldc$ behaves as a
+% delimited variation of $\Callcc$.
+%
+
+It is clear by the prompt semantics that invocation of either $\abort$
+and $\calldc$ is only well-defined within the dynamic extent of
+$\splitter$. Since the prompt is eliminated after use of either
+operation subsequent operation invocations must be guarded by a new
+instance of $\splitter$.
+%
+\dhil{Show an example}
+% \begin{reductions}
+%   \slab{Value}   & \splitter~abort~calldc.V &\reducesto& V\\
+%   \slab{Throw}   & \splitter~abort~calldc.\EC[\,abort~V] &\reducesto& V~\Unit\\
+%   \slab{Capture} &
+%      \splitter~abort~calldc.\EC[calldc~V] &\reducesto& V~\qq{\cont_{\EC}} \\
+%   \slab{Resume}  & \Continue~\cont_{\EC}~V &\reducesto& \EC[V]
+% \end{reductions}
 
 
 \paragraph{Spawn}
@@ -1799,51 +1924,155 @@ captured context $\EC$ with the argument $V$ plugged in.
 %
 \dhil{Show some example of use\dots}
 
-\paragraph{\citeauthor{PlotkinP09}'s effect handlers} Effect handlers
+\paragraph{\citeauthor{PlotkinP09}'s effect handlers} In 2009,
-were introduced by \citet{PlotkinP09} in 2009.
+\citet{PlotkinP09} introduced handlers for \citeauthor{PlotkinP01}'s
+algebraic effects~\cite{PlotkinP01,PlotkinP03,PlotkinP13}. In contrast
+to the previous control operators, the mathematical foundations of
+handlers were not an afterthought, rather, their origin is deeply
+rooted in mathematics. Nevertheless, they turn out to provide a
+pragmatic interface for programming with control. Operationally,
+effect handlers can be viewed as a small extension to exception
+handlers, where exceptions are resumable. Effect handlers are similar
+to fcontrol in that handling of control happens at the delimiter and
+not at the point of control capture. Unlike fcontrol, the interface of
+effect handlers provide a mechanism for handling the return value of a
+computation similar to \citeauthor{BentonK01}'s exception handlers
+with success continuations~\cite{BentonK01}.
+
+Effect handler definitions occupy their own syntactic category.
+%
+\begin{syntax}
+  &A,B \in \ValTypeCat &::=& \cdots \mid A \Harrow B \smallskip\\
+  &H   \in \HandlerCat &::=&  \{ \Return \; x \mapsto M \}
+                        \mid \{ \OpCase{\ell}{p}{k} \mapsto N \} \uplus H\\
+\end{syntax}
+%
+A handler consists of a $\Return$-clause and zero or more operation
+clauses.
+%
+\begin{syntax}
+  &\Sigma \in \mathsf{Sig} &::=& \emptyset \mid \{ \ell : A \opto B \} \uplus \Sigma\\
+  &A,B,C,D \in \ValTypeCat &::=& \cdots \mid A \opto B \smallskip\\
+  &M,N \in \CompCat    &::=& \cdots \mid \Do\;\ell\,V \mid \Handle \; M \; \With \; H\\[1ex]
+\end{syntax}
+%
+\begin{mathpar}
+  \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}
 %
 \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,\cont_{\Record{\EC;H}}/k],\\
+  \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}\\
   \slab{Resume}   & \Continue~\cont_{\Record{\EC;H}}~V &\reducesto& \Handle\;\EC[V]\;\With\;H\\
 \end{reductions}
 %
+The \slab{Value} rule differs from previous operators as it is not
+just the identity. Instead the $\Return$-clause of the handler
+definition is applied to the return value of the computation.
+%
+The \slab{Capture} rule handles operation invocation by checking
+whether the handler $H$ handles the operation $\ell$, otherwise the
+operation implicitly passes through the term to the context outside
+the handler. This behaviour is similar to how exceptions pass through
+the context until a suitable handler has been found.
+%
+If $H$ handles $\ell$, then the context $\EC$ from the operation
+invocation up to and including the handler $H$ are reified as a
+continuation object, which gets bound in the corresponding clause for
+$\ell$ in $H$ along with the payload of $\ell$.
+%
+This form of effect handlers is known as \emph{deep} handlers. They
+are deep in the sense that they embody a structural recursion scheme
+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.
+%
+
+The alternative to deep handlers is known as \emph{shallow}
+handlers. They do not embody a particular recursion scheme, rather,
+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\;-$.
+%
+\begin{mathpar}
+%\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 C;\Sigma}{N_i : D}]_i
+    }
+    {\typ{\Gamma;\Sigma}{H : C \Harrow D}}
+\end{mathpar}
+%
 \begin{reductions}
-  \slab{Capture}  & \Handle\;\EC[\Do\;\ell~V] \;\With\; H &\reducesto& M[V/p,\cont_{\EC}/k],\\
+  \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}
 %
 
-Deep handlers can be used to simulate shift and reset.
+Deep handlers can be used to simulate shift0 and reset0.
 %
 \begin{equations}
-  \sembr{\shift} &\defas& \lambda f. \Do\;\shift~f\\
+  \sembr{\shiftz~k.M} &\defas& \Do\;\dec{Shift0}~(\lambda k.M)\\
-  \sembr{\reset{M}} &\defas&
+  \sembr{\resetz{M}} &\defas&
               \ba[t]{@{~}l}\Handle\;m\,\Unit\;\With\\
                   ~\ba{@{~}l@{~}c@{~}l}
                       \Return\;x &\mapsto& x\\
-                      \OpCase{\dec{Shift}}{f}{k} &\mapsto& f\,(\lambda x. \Continue~k~x)
+                      \OpCase{\dec{Shift0}}{f}{k} &\mapsto& f\,(\lambda x. \Continue~k~x)
                    \ea
               \ea
 \end{equations}
 %
 
-Shallow handlers can be used to simulate prompt and control.
+Shallow handlers can be used to simulate control0 and prompt0.
 %
 \begin{equations}
-  \sembr{\Control} &\defas& \lambda f. \Do\;\dec{Control}~f\\
+  \sembr{\Controlz~k.M} &\defas& \Do\;\dec{Control0}~(\lambda k.M)\\
-  \sembr{\Prompt~M} &\defas&
+  \sembr{\Promptz~M} &\defas&
      \bl
-       prompt\,(\lambda\Unit.M)\\
+       prompt0\,(\lambda\Unit.M)\\
        \textbf{where}\;
          \bl
-            prompt~m \defas
+            prompt0~m \defas
               \ba[t]{@{~}l}\ShallowHandle\;m\,\Unit\;\With\\
                   ~\ba{@{~}l@{~}c@{~}l}
                       \Return\;x &\mapsto& x\\
-                      \OpCase{\dec{Control}}{f}{k} &\mapsto& prompt\,(\lambda\Unit.f\,(\lambda x. \Continue~k~x))
+                      \OpCase{\dec{Control0}}{f}{k} &\mapsto& prompt0\,(\lambda\Unit.f\,(\lambda x. \Continue~k~x))
                    \ea
               \ea
           \el
@@ -1880,9 +2109,20 @@ programs~\cite{Knuth97}. Canonical reference for implementing
 coroutines with call/cc~\cite{HaynesFW86}.
 
 \section{Programming continuations}
-Blind vs non-blind backtracking. Engines. Web
+%Blind vs non-blind backtracking. Engines. Web
-programming. Asynchronous
+% programming. Asynchronous
-programming. Coroutines. Meta-programming~\cite{LawallD94,KameyamaKS11,OishiK17,Yallop17}.
+% programming. Coroutines.
+
+Amongst the first uses of continuations were modelling of unrestricted
+jumps, such as \citeauthor{Landin98}'s modelling of \Algol{} labels
+and gotos using the J
+operator~\cite{Landin65,Landin65a,Landin98,Reynolds93}.
+
+Backtracking is another early and prominent use of
+continuations. \citet{Burstall69} used the J operator to implement a
+backtracking mechanism to facilitate tree-based search.
+
+Meta-programming~\cite{LawallD94,KameyamaKS11,OishiK17,Yallop17}.
 
 \section{Constraining continuations}
 For example callec is a variation of callcc where the continuation