Composable continuations. Controlling continuations intro.

thesis.tex

@@ -642,22 +642,9 @@ will classify them by their operational behaviour.
 The extent and behaviour of a continuation in programming are
 determined by its introduction and elimination forms,
 respectively. Programmatically, a continuation is introduced via a
-control operator, which typically reifies the control state as a
+control operator, which reifies the control state as a first-class
-first-class object, e.g. a function. A continuation is eliminated via
+object, e.g. a function, that can be eliminated via some form of
 application.
-%
-
-%
-% If the continuation is reified as a function, then the elimination
-% form coincides with ordinary function application. This is convenient
-% in practice for programming with continuations, but it is inconvenient
-% for formal examination. In order to examine and understand the
-% phenomenon it is generally a good idea to treat the phenomenon
-% specially. Therefore, our abstract control operator will reify the
-% control state as a value $\cont_{\EC}$, which is indexed by the
-% reified evaluation context $\EC$ to make notionally convenient to
-% reflect the context again. We will write $\Continue~\cont_{\EC}~W$ to
-% denote application of a $\cont$ object to the value $W$.
 
 \subsection{Introduction of continuations}
 %
@@ -684,10 +671,11 @@ computation $M$.
 continuation is indefinite as it ranges over the entire remainder of
 computation.
 %
-The most common undelimited continuation is the \emph{current}
+In functional programming languages undelimted control operators most
-continuation, which is the precisely continuation following the
+commonly expose the \emph{current} continuation, which is the
-control operator. The following is the characteristic reduction for
+precisely continuation following the control operator. The following
-the introduction of the current continuation.
+is the characteristic reduction for the introduction of the current
+continuation.
 % The indefinite extents means that undelimited continuation capture can
 % only be understood in context. The characteristic reduction is as
 % follows.
@@ -716,16 +704,17 @@ reification. Now, the programmer has control over the whole
 continuation, since it is entirely up to the programmer whether $\EC$
 gets evaluated.
 
-An alternative to reify the current continuation is to reify the
+Imperative statement-oriented programming languages commonly expose
-caller continuation. The caller continuation is the continuation of
+the \emph{caller} continuation, typically via a return statement. The
-the invocation context of the control operator. Characterising
+caller continuation is the continuation of the invocation context of
-undelimited caller continuations is slightly more involved as we have
+the control operator. Characterising undelimited caller continuations
-to remember the continuation of the invocation context. We will use a
+is slightly more involved as we have to remember the continuation of
-bold lambda $\llambda$ as a syntactic runtime marker to remember the
+the invocation context. We will use a bold lambda $\llambda$ as a
-continuation of an application. In addition we need three reduction
+syntactic runtime marker to remember the continuation of an
-rules, where the first is purely administrative, the second is an
+application. In addition we need three reduction rules, where the
-extension of regular application, and the third is the characteristic
+first is purely administrative, the second is an extension of regular
-reduction rule for undelimited control with caller continuations.
+application, and the third is the characteristic reduction rule for
+undelimited control with caller continuations.
 %
 \begin{reductions}
   & \llambda.V       &\reducesto& V\\
@@ -774,11 +763,11 @@ then continues as $M$ under the control delimiter. Note that the
 continuation of $\keyw{del}$ is invisible to $\CC$, and thus, the
 behaviour of $\CC$ can be understood locally.
 
-There are multiple design choices for delimited control operators. The
+The design space of delimited control is somewhat richer than that of
-control delimiter may remain in place after reification, as above, or
+undelimited control, as the control delimiter may remain in place
-be discarded. Similarly, the control reifier may reify the
+after reification, as above, or be discarded. Similarly, the control
-continuation up to and including the delimiter or, as above, without
+reifier may reify the continuation up to and including the delimiter
-the delimiter.
+or, as above, without the delimiter.
 %
 The most common variation of delimited control in the literature is
 abortive and reifies the current continuation up to, but not including
@@ -792,6 +781,90 @@ In the literature a delimited continuation is also known as a
 
 \subsection{Elimination of continuations}
 
+The purpose of continuation application is to reinstall the captured
+context.
+%
+However, a continuation application may affect the control state in
+various ways. The literature features two distinct behaviours of
+continuation application: abortive and composable. We need some
+notation for application of continuations in order to characterise
+abortive and composable behaviours. We will write
+$\Continue~\cont_{\EC}~V$ to denote the application of some
+continuation object $\cont$ to some value $V$.
+
+\paragraph{Abortive continuation} Upon invocation an abortive
+continuation discards the entire evaluation context before
+reinstalling the captured context. In other words, an abortive
+continuation replaces the current context with its captured context,
+i.e.
+%
+\[
+  \EC[\Continue~\cont_{\EC'}~V] \reducesto \EC'[V]
+\]
+%
+The current context $\EC$ is discarded in favour of the captured
+context $\EC'$ (whether the two contexts coincide depends on the
+control operator).  Abortive continuations are a global phenomenon due
+to their effect on the current context. However, in conjunction with a
+control delimiter the behaviour of an abortive continuation can be
+localised, i.e.
+%
+\[
+  \Delim{\EC[\Continue~\cont_{\EC'}~V]} \reducesto \EC'[V]
+\]
+%
+Here, the behaviour of continuation does not interfere with the
+context of $\keyw{del}$, and thus, the behaviour can be understood and
+reasoned about locally with respect to $\keyw{del}$.
+
+A key characteristic of an abortive continuation is that composition
+is meaningless. For example, composing an abortive continuation with
+itself have no effect.
+%
+\[
+  \EC[\Continue~\cont_{\EC'}~(\Continue~\cont_{\EC'}~V)] \reducesto \EC'[V]
+\]
+%
+The innermost application erases the outermost application term,
+consequently only the first application of $\cont$ occurs during
+runtime. It is as if the first application occurred in tail position.
+
+The continuations introduced by the early control operators were all
+abortive, since they were motivated by modelling unrestricted jumps
+akin to $\keyw{goto}$ in statement-oriented programming languages.
+
+An abortive continuation is also known as an `escape' continuation in
+the literature.
+
+\paragraph{Composable continuation} A composable continuation splices
+its captured context with the its invocation context, i.e.
+%
+\[
+  \Continue~\cont_{\EC}~V \reducesto \EC[V]
+\]
+%
+The application of a composable continuation can be understood
+locally, because it has no effect on its invocation context. A
+composable continuation behaves like a function in the sense that it
+returns to its caller, and thus composition is well-defined, e.g.
+%
+\[
+  \Continue~\cont_{\EC}~(\Continue~\cont_{\EC}~V) \reducesto \Continue~\cont_{\EC}~\EC[V]
+\]
+%
+The innermost application composes the captured context with the
+outermost application. Thus, the outermost application occurs when
+$\EC[V]$ has been reduced to a value.
+
+In the literature, virtually every delimited control operator provides
+composable continuations. However, the notion of composable
+continuation is not intimately connected to delimited control. It is
+perfect possible to conceive of a undelimited composable continuation,
+just as a delimited abortive continuation is conceivable.
+
+A composable continuation is also known as a `functional' continuation
+in the literature.
+
 % % \citeauthor{Reynolds93} has written a historical account of the
 % % various early discoveries of continuations~\cite{Reynolds93}.
 
@@ -841,66 +914,75 @@ In the literature a delimited continuation is also known as a
 % operation, i.e.  $\Delim{V} \reducesto V$. I will write $\EC$ to
 % denote an evaluation context~\cite{Felleisen87}.
 
-\paragraph{Undelimited continuation}
+% \paragraph{Undelimited continuation}
-%
+% %
-\[
+% \[
-  \EC[\CC\,k.M] \reducesto \EC[M[(\lambda x.\EC[x])/k]]
+%   \EC[\CC\,k.M] \reducesto \EC[M[(\lambda x.\EC[x])/k]]
-\]
+% \]
-%
+% %
-\begin{derivation}
+% \begin{derivation}
-  & 3 * (\CC\,k. 2 + k\,(k\,1))\\
+%   & 3 * (\CC\,k. 2 + k\,(k\,1))\\
-  \reducesto& \reason{captures the context $k = 3 * [~]$}\\
+%   \reducesto& \reason{captures the context $k = 3 * [~]$}\\
-  & 3 * (2 + k\,(k~1))[(\lambda x. 3 * x)/k]\\
+%   & 3 * (2 + k\,(k~1))[(\lambda x. 3 * x)/k]\\
-  =& \reason{substitution}\\
+%   =& \reason{substitution}\\
-  & 3 * (2 + (\lambda x. 3 * x)((\lambda x. 3 * x)\,1))\\
+%   & 3 * (2 + (\lambda x. 3 * x)((\lambda x. 3 * x)\,1))\\
-  \reducesto& \reason{$\beta$-reduction}\\
+%   \reducesto& \reason{$\beta$-reduction}\\
-  & 3 * (2 + (\lambda x. 3 * x)(3 * 1))\\
+%   & 3 * (2 + (\lambda x. 3 * x)(3 * 1))\\
-  \reducesto& \reason{$\beta$-reduction}\\
+%   \reducesto& \reason{$\beta$-reduction}\\
-  & 3 * (2 + (\lambda x. 3 * x)\,3)\\
+%   & 3 * (2 + (\lambda x. 3 * x)\,3)\\
-  \reducesto^4& \reason{$\beta$-reductions}\\
+%   \reducesto^4& \reason{$\beta$-reductions}\\
-  & 33
+%   & 33
-\end{derivation}
+% \end{derivation}
 
-\paragraph{Delimited continuation}
+% \paragraph{Delimited continuation}
-%
+% %
-\[
+% \[
-  \Delim{\EC[\CC\,k.M]} \reducesto \Delim{M[(\lambda x.\Delim{\EC[x]})/k]}
+%   \Delim{\EC[\CC\,k.M]} \reducesto \Delim{M[(\lambda x.\Delim{\EC[x]})/k]}
-\]
+% \]
-%
+% %
-\[
+% \[
-  \Delim{\EC[\CC\,k.M]} \reducesto M[(\lambda x.\Delim{\EC[x]})/k]
+%   \Delim{\EC[\CC\,k.M]} \reducesto M[(\lambda x.\Delim{\EC[x]})/k]
-\]
+% \]
 
-\paragraph{Abortive continuation} An abortive continuation discards the current context.Like delimited continuations, an
+% \paragraph{Abortive continuation} An abortive continuation discards the current context.Like delimited continuations, an
-abortive continuation is accompanied by a delimiter. The
+% abortive continuation is accompanied by a delimiter. The
-characteristic property of an abortive continuation is that it
+% characteristic property of an abortive continuation is that it
-discards its invocation context up to its enclosing delimiter.
+% discards its invocation context up to its enclosing delimiter.
-%
+% %
-\[
+% \[
-  \EC[k\,V] \reducesto V, \quad \text{where } k = (\lambda x. \keyw{abort}\;x).
+%   \EC[k\,V] \reducesto V, \quad \text{where } k = (\lambda x. \keyw{abort}\;x).
-\]
+% \]
-%
+% %
-Consequently, composing an abortive continuation with itself is
+% Consequently, composing an abortive continuation with itself is
-meaningless, e.g. in $k (k\,V)$ the innermost application erases the
+% meaningless, e.g. in $k (k\,V)$ the innermost application erases the
-outermost application.
+% outermost application.
 
-\paragraph{Composable continuation} The defining characteristic of a
+% \paragraph{Composable continuation} The defining characteristic of a
-composable continuation is that it composes the captured context with
+% composable continuation is that it composes the captured context with
-current context, i.e.
+% current context, i.e.
-%
+% %
-\[
+% \[
-  \EC[k\,V] \reducesto \EC[\EC'[V]], \quad \text{where } k = (\lambda x. \EC'[x])
+%   \EC[k\,V] \reducesto \EC[\EC'[V]], \quad \text{where } k = (\lambda x. \EC'[x])
-\]
+% \]
 
-Escape continuations, undelimited continuations, delimited
+% Escape continuations, undelimited continuations, delimited
-continuations, composable continuations.
+% continuations, composable continuations.
 
-Downward and upward use of continuations.
+% Downward and upward use of continuations.
 
 \section{Controlling continuations}
 \label{sec:controlling-continuations}
+As suggested in the previous section, the design space for
+continuation is rich. This richness is to an extent reflected by the
+considerable amount of control operators that appear in the literature
+and in practice.
+%
 Table~\ref{tbl:classify-ctrl} provides a classification of a
 non-exhaustive list of first-class control operators.
+
+It is worth remarking that a \emph{first-class} control operator is
+typically not itself a first-class citizen, rather, it means that the
+reified continuation is a first-class citizen.
 %
 \begin{table}
   \centering
@@ -922,7 +1004,7 @@ non-exhaustive list of first-class control operators.
     \hline
     control/prompt      & Delimited & Composable & \citet{Felleisen88}\\
     \hline
-    effect handlers     & Delimited & Composable & \citet{PlotkinP09,PlotkinP13} \\
+    effect handlers     & Delimited & Composable & \citet{PlotkinP13} \\
     \hline
     escape              & Undelimited & Abortive & \citet{Reynolds98a}\\
     \hline
@@ -934,19 +1016,22 @@ non-exhaustive list of first-class control operators.
     \hline
     shift/reset         & Delimited & Composable & \citet{DanvyF90}\\
     \hline
-    spawn               & Delimited & Composable & \citet{HiebDA94}\\
+    spawn               & Delimited & Composable & \citet{HiebD90}\\
     \hline
     splitter            & Delimited & Abortive, composable & \citet{QueinnecS91}\\
     \hline
   \end{tabular}
   \caption{Classification of first-class sequential control operators.}\label{tbl:classify-ctrl}
+  \dhil{TODO: Possibly split into two tables: undelimited and delimited. Change the table to display the behaviour of control reifiers.}
 \end{table}
 %
 
-\paragraph{An optical device for control}
+\paragraph{A small calculus for control}
 %
 To look at control we will a simply typed fine-grain call-by-value
-calculus. The calculus is essentially the same as the one used in
+calculus. Although, we will sometimes have to discard the types, as
+many of the control operators were invented and studied in a untyped
+setting. The calculus is essentially the same as the one used in
 Chapter~\ref{ch:handlers-efficiency}, except that here we will have an
 explicit invocation form for continuations. Although, in practice most
 systems disguise continuations as first-class functions, but for a
@@ -958,20 +1043,20 @@ depicts the syntax of types and terms in the calculus.
 \begin{figure}
   \centering
 \begin{syntax}
-  \slab{Types}        & A,B &::=& \UnitType \mid \Zero \mid A \to B \mid A + B \mid A \times B \mid \Cont\,\Record{A;B} \smallskip\\
+  \slab{Types}        & A,B &::=& \UnitType \mid A \to B \mid A \times B \mid \Cont\,\Record{A;B} \mid A + B \smallskip\\
-  \slab{Values}       & V,W &::=& x \mid \lambda x^A.M \mid V + W \mid \Record{V;W} \mid \Unit \mid \cont_\EC\\
+  \slab{Values}       & V,W &::=& \Unit \mid \lambda x^A.M \mid \Record{V;W} \mid \cont_\EC \mid \Inl~V \mid \Inr~W \mid x\\
-  \slab{Computations} & M,N &::=& \Return\;V \mid \Let\;x \revto M \;\In\;N \mid \Let \Record{x;y} = V \;\In\; N \\
+  \slab{Computations} & M,N &::=& \Return\;V \mid \Let\;x \revto M \;\In\;N \mid \Let\;\Record{x;y} = V \;\In\; N \\
-                       &     &\mid& \Absurd^A\;V \mid V\,W \mid \Continue~V~W \smallskip\\
+                       &     &\mid& V\,W \mid \Continue~V~W \smallskip\\
   \slab{Evaluation\textrm{ }contexts} & \EC &::=& [\,] \mid \Let\;x \revto \EC \;\In\;N
 \end{syntax}
 \caption{Types and term syntax}\label{fig:pcf-lang-control}
 \end{figure}
 %
-The types are the standard simple types with the addition of the empty
+The types are the standard simple types with the addition of the
-type $\Zero$ and the continuation object type $\Cont\,\Record{A;B}$,
+continuation object type $\Cont\,\Record{A;B}$, which is parameterised
-which is parameterised by an argument type and a result type,
+by an argument type and a result type, respectively. The static
-respectively. The static semantics is standard as well, except for the
+semantics is standard as well, except for the continuation invocation
-continuation invocation primitive $\Continue$.
+primitive $\Continue$.
 %
 \begin{mathpar}
     \inferrule*
@@ -1045,7 +1130,7 @@ $\Escape$, however, it is worth noting that this idiom require
 recursive types to type check. Even in a language without recursive
 types, the continuation may propagate outside its binding
 $\Escape$-expression if the language provides an escape hatch such as
-mutable reference cells.
+mutable references.
 % In our simply-typed setting it is not possible for the continuation to
 % propagate outside its binding $\Escape$-expression as it would require
 % the addition of either recursive types or some other escape hatch like