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

fcontrol

Browse Source
This commit is contained in:
Daniel Hillerström
2020-11-28 00:44:48 +00:00
parent 9e343cb064
commit 673958e406
1 changed files with 31 additions and 10 deletions
Download Patch File Download Diff File Expand all files Collapse all files

41
thesis.tex
View File

@@ -1657,29 +1657,50 @@ and state~\cite{Filinski94}.
\dhil{TODO: Canonical reference \citet{HiebDA94}} \dhil{TODO: Canonical reference \citet{HiebDA94}}
\paragraph{\citeauthor{Sitaram93}'s fcontrol} The control operator \paragraph{\citeauthor{Sitaram93}'s fcontrol} The control operator
`fcontrol' was introduced by \citet{Sitaram93} in 1993. The fcontrol `fcontrol' was introduced by \citet{Sitaram93} in 1993. It is a
operator distinguishes itself from the previous control operators in refinement of control0/prompt0, and thus, it can be characterised as a
that it supports handling of continuations. \citeauthor{Sitaram93}'s dynamic delimited control operator. The main novelty of fcontrol is
observation was that previous control operators had hardwired handling that is separate continuation handling from continuation capturing by
of continuations into the capture mechanism, e.g. callcc applies its providing the programmer with ability to attach a handler to the
argument with the captured continuation. The programmer has no control prompt. This handler is activated whenever a continuation is captured.
over whether to function argument should be run immediately or run at %
all. \citeauthor{Sitaram93}'s goal was decouple the continuation \citeauthor{Sitaram93}'s observation was that with previous control
capturing mechanism from the continuation handling mechanism. operators the capture and handling mechanisms are intertwined. For
example, callcc applies its argument with the captured
continuation. The programmer has no control over when the function
argument should be run.
The operator fcontrol is a value and prompt with handler is a
computation.
% %
\begin{syntax} \begin{syntax}
& V, W &::=& \cdots \mid \fcontrol\\ & V, W &::=& \cdots \mid \fcontrol\\
& M, N &::=& \cdots \mid \fprompt~V.M & M, N &::=& \cdots \mid \fprompt~V.M
\end{syntax} \end{syntax}
% %
As with $\Callcc$, the value $\fcontrol$ may be regarded as a special
unary function symbol. The value constituent of the prompt
($\fprompt$) is the control handler. It is a binary function, that
gets applied to the argument of $\fcontrol$ and the continuation up to
the prompt.
%
The dynamic semantics elucidate this behaviour.
%
\begin{reductions} \begin{reductions}
\slab{Value} & \slab{Value} &
\fprompt~V.W &\reducesto& W\\ \fprompt~V.W &\reducesto& W\\
\slab{Capture} & \slab{Capture} &
\fprompt~V.\EC[\fcontrol~W] &\reducesto& V~W~\cont_{\EC}, \text{ where $\EC$ contains no \fprompt}\\ \fprompt~V.\EC[\fcontrol~W] &\reducesto& V~W~\qq{\cont_{\EC}}, \text{ where $\EC$ contains no \fprompt}\\
\slab{Resume} & \Continue~\cont_{\EC}~V &\reducesto& \EC[V] \slab{Resume} & \Continue~\cont_{\EC}~V &\reducesto& \EC[V]
\end{reductions} \end{reductions}
% %
The $\slab{Value}$ is similar to the previous $\slab{Value}$
rules. The interesting rule is the $\slab{Capture}$. When $\fcontrol$
is applied to some value $W$ the enclosing context $\EC$ gets reified
and aborted up to the nearest enclosing prompt, which invokes the
handler $V$ with the argument $W$ and the continuation.
%
\dhil{Show an example\dots}
\paragraph{Cupto} The control operator cupto is a variation of \paragraph{Cupto} The control operator cupto is a variation of
control0/prompt0 designed to fit into the typed ML-family of control0/prompt0 designed to fit into the typed ML-family of