Progress on undelimited control.

macros.tex

@@ -16,6 +16,7 @@
 \newcommand{\CC}{\keyw{C}}
 % \newcommand{\Delim}[1]{\ensuremath{\langle\!\!\mkern-1.5mu\langle#1\rangle\!\!\mkern-1.5mu\rangle}}
 \newcommand{\Delim}[1]{\ensuremath{\langle#1\rangle}}
+\newcommand{\sembr}[1]{\ensuremath{\llbracket #1 \rrbracket}}
 
 %%
 %% Partiality
@@ -443,3 +444,4 @@
 \newcommand{\FelleisenF}{\ensuremath{\mathcal{F}}}
 \newcommand{\cont}{\keyw{cont}}
 \newcommand{\Cont}{\dec{Cont}}
+\newcommand{\Algol}{Algol~60}

thesis.bib

@@ -1295,7 +1295,10 @@
   volume    = {11},
   number    = {4},
   pages     = {363--397},
-  year      = {1998}
+  year      = {1998},
+  note      = {This paper originally appeared in the Proceedings of
+               the ACM National Conference, volume 2, August, 1972,
+               pages 717–740.}
 }
 
 # Shift/reset

thesis.tex

@@ -650,8 +650,8 @@ continuations, composable continuations.
 Downward and upward use of continuations.
 
 \section{First-class control operators}
-Describe how effect handlers fit amongst shift/reset, prompt/control,
+Table~\ref{tbl:classify-ctrl} provides a classification of a
-callcc, J, catchcont, etc.
+non-exhaustive list of first-class control operators.
 
 \begin{table}
   \centering
@@ -694,48 +694,23 @@ callcc, J, catchcont, etc.
 \end{table}
 
 \subsection{Undelimited operators}
+%
+The J operator was unveiled by Peter Landin in 1965~\cite{Landin98},
+making it the \emph{first} first-class control operator. A while after
+John \citeauthor{Reynolds98a} invented the escape operator which was
+influenced by the J operator~\cite{Reynolds98a}. Then came
+\citeauthor{SussmanS75}'s catch operator, and thereafter callcc
+appeared. Later another batch of control operators based on callcc
+appeared. However, common for all of the early operators is that their
+captured continuations have undelimited extent and exhibit abortive
+behaviour. Moreover, save for Landin's J operator they all capture the
+current continuation. Interestingly the three operators escape, catch,
+and callcc turned out to be essentially the same operator.
 
-\paragraph{Landin's J operator}
+\paragraph{Reynolds' escape} The escape operator was introduced by
-%
+\citeauthor{Reynolds98a} in 1972~\cite{Reynolds98a} to make
-\begin{mathpar}
+statement-oriented control mechanisms such as jumps and labels
-  \inferrule*
+programmable in an expression-oriented language.
-    {\typ{\Gamma,x:A;B \cons \Delta}{M : B}}
-    {\typ{\Gamma;\Delta}{\lambda x.M : A \to B}}
-
-  \inferrule*
-    {\typ{\Gamma;B \cons \Delta}{\lambda x. M : A \to B}}
-    {\typ{\Gamma;B \cons \Delta}{\J\,(\lambda x.M) : \Cont\,\Record{A;B}}}
-
-  \inferrule*
-    {\typ{\Gamma;\Delta}{V : A} \\ \typ{\Gamma;\Delta}{W : \Cont\,\Record{A;B}}}
-    {\typ{\Gamma;\Delta}{\Continue~W~V : B}}
-\end{mathpar}
-%
-\begin{reductions}
-  \slab{Dump}   & \EC[(\lambda x.M)~V] &\reducesto& \EC[\mathcal{D}[M[V/x]]]\\
-  \slab{Capture}   & \EC[\mathcal{D}[\J\,(\lambda x.M)]] &\reducesto& \EC[\mathcal{D}[\cont_{\Record{\EC;\lambda x.M}}]]\\
-  \slab{Resume}    & \EC[\Continue~\cont_{\Record{\EC';\lambda x.M}}~V]  &\reducesto& \EC'[(\lambda x.M)~V]
-\end{reductions}
-%
-
-\paragraph{Sussman and Steele's catch}
-%
-\begin{mathpar}
-  \inferrule*
-    {\typ{\Gamma,k : \Cont\,\Record{A;\Zero}}{M : A}}
-    {\typ{\Gamma}{\Catch~k.M : A}}
-
-  \inferrule*
-    {\typ{\Gamma}{V : A} \\ \typ{\Gamma}{W : \Cont\,\Record{A;\Zero}}}
-    {\typ{\Gamma}{\Continue~W~V : \Zero}}
-\end{mathpar}
-%
-\begin{reductions}
-  \slab{Capture} &  \EC[\Catch~k.M] &\reducesto& \EC[M[\cont_{\EC}/k]]\\
-  \slab{Resume}  &  \EC[\Continue~\cont_{\EC'}~V]  &\reducesto& \EC'[V]
-\end{reductions}
-%
-\paragraph{Reynolds' escape}
 %
 \begin{mathpar}
   \inferrule*
@@ -753,6 +728,32 @@ callcc, J, catchcont, etc.
 \end{reductions}
 %
 
+\paragraph{Sussman and Steele's catch}
+%
+The catch operator was introduced into the programming language Scheme
+by \citeauthor{SussmanS75} in 1975 as a mechanism for performing
+non-local exits~\cite{SussmanS75}.
+%
+\[
+  M,N ::= \cdots \mid \Catch~k.M
+\]
+%
+\begin{mathpar}
+  \inferrule*
+    {\typ{\Gamma,k : \Cont\,\Record{A;\Zero}}{M : A}}
+    {\typ{\Gamma}{\Catch~k.M : A}}
+
+  \inferrule*
+    {\typ{\Gamma}{V : A} \\ \typ{\Gamma}{W : \Cont\,\Record{A;\Zero}}}
+    {\typ{\Gamma}{\Continue~W~V : \Zero}}
+\end{mathpar}
+%
+\begin{reductions}
+  \slab{Capture} &  \EC[\Catch~k.M] &\reducesto& \EC[M[\cont_{\EC}/k]]\\
+  \slab{Resume}  &  \EC[\Continue~\cont_{\EC'}~V]  &\reducesto& \EC'[V]
+\end{reductions}
+%
+
 \paragraph{Call-with-current-continuation}
 %
 \begin{mathpar}
@@ -833,6 +834,118 @@ Contrast this result with
   \slab{Resume}  &  \Continue~\cont_{\EC}~V  &\reducesto& \EC[V]
 \end{reductions}
 
+\paragraph{Landin's J operator}
+%
+The J operator was introduced by Peter Landin in 1965 (making it the
+world's \emph{first} first-class control operator) as a means for
+translating jumps and labels in the statement-oriented language
+\Algol{} into an expression-oriented
+language~\cite{Landin65,Landin65a,Landin98}. Landin used the J
+operator to account for the meaning of \Algol{} labels.
+%
+The following example due to \citet{DanvyM08} provides a flavour of
+the correspondence between labels and J.
+%
+\[
+  \ba{@{}l@{~}l}
+    &\sembr{\keyw{begin}\;s_1;\;\keyw{goto}\;L;\;L:\,s_2\;\keyw{end}}\\
+    =& \lambda\Unit.\Let\;L \revto \J\,\sembr{s_2}\;\In\;\Let\;\Unit \revto \sembr{s_1}\,\Unit\;\In\;L\,\Unit
+  \ea
+\]
+%
+Here $\sembr{-}$ denotes the translation of statements. In the image,
+the label $L$ manifests as an application of $\J$ and the
+$\keyw{goto}$ manifests as an application of continuation captured by
+$\J$.
+%
+The operator extends the syntactic category of computations with a new
+form.
+%
+\[
+  M,N \in \CompCat ::= \cdots \mid \J\,W
+\]
+%
+The previous example hints at the fact that the J operator is quite
+different to the previously considered undelimited control operators
+in that the captured continuation is \emph{not} the current
+continuation, but rather, the continuation of the caller.
+%
+To this effect, the continuation object produced by a $\J$ application
+may be thought of as a first-class variation of the return statement
+commonly found in statement-oriented languages. Since it is a
+first-class object it can be passed to another function, meaning that
+any function can endow other functions with the ability to return from
+it, e.g.
+%
+\[
+  \dec{f} \defas \lambda g. \Let\;return \revto \J\,(\lambda x.x) \;\In\; g~return;~\True
+\]
+%
+If the function $g$ does not invoke its argument, then $\dec{f}$
+returns $\True$, e.g.
+\[
+  \dec{f}~(\lambda return.\False) \reducesto^+ \True
+\]
+%
+However, if $g$ does apply its argument, then the value provided to
+the application becomes the return value of $\dec{f}$, e.g.
+%
+\[
+  \dec{f}~(\lambda return.return~\False) \reducesto^+ \False
+\]
+%
+The function argument provided to $\J$ can intuitively be thought of
+as the expression attached to a return statement in a
+statement-oriented language.
+%
+
+Clearly, the return type of a continuation produced by an $\J$
+application must be the same as the caller of $\J$. Therefore to track
+the caller type we make use of an additional ordered context
+$\Delta$. This context is extended by the typing rule for
+$\lambda$-abstraction, and its contents are used by the typing rule
+for $\J$-applications.
+%
+\begin{mathpar}
+  \inferrule*
+    {\typ{\Gamma,x:A;B \cons \Delta}{M : B}}
+    {\typ{\Gamma;\Delta}{\lambda x.M : A \to B}}
+
+  \inferrule*
+    {\typ{\Gamma;B \cons \Delta}{W : A \to B}}
+    {\typ{\Gamma;B \cons \Delta}{\J\,W : \Cont\,\Record{A;B}}}
+
+  \inferrule*
+    {\typ{\Gamma;\Delta}{V : A} \\ \typ{\Gamma;\Delta}{W : \Cont\,\Record{A;B}}}
+    {\typ{\Gamma;\Delta}{\Continue~W~V : B}}
+\end{mathpar}
+%
+Any meaningful applications of $\J$ must appear under a
+$\lambda$-abstraction, because the application captures its caller's
+continuation. In order to capture the caller's continuation we
+annotate the evaluation contexts for ordinary applications.
+%
+\begin{reductions}
+  \slab{Annotate}   & \EC[(\lambda x.M)\,V] &\reducesto& \EC_\lambda[M[V/x]]\\
+  \slab{Capture}   & \EC_{\lambda}[\mathcal{D}[\J\,W]] &\reducesto& \EC_{\lambda}[\mathcal{D}[\cont_{\Record{\EC_{\lambda};W}}]]\\
+  \slab{Resume}    & \EC[\Continue~\cont_{\Record{\EC';W}}\,V]  &\reducesto& \EC'[W\,V]
+\end{reductions}
+%
+$\slab{Capture}$ rule only applies if the application of $\J$ takes
+place in annotated evaluation context. The continuation object
+produced by a $\J$ application encompasses the caller's continuation
+$\EC_\lambda$ and the value argument $W$.
+%
+This continuation object may be invoked in \emph{any} context. An
+invocation discards the current continuation $\EC$ and installs $\EC'$
+instead with the $\J$-argument $W$ applied to the value $V$.
+
+Let us end by remarking that the J operator is expressive enough to
+encode a familiar control operator like $\Callcc$.
+\[
+  \Callcc \defas \lambda f. f\,(\J\,(\lambda x.x))
+\]
+
 \subsection{Delimited operators}
 Delimited control: Control delimiters form the basis for delimited
 control. \citeauthor{Felleisen88} introduced control delimiters in
@@ -916,8 +1029,8 @@ undelimited control~\cite{Filinski94}
   \slab{Value} &
      \Catchcont \; f . \Record{V;W} &\reducesto& \Inl\; \Record{V;\lambda\,f. W}\\
   \slab{Capture} &
-     \Catchcont \; f .\EC[\,f\,V]   &\reducesto& \Inr\; \Record{V; \cont_{\Record{\EC;\,f}}}\\
+     \Catchcont \; f .\EC[\,f\,V]   &\reducesto& \Inr\; \Record{V; \lambda x. \lambda f. \Continue~\cont_{\EC}~x}\\
-  \slab{Resume} & \Continue~\cont_{\Record{\EC;\,f}}~V &\reducesto& \lambda f.\EC[V]
+  \slab{Resume} & \Continue~\cont_{\EC}~V &\reducesto& \EC[V]
 \end{reductions}
 
 \paragraph{Shift/reset}
@@ -949,7 +1062,7 @@ undelimited control~\cite{Filinski94}
 
 \paragraph{Spawn/controller}
 
-\section{Second-class control operators}
+\subsection{Second-class control operators}
 Coroutines, async/await, generators/iterators, amb.
 
 Backtracking: Amb~\cite{McCarthy63}.
@@ -960,6 +1073,11 @@ Conway, who used coroutines as a code idiom in assembly
 programs~\cite{Knuth97}. Canonical reference for implementing
 coroutines with call/cc~\cite{HaynesFW86}.
 
+\section{Constraining continuations}
+For example callec is a variation of callcc where the continuation
+only can be invoked during the dynamic extent of
+callec~\cite{Flatt20}.
+
 \section{Implementation strategies for first-class control}
 Table~\ref{tbl:ctrl-operators-impls} lists some programming languages
 with support for first-class control operators and their