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

Reword fcontrol paragraph

Browse Source
This commit is contained in:
Daniel Hillerström
2020-11-29 16:14:53 +00:00
parent 673958e406
commit e7a64dd145
1 changed files with 34 additions and 16 deletions
Download Patch File Download Diff File Expand all files Collapse all files

50
thesis.tex
View File

@@ -1055,7 +1055,10 @@ continuations and state.
The other way around also appears to be impossible, because neither The other way around also appears to be impossible, because neither
the base calculus nor $\Callcomc$ has the ability to discard an the base calculus nor $\Callcomc$ has the ability to discard an
evaluation context. evaluation context.
%
\dhil{Remark that $\Callcomc$ was originally obtained by decomposing
$\fcontrol$ a continuation composing primitive and an abortive
primitive. Source: Matthew Flatt, comp.lang.scheme, May 2007}
\paragraph{\FelleisenC{} and \FelleisenF{}} \paragraph{\FelleisenC{} and \FelleisenF{}}
% %
@@ -1658,17 +1661,20 @@ and state~\cite{Filinski94}.
\paragraph{\citeauthor{Sitaram93}'s fcontrol} The control operator \paragraph{\citeauthor{Sitaram93}'s fcontrol} The control operator
`fcontrol' was introduced by \citet{Sitaram93} in 1993. It is a `fcontrol' was introduced by \citet{Sitaram93} in 1993. It is a
refinement of control0/prompt0, and thus, it can be characterised as a refinement of control0/prompt0, and thus, it is a dynamic delimited
dynamic delimited control operator. The main novelty of fcontrol is control operator. The main novelty of fcontrol is that it shifts the
that is separate continuation handling from continuation capturing by handling of continuations from control capture operator to the control
providing the programmer with ability to attach a handler to the delimiter. The prompt interface for fcontrol lets the programmer
prompt. This handler is activated whenever a continuation is captured. attach a handler to it. This handler is activated whenever a
continuation captured.
% %
\citeauthor{Sitaram93}'s observation was that with previous control \citeauthor{Sitaram93}'s observation was that with previous control
operators the capture and handling mechanisms are intertwined. For operators the handling of control happens at continuation capture
example, callcc applies its argument with the captured point, meaning that the control handling logic gets intertwined with
continuation. The programmer has no control over when the function application logic. The inspiration for the interface of fcontrol and
argument should be run. its associated prompt came from exception handlers, where the handling
of exceptions is separate from the invocation site of
exceptions~\cite{Sitaram93}.
The operator fcontrol is a value and prompt with handler is a The operator fcontrol is a value and prompt with handler is a
computation. computation.
@@ -1679,12 +1685,13 @@ computation.
\end{syntax} \end{syntax}
% %
As with $\Callcc$, the value $\fcontrol$ may be regarded as a special As with $\Callcc$, the value $\fcontrol$ may be regarded as a special
unary function symbol. The value constituent of the prompt unary function symbol. The syntax $\fprompt$ denotes a prompt (in
($\fprompt$) is the control handler. It is a binary function, that \citeauthor{Sitaram93}'s terminology it is called run). The value
gets applied to the argument of $\fcontrol$ and the continuation up to constituent of $\fprompt$ is the control handler. It is a binary
the prompt. function, that gets applied to the argument of $\fcontrol$ and the
continuation up to the prompt.
% %
The dynamic semantics elucidate this behaviour. The dynamic semantics elucidate this behaviour formally.
% %
\begin{reductions} \begin{reductions}
\slab{Value} & \slab{Value} &
@@ -1754,7 +1761,18 @@ here, only the essential rules for the $\Cupto$ constructs.
The typing rule for $\Set$ uses the type embedded in the prompt to fix The typing rule for $\Set$ uses the type embedded in the prompt to fix
the type of the whole computation $N$. Similarly, the typing rule for the type of the whole computation $N$. Similarly, the typing rule for
$\Cupto$ uses the prompt type of its value argument to fix the answer $\Cupto$ uses the prompt type of its value argument to fix the answer
type for the continuation $k$. type for the continuation $k$. The type of the $\Cupto$ expression is
the same as the domain of the continuation, which at first glance may
seem strange. The intuition is that $\Cupto$ behaves as a let binding
for the continuation in the context of a $\Set$ expression, i.e.
%
\[
\bl
\Set\;p^{\prompttype~B}\;\In\;\EC[\Cupto\;p\;k^{A \to B}.M^B]^B\\
\reducesto \Let\;k \revto \lambda x^{A}.\EC[x]^B \;\In\;M^B
\el
\]
%
The dynamic semantics is generative to accommodate generation of fresh The dynamic semantics is generative to accommodate generation of fresh
prompts. Formally, the reduction relation is augmented with a store prompts. Formally, the reduction relation is augmented with a store