From 9f8bbe7ff47ca35692786adc0f6225246874dc61 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Daniel=20Hillerstr=C3=B6m?= Date: Sat, 5 Dec 2020 15:23:47 +0000 Subject: [PATCH] Composable continuations. Controlling continuations intro. --- thesis.tex | 68 ++++++++++++++++++++++++++++++++++++++++-------------- 1 file changed, 51 insertions(+), 17 deletions(-) diff --git a/thesis.tex b/thesis.tex index 228f17c..78375ad 100644 --- a/thesis.tex +++ b/thesis.tex @@ -827,7 +827,7 @@ itself have no effect. % The innermost application erases the outermost application term, consequently only the first application of $\cont$ occurs during -runtime. +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 @@ -837,11 +837,33 @@ 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. +its captured context with the its invocation context, i.e. % \[ - \EC[\Continue~\cont_{\EC'}~V] \reducesto \EC[\EC'[V]] + \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}. @@ -950,8 +972,17 @@ its captured context with the its invocation context. \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 @@ -973,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 @@ -985,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 @@ -1009,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{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{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 &::=& \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 \\ + & &\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$. +The types are the standard simple types with the addition of 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* @@ -1096,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