From eec734c014e5bb9363753851eee14927293ef502 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Daniel=20Hillerstr=C3=B6m?= Date: Tue, 24 Nov 2020 20:45:57 +0000 Subject: [PATCH] Control calculus --- thesis.tex | 202 ++++++++++++++++++++++++++++++++++++++++++----------- 1 file changed, 163 insertions(+), 39 deletions(-) diff --git a/thesis.tex b/thesis.tex index af09dd9..5cf2a44 100644 --- a/thesis.tex +++ b/thesis.tex @@ -568,6 +568,42 @@ the translation preserve typeability. \citet{Shan04} shows that dynamic delimited control and static delimited control is macro-expressible in an untyped setting. +\paragraph{A language for understanding 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 +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 +theoretical examination it is convenient to treat them specially such +that continuation invocation is a separate reduction rule from +ordinary function application. Figure~\ref{fig:pcf-lang-control} +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{Values} & V,W &::=& x \mid \lambda x^A.M \mid V + W \mid \Record{V;W} \mid \Unit \mid \cont_\EC\\ + \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\\ + \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 +type $\Zero$ and the continuation object type $\Cont\,\Record{A;B}$, +which is parameterised by an argument type and a result type, +respectively. The static semantics is standard as well, except for the +continuation invocation primitive $\Continue$. +% +\begin{mathpar} + \inferrule* + {\typ{\Gamma}{V : A} \\ \typ{\Gamma}{W : \Cont\,\Record{A;B}}} + {\typ{\Gamma}{\Continue~W~V : B}} +\end{mathpar} + \section{Classifying continuations} % \citeauthor{Reynolds93} has written a historical account of the @@ -678,7 +714,7 @@ Downward and upward use of continuations. \section{Controlling continuations} Table~\ref{tbl:classify-ctrl} provides a classification of a non-exhaustive list of first-class control operators. - +% \begin{table} \centering \begin{tabular}{| l | l | l | l |} @@ -718,8 +754,9 @@ non-exhaustive list of first-class control operators. \end{tabular} \caption{Classification of first-class sequential control operators.}\label{tbl:classify-ctrl} \end{table} +% -\subsection{Undelimited operators} +\subsection{Undelimited control operators} % The early inventions of undelimited control operators were driven by the desire to provide a `functional' equivalent of jumps as provided @@ -744,7 +781,7 @@ composable variant of callcc appeared. Moreover, every operator, except for \citeauthor{Landin98}'s J operator, capture the current continuation. -\paragraph{Reynolds' escape} The escape operator was introduced by +\paragraph{\citeauthor{Reynolds98a}' escape} The escape operator was introduced by \citeauthor{Reynolds98a} in 1972~\cite{Reynolds98a} to make statement-oriented control mechanisms such as jumps and labels programmable in an expression-oriented language. @@ -817,7 +854,7 @@ plugged into the context. The \slab{Resume} discards the current context $\EC$ and installs the captured context $\EC'$ with the argument $V$ plugged in. -\paragraph{Sussman and Steele's catch} +\paragraph{\citeauthor{SussmanS75}'s catch} % The catch operator originated in Lisp as an exception handling construct. It had a companion throw operation, which would unwind the @@ -1022,14 +1059,16 @@ evaluation context. \paragraph{\FelleisenC{} and \FelleisenF{}} % -The C operator is a variation of callcc, where capture mechanism -aborts the current continuation after capture. It was introduced by -\citeauthor{FelleisenFKD86} in two papers in -1986~\cite{FelleisenF86,FelleisenFKD86}. The year after +The C operator is a variation of callcc that provides control over the +whole continuation as it aborts the current continuation after +capture, whereas callcc implicitly invokes the current continuation on +the value of its argument. The C operator was introduced by +\citeauthor{FelleisenFKD86} in two papers during +1986~\cite{FelleisenF86,FelleisenFKD86}. The following year, \citet{FelleisenFDM87} introduced the F operator which is a variation -of C, where the captured continuation is composable. +of C, whose captured continuation is composable. -Both operators are values. +In our framework both operators are value forms. % \[ V,W \in \ValCat ::= \cdots \mid \FelleisenC \mid \FelleisenF @@ -1077,7 +1116,7 @@ $\FelleisenC$. % \citet{FelleisenFDM87} also postulate that $\FelleisenC$ cannot express $\FelleisenF$. -\paragraph{Landin's J operator} +\paragraph{\citeauthor{Landin98}'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 @@ -1222,20 +1261,105 @@ syntactically embedded using callcc. \dhil{I am sort of torn between whether to treat continuations as first-class functions\dots} -\subsection{Delimited operators} -% -A delimited control operator captures only a designated segment of the -evaluation stack. Typically, a delimited control operator is a pair -consisting of a \emph{delimiter} and \emph{capture operation}. The -delimiter delimits the extent of the continuation captured by the -capture operation. -% -The first delimited control operator was introduced by -\citet{Felleisen88} with prompt and control, where prompt is the -delimiter and control is the capture operation. Shortly after -\citet{DanvyF89} introduced their shift and reset as an alternative -capture operation and delimiter, respectively. Since then a whole -variety of delimited control operators have been invented. +\subsection{Delimited control operators} +% +The main problem with undelimited control is that it is the +programmatic embodiment of the proverb \emph{all or nothing} in the +sense that an undelimited continuation always represent the entire +residual program from its point of capture. With undelimited control +there is no middle that allows some segments of the evaluation context +to be reified. +% +Delimited control rectifies this problem by associating each control +operator with a control delimiter such that designated segments of the +evaluation context can be captured individually without interfering +with the context beyond the delimiter. This provides a powerful and +modular programmatic tool that enables programmers to isolate the +control flow of specific parts of their programs, and thus enables +local reasoning about the behaviour of control infused program +segments. +% +One may argue that delimited control to an extent is more first-class +than undelimited control, because it provides fine-grain control over +the evaluation context. +% +Essentially, delimited control adds the excluded middle: \emph{all, + some, or nothing}. + +In 1988 \citeauthor{Felleisen88} introduced the first control +delimiter known as `prompt', as a companion to the composable control +operator F (alias control)~\cite{Felleisen88}. +% +In \citeauthor{Felleisen88}'s line of work that led to the invention +of prompt was driven by a dynamic understanding of composable +continuations in terms of algebraic manipulation of continuations in +the control string of abstract machines. In context of abstract +machines a continuation is defined as a sequence of frames, whose end +is marked by a prompt, and the composition of continuations is defined +as concatenation of their +sequences~\cite{Felleisen87,FelleisenF86,FelleisenWFD88}. +% +This understanding of composable continuations ultimately led to the +control phenomenon known as \emph{dynamic delimited control}. + +The following year, \citet{DanvyF89} introduced an alternative pair of +operators known as `shift' and `reset'. Their line of work were driven +by a static understanding of composable continuations in terms of +continuation passing style~\cite{DanvyF89,DanvyF90,DanvyF92}. +% +In this context a continuation is a compositional function in the +sense of \citeauthor{StracheyW74}'s denotational continuation +semantics~\cite{StracheyW74,StracheyW00}. +% +Their understanding of composable continuations ultimately led to the +control phenomenon known as \emph{static delimited control}. + + +% \citeauthor{Felleisen88}'s line of work +% that led to the invention of prompt was driven by motivation to +% provide a modular basis for programming with composable continuations, +% or `functional' jumps, which represent a shift in focus from abortive +% continuations, or `imperative' jumps, which had motivated undelimited +% control. +% + + +% The early inventions of delimited operators were driven by a desire to +% provide a modular and compositional basis for implementing various +% control phenomena such as exceptions, coroutines, +% engines~\cite{HaynesF84}, etc. +% % +% Whilst \citet{FriedmanH85} were arguing that undelimited control must be +% constrained, because the integrity of control phenomena embedded using +% undelimited is easily destroyed control are brittle and interact +% poorly with the environment. + +% observed that control abstractions implemented in +% terms of unrestricted undelimited control, as provided by callcc, is +% brittle and inappropriate use can easily destroy the integrity of the +% embedded abstractions. They suggested to impose several ad-hoc, and +% rather complicated, restrictions on callcc and its continuations to +% make them modular. +% % + +% \citeauthor{Felleisen88} wanted to develop a principled mechanism for +% capturing and composing continuations. The initial ideas towards +% delimited control were developed in \citeauthor{Felleisen87}'s PhD +% dissertation~\cite{Felleisen87} and related +% papers~\cite{FelleisenF86,FelleisenFDM87} with the design of the +% operator F. +% % A delimited control operator captures only a designated segment of the +% % evaluation stack. Typically, a delimited control operator is a pair +% % consisting of a \emph{delimiter} and \emph{capture operation}. The +% % delimiter delimits the extent of the continuation captured by the +% % capture operation. +% % +% The first delimited control operator was introduced by +% \citet{Felleisen88} with prompt and control, where prompt is the +% delimiter and control is the capture operation. Shortly after +% \citet{DanvyF89} introduced their shift and reset as an alternative +% capture operation and delimiter, respectively. Since then a whole +% variety of delimited control operators have been invented. % Delimited control: Control delimiters form the basis for delimited % control. \citeauthor{Felleisen88} introduced control delimiters in @@ -1258,7 +1382,7 @@ variety of delimited control operators have been invented. \paragraph{\citeauthor{Felleisen88}'s control and prompt} % Control and prompt were introduced by \citeauthor{Felleisen88} in -1988~\cite{Felleisen88}. The capture operation `control' is a +1988~\cite{Felleisen88}. The control operator `control' is a rebranding of the F operator. Although, the name `control' was first introduced a little later by \citet{SitaramF90}. A prompt acts as a control-flow barrier that delimits different parts of a program, @@ -1318,7 +1442,7 @@ typing judgement as $\FelleisenF$. % The dynamic semantics for control and prompt consist of three rules: -1) to handle return through a prompt, 2) continuation capture, and 3) +1) handle return through a prompt, 2) continuation capture, and 3) continuation invocation. % \begin{reductions} @@ -1364,11 +1488,11 @@ few simple examples. The continuation captured by the application of $\Control$ is oblivious to the continuation $1 + [\,]$ of $\Prompt$. Since the captured continuation is composable it returns to its call site. The -first invocation of $k$ returns the value 2, which is provided as the -argument to the second invocation of $k$, resulting in the value -$4$. The prompt gets eliminated after its computation constituent has -been fully reduced. Technically, the prompt is eliminated by applying -the continuation of $\Prompt$ with the value $4$. +first invocation of the continuation $k$ returns the value 2, which is +provided as the argument to the second invocation of $k$, resulting in +the value $4$. The prompt $\Prompt$ gets eliminated when the +computation constituent of $\Prompt$ has been reduced to the value +$4$, which is (implicitly) supplied to the continuation of $\Prompt$. Let us consider a slight variation of the previous example. % @@ -1417,11 +1541,11 @@ discarded, because the continuation $k'$ is never invoked. % % -\begin{reductions} - % \slab{Value} & \reset{V} &\reducesto& V\\ - \slab{Capture} & \reset{\EC[\shift\,k.M]} &\reducesto& M[\cont_{\reset{\EC}}/k]\\ - % \slab{Resume} & \Continue~\cont_{\reset{\EC}}~V &\reducesto& \reset{\EC[V]}\\ -\end{reductions} +% \begin{reductions} +% % \slab{Value} & \reset{V} &\reducesto& V\\ +% \slab{Capture} & \reset{\EC[\shift\,k.M]} &\reducesto& M[\cont_{\reset{\EC}}/k]\\ +% % \slab{Resume} & \Continue~\cont_{\reset{\EC}}~V &\reducesto& \reset{\EC[V]}\\ +% \end{reductions} % \paragraph{\citeauthor{PlotkinP09}'s effect handlers} @@ -1562,7 +1686,7 @@ implementation strategies. \hline OchaCaml & shift/reset & Virtual machine\\ \hline - Racket & callcc, callcc$^{\ast}$, cupto, fcontrol, prompt/control, shift/reset, splitter, spawn & Continuation marks\\ + Racket & callcc, callcc$^{\ast}$, cupto, fcontrol, control/prompt, shift/reset, splitter, spawn & Continuation marks\\ \hline Rhino JavaScript & JI & Interpreter \\ \hline @@ -1570,7 +1694,7 @@ implementation strategies. \hline SML/NJ & callcc & CPS\\ \hline - Wasm/k & prompt/control & ?? \\ + Wasm/k & control/prompt & ?? \\ \hline \end{tabular} \caption{Some languages and their implementation strategies for first-class control.}\label{tbl:ctrl-operators-impls}