dhil/phd-dissertation
1
0
Fork 0
mirror of https://github.com/dhil/phd-dissertation synced 2026-03-13 02:58:26 +00:00
Code Issues Releases Wiki Activity

Callcc

Browse Source
This commit is contained in:
Daniel Hillerström
2020-11-09 01:37:05 +00:00
parent 293bdae1d3
commit ea9763fd70
2 changed files with 42 additions and 12 deletions
Download Patch File Download Diff File Expand all files Collapse all files

6
macros.tex
View File

@@ -150,7 +150,7 @@
%% %%
%% Labels %% Labels
%% %%
\newcommand{\slab}[1]{\textrm{#1}} \newcommand{\slab}[1]{\ensuremath{\mathsf{#1}}}
\newcommand{\rulelabel}[2]{\ensuremath{\mathsf{#1\textrm{-}#2}}} \newcommand{\rulelabel}[2]{\ensuremath{\mathsf{#1\textrm{-}#2}}}
\newcommand{\klab}[1]{\rulelabel{K}{#1}} \newcommand{\klab}[1]{\rulelabel{K}{#1}}
\newcommand{\semlab}[1]{\rulelabel{S}{#1}} \newcommand{\semlab}[1]{\rulelabel{S}{#1}}
@@ -440,8 +440,8 @@
\newcommand{\fprompt}{\%} \newcommand{\fprompt}{\%}
\newcommand{\splitter}{\keyw{splitter}} \newcommand{\splitter}{\keyw{splitter}}
\newcommand{\J}{\keyw{J}} \newcommand{\J}{\keyw{J}}
\newcommand{\FelleisenC}{\ensuremath{\mathcal{C}}} \newcommand{\FelleisenC}{\ensuremath{\keyw{C}}}
\newcommand{\FelleisenF}{\ensuremath{\mathcal{F}}} \newcommand{\FelleisenF}{\ensuremath{\keyw{F}}}
\newcommand{\cont}{\keyw{cont}} \newcommand{\cont}{\keyw{cont}}
\newcommand{\Cont}{\dec{Cont}} \newcommand{\Cont}{\dec{Cont}}
\newcommand{\Algol}{Algol~60} \newcommand{\Algol}{Algol~60}

48
thesis.tex
View File

@@ -679,7 +679,7 @@ non-exhaustive list of first-class control operators.
\hline \hline
\multicolumn{1}{| l |}{\textbf{Name}} & \multicolumn{1}{l |}{\textbf{Extent}} & \multicolumn{1}{l |}{\textbf{Continuation behaviour}} & \multicolumn{1}{l |}{\textbf{Canonical reference}}\\ \multicolumn{1}{| l |}{\textbf{Name}} & \multicolumn{1}{l |}{\textbf{Extent}} & \multicolumn{1}{l |}{\textbf{Continuation behaviour}} & \multicolumn{1}{l |}{\textbf{Canonical reference}}\\
\hline \hline
\FelleisenC & Undelimited & Abortive & \citet{FelleisenF86} \\ C & Undelimited & Abortive & \citet{FelleisenF86} \\
\hline \hline
call/cc & Undelimited & Abortive & \citet{AbelsonHAKBOBPCRFRHSHW85} \\ call/cc & Undelimited & Abortive & \citet{AbelsonHAKBOBPCRFRHSHW85} \\
\hline \hline
@@ -697,7 +697,7 @@ non-exhaustive list of first-class control operators.
\hline \hline
escape & Undelimited & Abortive & \citet{Reynolds98a}\\ escape & Undelimited & Abortive & \citet{Reynolds98a}\\
\hline \hline
\FelleisenF & Undelimited & Composable & \citet{FelleisenFDM87}\\ F & Undelimited & Composable & \citet{FelleisenFDM87}\\
\hline \hline
fcontrol & Delimited & Composable & \citet{Sitaram93} \\ fcontrol & Delimited & Composable & \citet{Sitaram93} \\
\hline \hline
@@ -837,7 +837,24 @@ As an aside it is worth to mention that \citet{CartwrightF92} used a
variation of $\Catch$ to show that control operators enable programs variation of $\Catch$ to show that control operators enable programs
to observe the order of evaluation. to observe the order of evaluation.
\paragraph{Call-with-current-continuation} \paragraph{Call-with-current-continuation} In 1982 the Scheme
implementors observed that they could dispense of the special syntax
for $\Catch$ in favour of a higher-order function that would apply its
argument to the current continuation, and thus callcc was born (callcc
is short for
call-with-current-continuation)~\cite{AbelsonHAKBOBPCRFRHSHW85}.
%
Unlike the previous operators, callcc augments the syntactic
categories of values.
%
\[
V,W \in \ValCat ::= \cdots \mid \Callcc
\]
%
The value $\Callcc$ is essentially a hard-wired function name. The
typing rule for $\Callcc$ makes it clear that it is a particular
higher-order function.
% %
\begin{mathpar} \begin{mathpar}
\inferrule* \inferrule*
@@ -849,11 +866,22 @@ to observe the order of evaluation.
{\typ{\Gamma}{\Continue~W~V : \Zero}} {\typ{\Gamma}{\Continue~W~V : \Zero}}
\end{mathpar} \end{mathpar}
% %
An invocation of $\Callcc$ returns a value of type $A$. This value can
be produced in one of two ways, either the function argument returns
normally or it applies the provided continuation object to a value
that then becomes the result of $\Callcc$-application.
%
\begin{reductions} \begin{reductions}
\slab{Capture} & \EC[\Callcc~V] &\reducesto& \EC[V~\cont_{\EC}]\\ \slab{Capture} & \EC[\Callcc~V] &\reducesto& \EC[V~\cont_{\EC}]\\
\slab{Resume} & \EC[\Continue~\cont_{\EC'}~V] &\reducesto& \EC'[V] \slab{Resume} & \EC[\Continue~\cont_{\EC'}~V] &\reducesto& \EC'[V]
\end{reductions} \end{reductions}
% %
From the dynamic semantics it is evident that $\Callcc$ is a
syntax-free alternative to $\Catch$, i.e.
%
\[
\sembr{\Catch~k.M} = \Callcc\,(\lambda k.M)
\]
\paragraph{Call-with-composable-continuation} \paragraph{Call-with-composable-continuation}
call-with-composable-continuation (MzScheme 360, November 2006). call-with-composable-continuation (MzScheme 360, November 2006).
@@ -1014,8 +1042,8 @@ annotate the evaluation contexts for ordinary applications.
\slab{Resume} & \EC[\Continue~\cont_{\Record{\EC';W}}\,V] &\reducesto& \EC'[W\,V] \slab{Resume} & \EC[\Continue~\cont_{\Record{\EC';W}}\,V] &\reducesto& \EC'[W\,V]
\end{reductions} \end{reductions}
% %
$\slab{Capture}$ rule only applies if the application of $\J$ takes The $\slab{Capture}$ rule only applies if the application of $\J$
place in annotated evaluation context. The continuation object takes place in annotated evaluation context. The continuation object
produced by a $\J$ application encompasses the caller's continuation produced by a $\J$ application encompasses the caller's continuation
$\EC_\lambda$ and the value argument $W$. $\EC_\lambda$ and the value argument $W$.
% %
@@ -1055,6 +1083,8 @@ undelimited control~\cite{Filinski94}
\paragraph{Control/prompt} \paragraph{Control/prompt}
% %
The operator control is a rebranding of Felleisen's F operator.
%
\begin{reductions} \begin{reductions}
\slab{Value} & \slab{Value} &
\Prompt~V &\reducesto& V\\ \Prompt~V &\reducesto& V\\
@@ -1123,9 +1153,9 @@ undelimited control~\cite{Filinski94}
% %
\begin{reductions} \begin{reductions}
\slab{Value} & \reset{V} &\reducesto& V\\ \slab{Value} & \reset{V} &\reducesto& V\\
\slab{Capture} & \reset{\EC[\shift\,k.M]} &\reducesto& \reset{M[\cont_{\reset{\EC}}/k]}, \text { where $\EC$ contains no $\reset{-}$}\\ \slab{Capture} & \reset{\EC[\shift\,k.M]} &\reducesto& \reset{M[\cont_{\EC}/k]}, \text { where $\EC$ contains no $\reset{-}$}\\
% \slab{Resume} & \reset{\EC[\Continue~\cont_{\reset{\EC'}}~V]} &\reducesto& \reset{\EC[\reset{\EC'[V]}]}\\ % \slab{Resume} & \reset{\EC[\Continue~\cont_{\reset{\EC'}}~V]} &\reducesto& \reset{\EC[\reset{\EC'[V]}]}\\
\slab{Resume} & \Continue~\cont_{\reset{\EC}}~V &\reducesto& \reset{\EC[V]}\\ \slab{Resume} & \Continue~\cont_{\EC}~V &\reducesto& \reset{\EC[V]}\\
\end{reductions} \end{reductions}
% %
@@ -1139,9 +1169,9 @@ undelimited control~\cite{Filinski94}
\paragraph{Splitter} \paragraph{Splitter}
\begin{reductions} \begin{reductions}
\slab{Throw} & \splitter~f~g.\EC[\,f~V] &\reducesto& V~\Unit\\ \slab{Throw} & \splitter~throw~callpc.\EC[\,throw~V] &\reducesto& V~\Unit\\
\slab{Capture} & \slab{Capture} &
\splitter~f~g.\EC[g~V] &\reducesto& V~\cont_{\EC} \\ \splitter~throw~callpc.\EC[callpc~V] &\reducesto& V~\cont_{\EC} \\
\slab{Resume} & \Continue~\cont_{\EC}~V &\reducesto& \EC[V] \slab{Resume} & \Continue~\cont_{\EC}~V &\reducesto& \EC[V]
\end{reductions} \end{reductions}