dhil
/
phd-dissertation
mirror of https://github.com/dhil/phd-dissertation
1
0
Fork 0
Code Issues Releases Wiki Activity
Browse Source

Example

master
Daniel Hillerström 5 years ago
parent
d6b67950b2
commit
50125e86ac
1 changed files with 222 additions and 211 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 425
      thesis.tex

425
thesis.tex
View File

@ -11226,9 +11226,9 @@ a deep, parameterised, and shallow handler.
\Return\;x &\mapsto& [x]\\
\OpCase{\Fork}{\Unit}{resume} &\mapsto&
\bl
\Let\;t \revto resume~\True\;\In\\
\Let\;f \revto resume~\False\;\In\\
t \concat f
\Let\;xs \revto resume~\True\;\In\\
\Let\;ys \revto resume~\False\;\In\;
xs \concat ys
\el
\ea
\el
@ -11249,7 +11249,7 @@ a deep, parameterised, and shallow handler.
\ParamHandle\;m\,\Unit\;\With\\
~\left(i.\,\ba{@{~}l@{~}c@{~}l}
\Return\;x &\mapsto& x\\
\OpCase{\Incr}{\Unit}{resume} &\mapsto& resume\,\Record{i+1;i}
\OpCase{\Incr}{\Unit}{resume} &\mapsto& \Let\;i' \revto i+1\;\In\;resume\,\Record{i';i}
\ea\right)~i_0
\el
\el
@ -11284,14 +11284,14 @@ a deep, parameterised, and shallow handler.
\prodf : \UnitType \to \alpha \eff \{\Incr : \UnitType \opto \Int; \Yield : \Int \opto \UnitType\}\\
\prodf\,\Unit \defas
\bl
\Let\;i \revto \Do\;\Incr\,\Unit\;\In\\
\Let\;x \revto \Do\;\Yield~i\\
\Let\;j \revto \Do\;\Incr\,\Unit\;\In\;
\Let\;x \revto \Do\;\Yield~j\;
\In\;\dec{prod}\,\Unit
\el\smallskip\\
\consf : \UnitType \to \Int \eff \{\Fork : \UnitType \opto \Bool; \Await : \UnitType \opto \Int\}\\
\consf\,\Unit \defas
\bl
\Let\;b \revto \Do\;\Fork\,\Unit\;\In\\
\Let\;b \revto \Do\;\Fork\,\Unit\;\In\;
\Let\;x \revto \Do\;\Await\,\Unit\;\In\\
% \Let\;y \revto \Do\;\Await\,\Unit\;\In\\
\If\;b\;\Then\;x+2\;\Else\;x*2
@ -11299,269 +11299,280 @@ a deep, parameterised, and shallow handler.
\el
\]
%
\begin{equation}
\nondet\,(\lambda\Unit.\incr\,\Record{1;\lambda\Unit.\Pipe\,\Record{\prodf;\consf}})\label{eq:abs-prog}
\end{equation}
%
Function interpretation is somewhat heavy notation-wise as
environments need to be built. To make the notation a bit more
lightweight I will not define the initial environments for closures
explicitly. By convention I will subscript initial environments with
the name of function, e.g. $\env_\consf$ denotes the initial
environment for the closure of $\consf$. Extensions of initial
environments will use superscripts to differentiate themselves,
e.g. $\env_\consf'$ is an extension of $\env_\consf$. As a final
environment simplification, I will take the initial environments to
contain the bindings for parameters of their closures, that is, an
initial environment is really the environment for the body of its
closure. In a similar fashion, I will use superscripts and subscripts
to differentiate handler closures, e.g. $\chi^\dagger_\Pipe$ denotes
the handler closure for the shallow handler definition in $\Pipe$. The
environment of a handler closure is to be understood
implicitly. Furthermore, the definitions above should be understood to
be implicitly $\Let$-sequenced, whose tail computation is
\eqref{eq:abs-prog}. Evaluation of this sequence gives rise to a
`toplevel' environment, which binds the closures for the definition. I
shall use $\env_0$ to denote this environment.
The machine starts in an initial configuration with the $\env_0$
environment. The initial transitions install the three handlers in
order: $\nondet$, $\incr$, and $\Pipe$.
%
\begin{derivation}
&\nondet\,(\lambda\Unit.\incr\,\Record{0;\lambda\Unit.\Pipe\,\Record{\prodf;\consf}})\\
&\nondet\,(\lambda\Unit.\incr\,\Record{1;\lambda\Unit.\Pipe\,\Record{\prodf;\consf}})\\
\stepsto& \reason{\mlab{Init} with $\env_0$}\\
&\cek{\nondet\,(\lambda\Unit.\incr\,\Record{0;\lambda\Unit.\Pipe\,\Record{\prodf;\consf}}) \mid \env_0 \mid \sks_0}\\
\stepsto^+& \reason{$3\times$(\mlab{App}, \mlab{Handle^\delta})}\\
&\bl
&% \bl
\cek{c\,\Unit \mid \env_\Pipe \mid (\nil,\chi^\dagger_\Pipe) \cons (\nil, \chi^\param_\incr) \cons (\nil, \chi_\nondet) \cons \kappa_0}\\
\text{where }
\bl
\env_\Pipe = \env_0[c \mapsto (\env_0, \consf), p \mapsto (\env_0, \prodf)]\\
\chi^\dagger_\Pipe = (\env_\Pipe, H^\dagger_\Pipe)\\
\env_\incr = \env_0[m \mapsto (\env_0, \lambda\Unit.\Pipe\cdots),i \mapsto 0]\\
\chi^\param_\incr = (\env_\incr, H^\param_\incr)\\
\env_\nondet = \env_0[m \mapsto (\env_0, \lambda\Unit.\incr \cdots)]\\
\chi_\nondet = (\env_\nondet, H_\nondet)
\el
\el\\
% \text{where }
% \bl
% % \env_\Pipe = \env_0[c \mapsto (\env_0, \consf), p \mapsto (\env_0, \prodf)]\\
% % \chi^\dagger_\Pipe = (\env_\Pipe, H^\dagger_\Pipe)\\
% % \env_\incr = \env_0[m \mapsto (\env_0, \lambda\Unit.\Pipe\cdots),i \mapsto 0]\\
% % \chi^\param_\incr = (\env_\incr, H^\param_\incr)\\
% % \env_\nondet = \env_0[m \mapsto (\env_0, \lambda\Unit.\incr \cdots)]\\
% % \chi_\nondet = (\env_\nondet, H_\nondet)
% \el
% \el\\
\end{derivation}
%
At this stage the continuation consists of four frames. The first
three frames each corresponds to an installed handler, whereas the
last frame is the identity handler. The control component focuses the
application of consumer computation provided as an argument to
$\Pipe$. The next few transitions get us to the first operation
invocation.
%
\begin{derivation}
\stepsto^+& \reason{\mlab{App}, \mlab{Let}}\\
&\bl
\cek{\Do\;\Fork\,\Unit \mid \env_0 \mid ([(\env_0,b,\Let\;x \revto \cdots)],(\env_\Pipe,H^\dagger_\Pipe)) \cons \kappa_1}\\
\text{where } \kappa_1 = (\nil, \chi^\param_\incr) \cons (\nil, \chi_\nondet) \cons \kappa_0
\cek{\Do\;\Fork\,\Unit \mid \env_\consf \mid ([(\env_\consf,b,\Let\;x \revto \cdots)],\chi^\dagger_\Pipe) \cons (\nil, \chi^\param_\incr) \cons (\nil, \chi_\nondet) \cons \kappa_0}\\
\el\\
\stepsto^+& \reason{\mlab{Forward}, \mlab{Forward}}\\
&\bl
\cek{\Do\;\Fork\,\Unit \mid \env_0 \mid [(\nil, \chi_\nondet),(\nil,\chiid)] \circ \kappa'}\\
\text{where } \kappa' = [([(\env_0,b,\Let\;x \revto \cdots)],(\env_\Pipe,H^\dagger_\Pipe)),(\nil, \chi^\param_\incr)]
\cek{\Do\;\Fork\,\Unit \mid \env_\consf \mid [(\nil, \chi_\nondet),(\nil,\chiid)] \circ \kappa'}\\
\text{where } \kappa' = [([(\env_\consf,b,\Let\;x \revto \cdots)],\chi^\dagger_\Pipe),(\nil, \chi^\param_\incr)]
\el\\
\end{derivation}
%
The pure continuation under $\chi^\dagger_\Pipe$ has been augmented
with the pure frame corresponding to $\Let$-binding of the invocation
of $\Fork$. Operation invocation causes the machine to initiate a
search for a suitable handler, as the top-most handler $\Pipe$ does
not handle $\Fork$. The machine performs two $\mlab{Forward}$
transitions, which moves the two top-most frames from the program
continuation onto the forwarding continuation.
%
As a result the, now, top-most frame of the program continuation
contains a suitable handler for $\Fork$. Thus the following
transitions transfer control to $\Fork$-case inside the $\nondet$
handler.
%
\begin{derivation}
\stepsto^+& \reason{\mlab{Do}, \mlab{Let}}\\
&\bl
\cek{resume~\True \mid \env_\nondet' \mid \kappa_0'}\\
\text{where }
\ba[t]{@{~}r@{~}c@{~}l}
\env_\nondet' &=& \env_\nondet[resume \mapsto \kappa' \concat [(\nil, \chi_\nondet)]]\\
\kappa_0' &=& [([(\env_\nondet',x,\Let\;y\revto\cdots)],\chiid)]
\kappa_0' &=& [([(\env_\nondet',xs,\Let\;ys\revto\cdots)],\chiid)]
\el
\el\\
\el
\end{derivation}
%
The $\mlab{Do}$ transition is responsible for activating the handler,
and the $\mlab{Let}$ transition focuses the first resumption
invocation. The resumption $resume$ is bound in the environment to the
forwarding continuation $\kappa'$ extended with the frame for the
current handler. The pure continuation running under the identity
handler gets extended with the $\Let$-binding containing the first
resumption invocation. The next transitions reassemble the program
continuation and focuses control on the invocation of $\Await$.
%
\begin{derivation}
\stepsto^+& \reason{\mlab{Resume}, \mlab{PureCont}, \mlab{Let}}\\
&\bl
\cek{\Do\;\Await\,\Unit \mid \env_0' \mid \kappa'}\\
\cek{\Do\;\Await\,\Unit \mid \env_\consf' \mid ([(\env_\consf',x,\If\;b\cdots)], \chi^\dagger_\Pipe) \cons (\nil,\chi^\param_\incr) \cons (\nil, \chi_\nondet) \cons \kappa_0'}\\
\text{where }
\ba[t]{@{~}r@{~}c@{~}l}
\env_0' &=& \env_0[b \mapsto \True]\\
\kappa' &=& [([(\env_0',x,\If\;\cdots)], \chi^\dagger_\Pipe),(\nil,\chi^\param_\incr),(\nil, \chi_\nondet)] \concat \kappa_0'
\env_\consf' &=& \env_\consf[b \mapsto \True]\\
\ea
\el\\
\stepsto^+& \reason{\mlab{Forward}, \mlab{Do^\dagger}}\\
\el
\end{derivation}
%
At this stage the context of $\consf$ has been restored with $b$ being
bound to the value $\True$. The pure continuation running under
$\Pipe$ has been extended with pure frame corresponding to the
continuation of the $\Let$-binding of the $\Await$
invocation. Handling of this invocation requires no use of the
forwarding continuation as the top-most frame contains a suitable
handler.
%
\begin{derivation}
\stepsto& \reason{\mlab{Do^\dagger}}\\
&\bl
\cek{\Copipe\,\Record{resume;p} \mid \env_\Pipe' \mid \kappa'}\\
\cek{\Copipe\,\Record{resume;p} \mid \env_\Pipe' \mid (\nil,\chi^\param_\incr) \cons (\nil, \chi_\nondet) \cons \kappa_0'}\\
\text{where }
\ba[t]{@{~}r@{~}c@{~}l}
\env_\Pipe' &=& \env_\Pipe[resume \mapsto (\nil, [(\env_0',x,\If\;\cdots)])]\\
\kappa' &=& [(\nil,\chi^\param_\incr),(\nil, \chi_\nondet)] \concat \kappa_0'
\env_\Pipe' &=& \env_\Pipe[resume \mapsto (\nil, [(\env_\consf',x,\If\;b\cdots)])]\\
\ea
\el\\
\el
\end{derivation}
%
Now the $\Await$-case of the $\Pipe$ handler has been activated. The
resumption $resume$ is bound to the shallow resumption in the
environment. The generalised continuation component of the shallow
resumption is empty, because no forwarding was involved in locating
the handler. The next transitions install the $\Copipe$ handler and
runs the producer computation.
%
\begin{derivation}
\stepsto^+& \reason{\mlab{App}, \mlab{Handle^\dagger}}\\
&\bl
\cek{p\,\Unit \mid \env_\Copipe \mid (\nil, \chi^\dagger_\Copipe) \cons \kappa'}\\
\cek{p\,\Unit \mid \env_\Copipe' \mid (\nil, \chi^\dagger_\Copipe) \cons \kappa'}\\
\text{where }
\ba[t]{@{~}r@{~}c@{~}l}
\env_\Copipe &=& \env_0[c \mapsto (\nil, [(\env_0',x,\If\;\cdots)]), p \mapsto (\env_0,\prodf)]\\
\chi_\Copipe &=& (\env_\Copipe,H^\dagger_\Copipe)\\
\env_\Copipe' &=& \env_\Copipe[c \mapsto (\nil, [(\env_\consf',x,\If\;b\cdots)])]\\
% \chi_\Copipe &=& (\env_\Copipe,H^\dagger_\Copipe)\\
\ea
\el\\
\stepsto^+& \reason{\mlab{AppRec}, \mlab{Let}}\\
&\cek{\Do\;\Incr\,\Unit \mid \env_0 \mid ([(\env_0,i,\Let\;x\revto\cdots)],\chi^\dagger_\Copipe) \cons \kappa'}\\
&\cek{\Do\;\Incr\,\Unit \mid \env_\prodf \mid ([(\env_\prodf,j,\Let\;x\revto\cdots)],\chi^\dagger_\Copipe) \cons \kappa'}\\
\stepsto^+& \reason{\mlab{Forward}, \mlab{Do^\param}, \mlab{Let}, \mlab{App}, \mlab{PureCont}}\\
&\bl
\cek{resume\,\Record{1;0} \mid \env_\incr' \mid (\nil, \chi_\nondet) \cons \kappa_0'}\\
\cek{resume\,\Record{i';i} \mid \env_\incr' \mid (\nil, \chi_\nondet) \cons \kappa_0'}\\
\text{where }
\ba[t]{@{~}r@{~}c@{~}l}
\env_\incr' &=& \env_\incr[i' \mapsto 1, resume \mapsto [([(\env_0,i,\Let\;x\revto\cdots)],\chi^\dagger_\Copipe),(\nil,\chi^\param_\incr)]]
\env_\incr' &=& \env_\incr[\bl
i \mapsto 1, i' \mapsto 2,\\
resume \mapsto [([(\env_\prodf,j,\Let\;x\revto\cdots)],\chi^\dagger_\Copipe),(\nil,\chi^\param_\incr)]]
\el
\ea
\el
\end{derivation}
%
The producer computation performs the $\Incr$ operation, which
requires one $\mlab{Forward}$ transition in order to locate a suitable
handler for it. The $\Incr$-case of the $\incr$ handler increments the
counter $i$ by one. The environment binds the current value of the
counter. The following $\mlab{Resume^\param}$ transition updates the
counter value to be that of $i'$ and continues the producer
computation.
%
\begin{derivation}
\stepsto^+&\reason{\mlab{Resume^\param}, \mlab{PureCont}, \mlab{Let}}\\
&\bl
\cek{\Do\;\Yield~i \mid \env_{\prodf}' \mid ([(\env_{\prodf}',x,\prodf\,\Unit)],\chi^\dagger_\Copipe) \cons \kappa_1}\\
\cek{\Do\;\Yield~j \mid \env_{\prodf}'' \mid ([(\env_{\prodf}'',x,\prodf\,\Unit)],\chi^\dagger_\Copipe) \cons (\nil,\chi^\param_\incr) \cons (\nil, \chi_\nondet) \cons \kappa_0'}\\
\text{where }
\ba[t]{@{~}r@{~}c@{~}l}
\env_\prodf' &=& \env_\prodf[i \mapsto 0]\\
\kappa_1 &=& ([(\env_0,x,\If\;b\cdots)],\chi^\dagger_\Copipe) \cons (\nil,\chi^\param_\incr) \cons (\nil, \chi_\nondet) \cons \kappa_0'
\env_\prodf'' &=& \env_\prodf'[j \mapsto 1]\\
\ea
\el\\
\stepsto& \reason{\mlab{Do^\dagger}}\\
&\bl
\cek{\Pipe\,\Record{resume;\lambda\Unit.c\,y} \mid \env_\Copipe' \mid \kappa_1}\\
\cek{\Pipe\,\Record{resume;\lambda\Unit.c\,y} \mid \env_\Pipe' \mid (\nil,\chi^\param_\incr) \cons (\nil, \chi_\nondet) \cons \kappa_0'}\\
\text{where }
\ba[t]{@{~}r@{~}c@{~}l}
\env_\Copipe' &=& \env_\Copipe[y \mapsto 0, resume \mapsto (\nil,[(\env_{\prodf}',x,\prodf\,\Unit)])]
\env_\Pipe' &=& \env_\Pipe[y \mapsto 1, resume \mapsto (\nil,[(\env_{\prodf}'',x,\prodf\,\Unit)])]
\ea
\el\\
\stepsto^+& \reason{\mlab{App}, \mlab{Handle^\dagger}, \mlab{Resume^\dagger}, \mlab{PureCont}}\\
&\bl
\cek{\If\;b\;\Then\;x + 2\;\Else\;x*2 \mid \env_\consf'' \mid \kappa_2}\\
\cek{\If\;b\;\Then\;x + 2\;\Else\;x*2 \mid \env_\consf'' \mid (\nil, \chi^\dagger_\Pipe) \cons (\nil,\chi^\param_\incr) \cons (\nil, \chi_\nondet) \cons \kappa_0'}\\
\text{where }
\ba[t]{@{~}r@{~}c@{~}l}
\env_\consf'' &=& \env_\consf[x \mapsto 0]\\
\kappa_2 &=& ([(\env_0,i,\Let\;x\revto\cdots)],\chi^\dagger_\Pipe) \cons (\nil,\chi^\param_\incr) \cons (\nil, \chi_\nondet) \cons \kappa_0'
\env_\consf'' &=& \env_\consf[x \mapsto 1]
\ea
\el
\end{derivation}
%
% \paragraph{Example} To make the transition rules in
% Figure~\ref{fig:abstract-machine-semantics} concrete we give an
% example of the abstract machine in action. We reuse the small producer
% and consumer from Section~\ref{sec:shallow-handlers-tutorial}. We
% reproduce their definitions here in ANF.
% %
% \[
% \bl
% \Ones \defas \Rec\;ones~\Unit. \Do\; \Yield~1; ones~\Unit \\
% \AddTwo \defas
% \lambda \Unit.
% \Let\; x \revto \Do\;\Await~\Unit \;\In\;
% \Let\; y \revto \Do\;\Await~\Unit \;\In\;
% x + y \\
% \el
% \]%
% %
% Let $N_x$ denote the term $\Let\;x \revto \Do\;\Await~\Unit\;\In\;N_y$
% and $N_y$ the term $\Let\;y \revto \Do\;\Await~\Unit\;\In\;x+y$.
% %
% %% For clarity, we annotate each bound variable $resume$ with a subscript
% %% $\Await$ or $\Yield$ according to whether it was captured by a
% %% consumer or a producer.
% %
% Suppose $\Ones$, $\AddTwo$, $\Pipe$, and $\Copipe$ are bound in
% $\env_\top$. Furthermore, let $H_\Pipe$ and $H_\Copipe$ denote the
% pipe and copipe handler definitions. The machine begins by applying
% $\Pipe$.
% %
% \begin{derivation}
% &\cek{\Pipe~\Record{\Ones, \AddTwo} \mid \env_\top \mid \kappaid}\\
% \stepsto& \reason{apply $\Pipe$}\\
% &\cek{\ShallowHandle\;c~\Unit\;\With\;H_\Pipe \mid \env_\top[c \mapsto (\emptyset, \AddTwo), p \mapsto (\emptyset, \Ones)] \mid \kappaid}\\
% \stepsto& \reason{install $H_\Pipe$ with $\env_\Pipe = \env_\top[c \mapsto (\emptyset, \AddTwo), p \mapsto (\emptyset, \Ones)]$}\\
% &\cek{c~\Unit \mid \env_\Pipe \mid (\nil, (\env_\Pipe, H_\Pipe)) \cons \kappaid}\\
% \stepsto& \reason{apply $c$ and $\val{c}\env_\Pipe = (\emptyset, \AddTwo)$}\\
% &\cek{N_x \mid \emptyset \mid (\nil, (\env_\Pipe, H_\Pipe)) \cons \kappaid}\\
% \stepsto& \reason{focus on left operand}\\
% &\cek{\Do\;\Await~\Unit \mid \emptyset \mid ([(\emptyset, x, N_y)], (\env_\Pipe, H_\Pipe)) \cons \kappaid}\\
% \stepsto& \reason{shallow continuation capture $v_\Await = (\nil, [(\emptyset, x, N_y)])$}\\
% &\cek{\Copipe~\Record{resume, p} \mid \env_\Pipe[resume \mapsto v_\Await] \mid \kappaid}\\
% \end{derivation}
% %
% The invocation of $\Await$ begins a search through the machine
% continuation to locate a matching handler. In this instance the
% top-most handler $H_\Pipe$ handles $\Await$. The complete shallow
% resumption consists of an empty continuation and a singleton pure
% continuation. The former is empty as $H_\Pipe$ is a shallow handler,
% meaning that it is discarded.
% Evaluation continues by applying $\Copipe$.
% %
% \begin{derivation}
% \stepsto& \reason{apply $\Copipe$}\\
% &\cek{\ShallowHandle\; p~\Unit \;\With\;H_\Copipe \mid \env_\top[c \mapsto v_\Await, p \mapsto (\emptyset, \Ones)] \mid \kappaid}\\
% \stepsto& \reason{install $H_\Copipe$ with $\env_\Copipe = \env_\top[c \mapsto v_\Await, p \mapsto (\emptyset, \Ones)]$}\\
% &\cek{p~\Unit \mid \env_\Copipe \mid (\emptyset, (\env_\Copipe, H_\Copipe)) \cons \kappaid}\\
% \stepsto^2& \reason{apply $p$, $\val{p}\env_\Copipe = (\emptyset, \Ones)$, and $\env_{\Ones} = \emptyset[ones \mapsto (\emptyset, \Ones)]$}\\
% % &\cek{\Do\;\Yield~1;~ones~\Unit \mid \env_{ones} \mid (\nil, (\env_\Copipe, H_\Copipe)) \cons \kappaid}\\
% % \stepsto^2& \reason{focus on $\Yield$}\\
% &\cek{\Do\;\Yield~1 \mid \env_{\Ones} \mid ([(\env_{\Ones},\_,ones~\Unit)], (\env_\Copipe, H_\Copipe)) \cons \kappaid}\\
% \stepsto& \reason{shallow continuation capture $v_\Yield = (\nil, [(\env_{\Ones}, \_, ones~\Unit)])$}\\
% &\cek{\Pipe~\Record{resume, \lambda\Unit.c~s} \mid \env_\Copipe[s \mapsto 1,resume \mapsto v_\Yield] \mid \kappaid}
% \end{derivation}
% %
% At this point the situation is similar as before: the invocation of
% $\Yield$ causes the continuation to be unwound in order to find an
% appropriate handler, which happens to be $H_\Copipe$. Next $\Pipe$ is
% applied.
% %
% \begin{derivation}
% \stepsto& \reason{apply $\Pipe$ and $\env_\Pipe' = \env_\top[c \mapsto (\env_\Copipe[c \mapsto v_\Await, s\mapsto 1]), p \mapsto v_\Yield])]$}\\
% &\cek{\ShallowHandle\;c~\Unit\;\With\; H_\Pipe \mid \env_\Pipe' \mid \kappaid}\\
% \stepsto& \reason{install $H_\Pipe$}\\
% &\cek{c~\Unit \mid \env_\Pipe' \mid (\nil, (\env_\Pipe', H_\Pipe)) \cons \kappaid}\\
% \stepsto& \reason{apply $c$ and $\val{c}\env_\Pipe' = (\env_\Copipe[c \mapsto v_\Await, s\mapsto 1])$}\\
% &\cek{c~s \mid \env_\Copipe[c \mapsto v_\Await, s\mapsto 1] \mid (\nil, (\env_\Pipe', H_\Pipe)) \cons \kappaid}\\
% \stepsto& \reason{shallow resume with $v_\Await = (\nil, [(\emptyset,x,N_y)])$}\\
% &\cek{\Return\;1 \mid \env_\Pipe' \mid ([(\emptyset,x,N_y)], (\env_\Pipe', H_\Pipe)) \cons \kappaid}
% \end{derivation}
% %
% Applying the resumption concatenates the first component (the
% continuation) with the machine continuation. The second component
% (pure continuation) gets concatenated with the pure continuation of
% the top-most frame of the machine continuation. Thus in this
% particular instance, the machine continuation is manipulated as
% follows.
% %
% \[
% \ba{@{~}l@{~}l}
% &\nil \concat ([(\emptyset,x,N_y)] \concat \nil, (\env_\Pipe', H_\Pipe)) \cons \kappaid\\
% =& ([(\emptyset,x,N_y)], (\env_\Pipe', H_\Pipe)) \cons \kappaid
% \ea
% \]
% %
% Because the control component contains the expression $\Return\;1$ and
% the pure continuation is nonempty, the machine applies the pure
% continuation.
% \begin{derivation}
% \stepsto& \reason{apply pure continuation, $\env_{\AddTwo} = \emptyset[x \mapsto 1]$}\\
% &\cek{N_y \mid \env_{\AddTwo} \mid (\nil, (\env_\Pipe', H_\Pipe)) \cons \kappaid}\\
% \stepsto& \reason{focus on right operand}\\
% &\cek{\Do\;\Await~\Unit \mid \env_{\AddTwo} \mid ([(\env_{\AddTwo}, y, x + y)], (\env_\Pipe', H_\Pipe)) \cons \kappaid}\\
% \stepsto^2& \reason{shallow continuation capture $w_\Await = (\nil, [(\env_{\AddTwo}, y, x + y)])$, apply $\Copipe$}\\
% &\cek{\ShallowHandle\;p~\Unit \;\With\; \env_\Copipe \mid \env_\top[c \mapsto w_\Await, p \mapsto v_\Yield] \mid \kappaid}\\
% \reducesto& \reason{install $H_\Copipe$ with $\env_\Copipe = \env_\top[c \mapsto w_\Await, p \mapsto v_\Yield]$}\\
% &\cek{p~\Unit \mid \env_\Copipe \mid (\nil, (\env_\Copipe, H_\Copipe)) \cons \kappaid}
% \end{derivation}
% %
% The variable $p$ is bound to the shallow resumption $v_\Yield$, thus
% invoking it will transfer control back to the $\Ones$ computation.
% %
% \begin{derivation}
% \stepsto & \reason{shallow resume with $v_\Yield = (\nil, [(\env_{\Ones}, \_, ones~\Unit)])$}\\
% &\cek{\Return\;\Unit \mid \env_\Copipe \mid ([(\env_{\Ones}, \_, ones~\Unit)], (\env_\Copipe, H_\Copipe)) \cons \kappaid}\\
% \stepsto^3& \reason{apply pure continuation, apply $ones$, focus on $\Yield$}\\
% &\cek{\Do\;\Yield~1 \mid \env_{\Ones} \mid ([(\env_{\Ones}, \_, ones~\Unit)], (\env_\Copipe, H_\Copipe)) \cons \kappaid}\\
% \end{derivation}
% %
% At this stage the machine repeats the transitions from before: the
% shallow continuation of $\Do\;\Yield~1$ is captured, control passes to
% the $\Yield$ clause in $H_\Copipe$, which again invokes $\Pipe$ and
% subsequently installs the $H_\Pipe$ handler with an environment
% $\env_\Pipe''$. The handler runs the computation $c~\Unit$, where $c$
% is an abstraction over the resumption $w_\Await$ applied to the
% yielded value $1$.
% %
% \begin{derivation}
% \stepsto^6 & \reason{by the above reasoning, shallow resume with $w_\Await = (\nil, [(\env_{\AddTwo}, y, x + y)])$}\\
% &\cek{x + y \mid \env_{\AddTwo}[y \mapsto 1] \mid (\nil, (\env_\Pipe'', H_\Pipe)) \cons \kappaid}\\
% \stepsto& \reason{$\val{x}\env_{\AddTwo}[y\mapsto 1] = 1$ and $\val{y}\env_{\AddTwo}[y\mapsto 1] = 1$}\\
% &\cek{\Return\;2 \mid \env_{\AddTwo}[y \mapsto 1] \mid (\nil, (\env_\Pipe'', H_\Pipe)) \cons \kappaid}
% \end{derivation}
% %
% Since the pure continuation is empty the $\Return$ clause of $H_\Pipe$
% gets invoked with the value $2$. Afterwards the $\Return$ clause of the
% identity continuation in $\kappaid$ is invoked, ultimately
% transitioning to the following final configuration.
% %
% \begin{derivation}
% \stepsto^2& \reason{by the above reasoning}\\
% &\cek{\Return\;2 \mid \emptyset \mid \nil}
% \end{derivation}
% %
% %\env_\top[c \mapsto (\env_\Copipe, \lambda\Unit.w_\Await~1),p \mapsto (\nil, [(\env_{\Ones}, \_, ones~\Unit)])]
% \paragraph{Remark} If the main continuation is empty then the machine gets
% stuck. This occurs when an operation is unhandled, and the forwarding
% continuation describes the succession of handlers that have failed to
% handle the operation along with any pure continuations that were
% encountered along the way.
% %
% Assuming the input is a well-typed closed computation term $\typc{}{M
% : A}{E}$, the machine will either not terminate, return a value of
% type $A$, or get stuck failing to handle an operation appearing in
% $E$. We now make the correspondence between the operational semantics
% and the abstract machine more precise.
The $\Yield$ operation causes another instance of the $\Pipe$ to be
installed in place of the $\Copipe$. The $\mlab{Resume^\dagger}$
transition occurs because the consumer argument provided to $\Pipe$ is
the resumption of captured by the original instance of $\Pipe$, thus
invoking it causes the context of the original consumer computation to
be restored. Since $b$ is $\True$ the $\If$-expression will dispatch
to the $\Then$-branch, meaning the computation will ultimately return
$2$. This return value gets propagated through the handler stack.
%
\begin{derivation}
\stepsto^+& \reason{\mlab{Case}, \mlab{App}, \mlab{GenCont}, \mlab{GenCont}, \mlab{GenCont}}\\
&\cek{\Return\;[x] \mid \env_\nondet[x \mapsto 2] \mid \kappa_0'}
\end{derivation}
%
The $\Return$-clauses of the $\Pipe$ and $\incr$ handlers are
identities, and thus, the return value $x$ passes through
unmodified. The $\Return$-case of $\nondet$ lifts the value into a
singleton list. Next the pure continuation is invoked, which restores
the handling context of the first operation invocation $\Fork$.
%
\begin{derivation}
\stepsto& \reason{\mlab{PureCont}, \mlab{Let}}\\
&\bl
\cek{resume~\False \mid \env_\nondet' \mid \kappa_0''}\\
\text{where }
\ba[t]{@{~}r@{~}c@{~}l}
\env_\nondet'' &=& \env_\nondet'[xs \mapsto [3]]\\
\kappa_0'' &=& [([(\env_\nondet'',ys,xs \concat ys)],\chiid)]
\ea
\el\\
\stepsto^+& \reason{\mlab{Resume}, \mlab{PureCont}, \mlab{Let}}\\
&\bl
\cek{\Do\;\Await\,\Unit \mid \env_\consf''' \mid ([(\env_\consf''',x,\If\;b\cdots)], \chi^\dagger_\Pipe) \cons (\nil, \chi^\param_\incr) \cons (\nil, \chi_\nondet) \cons \kappa_0''}\\
\text{where }
\ba[t]{@{~}r@{~}c@{~}l}
\env_\consf''' &=& \env_\consf''[b \mapsto \False]\\
\ea
\el\\
\end{derivation}
%
The second invocation of the resumption $resume$ interprets $\Fork$ as
$\False$. The consumer computation is effectively restarted with $b$
bound to $\False$. The previous transitions will be repeated.
%
\begin{derivation}
\stepsto^+ & \reason{same reasoning as above}\\
&\bl
\cek{resume\,\Record{i';i} \mid \env_\incr'' \mid (\nil, \chi_\nondet) \cons \kappa_0''}\\
\text{where }
\ba[t]{@{~}r@{~}c@{~}l}
\env_\incr' &=& \env_\incr[\bl
i \mapsto 2, i' \mapsto 3,\\
resume \mapsto [([(\env_\prodf'',i,\Let\;x\revto\cdots)],\chi^\dagger_\Copipe),(\nil,\chi^\param_\incr)]]\el
\ea
\el
\end{derivation}
%
After some amount transitions the parameterised handler $\incr$ will
be activated again. The counter variable $i$ is bound to the value
computed during the previous activation of the handler. The machine
proceeds as before and eventually reaches concatenation application
inside the $\Fork$-case.
%
\begin{derivation}
\stepsto^+& \reason{same reasoning as above}\\
&\bl
\cek{xs \concat ys \mid \env_\nondet'' \mid \kappa_0}\\
\text{where }
\ba[t]{@{~}r@{~}c@{~}l}
\env_\nondet'' &=& \env_\nondet'[ys \mapsto [4]]
\ea
\el\\
\stepsto& \reason{\mlab{App}, \mlab{GenCont}, \mlab{Halt}}\\
& [3,4]
\end{derivation}
%
\section{Realisability and efficiency implications}
\label{subsec:machine-realisability}

Write Preview
Loading…
Cancel
Save