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

Simplify CPS

master
Daniel Hillerström 5 years ago
parent
7f99b18242
commit
1b2882b1eb
2 changed files with 95 additions and 53 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Unified View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 5
      macros.tex
  2. 143
      thesis.tex

5
macros.tex
View File

@ -306,8 +306,9 @@
% Canonical variables for handler components % Canonical variables for handler components
\newcommand{\vhret}{h^{\mret}} \newcommand{\vhret}{h^{\mret}}
\newcommand{\vhops}{h^{\mops}} \newcommand{\vhops}{h^{\mops}}
\newcommand{\svhret}{\chi^{\mret}}
\newcommand{\svhops}{\chi^{\mops}}
\newcommand{\sv}{\chi}
\newcommand{\svhret}{\sv^{\mret}}
\newcommand{\svhops}{\sv^{\mops}}
% \newcommand{\dk}{\dRecord{fs,\dRecord{\vhret,\vhops}}} % \newcommand{\dk}{\dRecord{fs,\dRecord{\vhret,\vhops}}}
\newcommand{\dk}{k} \newcommand{\dk}{k}

143
thesis.tex
View File

@ -9100,9 +9100,9 @@ matching notation. The static meta language is generated by the
following productions. following productions.
% %
\begin{syntax} \begin{syntax}
\slab{Static patterns} &\sP \in \SPatCat &::=& \sks \mid \sk \scons \sP\\
\slab{Static values} & \sV, \sW \in \SValCat &::=& \reflect V \mid \sV \scons \sW \mid \slam \sP. \sM\\
\slab{Static computations} & \sM \in \SCompCat &::=& \sV \mid \sV \sapp \sW \mid \sV \dapp V \dapp W
\slab{Static\text{ }patterns} &\sP \in \SPatCat &::=& \sks \mid \sk \scons \sP\\
\slab{Static\text{ }values} & \sV, \sW \in \SValCat &::=& \reflect V \mid \sV \scons \sW \mid \slam \sP. \sM\\
\slab{Static\text{ }computations} & \sM \in \SCompCat &::=& \sV \mid \sV \sapp \sW \mid \sV \dapp V \dapp W
\end{syntax} \end{syntax}
% %
The patterns comprise only static list deconstructing. We let $\sP$ The patterns comprise only static list deconstructing. We let $\sP$
@ -10027,11 +10027,11 @@ first-class objects, but rather as a special kinds of functions.
\begin{equations} \begin{equations}
\cps{\Return\,V} &\defas& \slam \shk.\kapp\;(\reify \shk)\;\cps{V} \\ \cps{\Return\,V} &\defas& \slam \shk.\kapp\;(\reify \shk)\;\cps{V} \\
\cps{\Let~x \revto M~\In~N} &\defas& \cps{\Let~x \revto M~\In~N} &\defas&
\bl\slam \sRecord{\shf, \sRecord{\svhret, \svhops}} \scons \shk.
\bl\slam \sRecord{\shf, \sv} \scons \shk.
\ba[t]{@{}l} \ba[t]{@{}l}
\cps{M} \sapp (\sRecord{\bl\reflect((\dlam x\,\dhk.\bl\Let\;(\dk \dcons \dhk') = \dhk\;\In\\ \cps{M} \sapp (\sRecord{\bl\reflect((\dlam x\,\dhk.\bl\Let\;(\dk \dcons \dhk') = \dhk\;\In\\
\cps{N} \sapp (\reflect\dk \scons \reflect \dhk')) \el\\ \cps{N} \sapp (\reflect\dk \scons \reflect \dhk')) \el\\
\dcons \reify\shf), \sRecord{\svhret, \svhops}} \scons \shk)\el
\dcons \reify\shf), \sv} \scons \shk)\el
\ea \ea
\el\\ \el\\
\cps{\Do\;\ell\;V} &\defas& \cps{\Do\;\ell\;V} &\defas&
@ -10083,7 +10083,10 @@ The CPS translation is given in
Figure~\ref{fig:cps-higher-order-uncurried-simul}. In essence, it is Figure~\ref{fig:cps-higher-order-uncurried-simul}. In essence, it is
the same as the CPS translation for deep effect handlers as described the same as the CPS translation for deep effect handlers as described
in Section~\ref{sec:higher-order-uncurried-deep-handlers-cps}, though in Section~\ref{sec:higher-order-uncurried-deep-handlers-cps}, though
it is adjusted to account for generalised continuation representation.
it is adjusted to account for generalised continuation
representation. For notational convenience, we write $\chi$ to denote
a statically known effect continuation frame
$\sRecord{\svhret,\svhops}$.
% %
The translation of $\Return$ invokes the continuation $\shk$ using the The translation of $\Return$ invokes the continuation $\shk$ using the
continuation application primitive $\kapp$. continuation application primitive $\kapp$.
@ -10092,8 +10095,9 @@ The translations of deep and shallow handlers differ only in their use
of the resumption construction primitive. of the resumption construction primitive.
A major aesthetic improvement due to the generalised continuation A major aesthetic improvement due to the generalised continuation
representation is that continuation construction and deconstruction is
now uniform: only a single continuation frame is inspected at a time.
representation is that continuation construction and deconstruction
are now uniform: only a single continuation frame is inspected at a
time.
\subsubsection{Correctness} \subsubsection{Correctness}
\label{sec:cps-gen-cont-correctness} \label{sec:cps-gen-cont-correctness}
@ -10110,7 +10114,9 @@ element is always known statically, i.e., it is of the form
$\sRecord{\sV_{fs}, \sRecord{\sV_{\mret},\sV_{\mops}}} \scons $\sRecord{\sV_{fs}, \sRecord{\sV_{\mret},\sV_{\mops}}} \scons
\sW$. Moreover, the static values $\sV_{fs}$, $\sV_{\mret}$, and \sW$. Moreover, the static values $\sV_{fs}$, $\sV_{\mret}$, and
$\sV_{\mops}$ are all reflected dynamic terms (i.e., of the form $\sV_{\mops}$ are all reflected dynamic terms (i.e., of the form
$\reflect V$). This fact is used implicitly in the proofs.
$\reflect V$). This fact is used implicitly in the proofs. For brevity
we write $\sV_f$ to denote a statically known continuation frame
$\sRecord{\sV_{fs}, \sRecord{\sV_{\mret},\sV_{\mops}}}$.
% %
\begin{lemma}[Substitution]\label{lem:subst-gen-cont} \begin{lemma}[Substitution]\label{lem:subst-gen-cont}
@ -10124,8 +10130,10 @@ $\reflect V$). This fact is used implicitly in the proofs.
and with substitution in computation terms and with substitution in computation terms
\[ \[
\ba{@{}l@{~}l} \ba{@{}l@{~}l}
&(\cps{M} \sapp (\sRecord{\sV_{fs},\sRecord{\sV_{\mret},\sV_{\mops}}} \scons \sW))[\cps{V}/x]\\
= &\cps{M[V/x]} \sapp (\sRecord{\sV_{fs},\sRecord{\sV_{\mret},\sV_{\mops}}} \scons\sW)[\cps{V}/x],
% &(\cps{M} \sapp (\sRecord{\sV_{fs},\sRecord{\sV_{\mret},\sV_{\mops}}} \scons \sW))[\cps{V}/x]\\
% = &\cps{M[V/x]} \sapp (\sRecord{\sV_{fs},\sRecord{\sV_{\mret},\sV_{\mops}}} \scons\sW)[\cps{V}/x],
&(\cps{M} \sapp (\sV_f \scons \sW))[\cps{V}/x]\\
= &\cps{M[V/x]} \sapp (\sV_f \scons \sW)[\cps{V}/x],
\ea \ea
\] \]
% %
@ -10150,10 +10158,10 @@ the same translations as for the corresponding constructs in $\SCalc$.
\cps{\Let\; x \revto \EC \;\In\; N} \cps{\Let\; x \revto \EC \;\In\; N}
&=& &=&
\begin{array}[t]{@{}l} \begin{array}[t]{@{}l}
\slam \sRecord{\shf, \sRecord{\svhret, \svhops}} \scons \shk.\\
\slam \sRecord{\shf, \sv} \scons \shk.\\
\quad \cps{\EC} \sapp (\bl\sRecord{\reflect((\dlam x\,\dhk.\bl\Let\;\dRecord{fs,\dRecord{\vhret,\vhops}}\dcons \dhk'=\dhk\;\In\\ \quad \cps{\EC} \sapp (\bl\sRecord{\reflect((\dlam x\,\dhk.\bl\Let\;\dRecord{fs,\dRecord{\vhret,\vhops}}\dcons \dhk'=\dhk\;\In\\
\cps{N} \sapp (\sRecord{\reflect fs, \sRecord{\reflect \vhret, \reflect \vhops}} \scons \reflect \dhk')) \dcons \reify\shf),\el\\ \cps{N} \sapp (\sRecord{\reflect fs, \sRecord{\reflect \vhret, \reflect \vhops}} \scons \reflect \dhk')) \dcons \reify\shf),\el\\
\sRecord{\svhret,\svhops}} \scons \shk)\el
\sv} \scons \shk)\el
\end{array} \end{array}
\\ \\
\cps{\Handle^\depth\; \EC \;\With\; H} \cps{\Handle^\depth\; \EC \;\With\; H}
@ -10169,9 +10177,12 @@ context.
\begin{lemma}[Evaluation context decomposition] \begin{lemma}[Evaluation context decomposition]
\label{lem:decomposition-gen-cont} \label{lem:decomposition-gen-cont}
\[ \[
\cps{\EC[M]} \sapp (\sRecord{\sV_{fs}, \sRecord{\sV_{\mret},\sV_{\mops}}} \scons \sW)
% \cps{\EC[M]} \sapp (\sRecord{\sV_{fs}, \sRecord{\sV_{\mret},\sV_{\mops}}} \scons \sW)
% =
% \cps{M} \sapp (\cps{\EC} \sapp (\sRecord{\sV_{fs}, \sRecord{\sV_{\mret},\sV_{\mops}}} \scons \sW))
\cps{\EC[M]} \sapp (\sV_f \scons \sW)
= =
\cps{M} \sapp (\cps{\EC} \sapp (\sRecord{\sV_{fs}, \sRecord{\sV_{\mret},\sV_{\mops}}} \scons \sW))
\cps{M} \sapp (\cps{\EC} \sapp (\sV_f \scons \sW))
\] \]
\end{lemma} \end{lemma}
% %
@ -10191,11 +10202,14 @@ continuation is known.
% %
\begin{lemma}[Reflect after reify] \begin{lemma}[Reflect after reify]
\label{lem:reflect-after-reify-gen-cont} \label{lem:reflect-after-reify-gen-cont}
%
\[ \[
\cps{M} \sapp (\sRecord{\sV_{fs}, \sRecord{\sV_{\mret},\sV_{\mops}}} \scons \reflect \reify \sW)
% \cps{M} \sapp (\sRecord{\sV_{fs}, \sRecord{\sV_{\mret},\sV_{\mops}}} \scons \reflect \reify \sW)
% =
% \cps{M} \sapp (\sRecord{\sV_{fs}, \sRecord{\sV_{\mret},\sV_{\mops}}} \scons \sW).
\cps{M} \sapp (\sV_f \scons \reflect \reify \sW)
= =
\cps{M} \sapp (\sRecord{\sV_{fs}, \sRecord{\sV_{\mret},\sV_{\mops}}} \scons \sW).
\cps{M} \sapp (\sV_f \scons \sW).
\] \]
\end{lemma} \end{lemma}
@ -10228,27 +10242,49 @@ dynamic language, as described above.
\begin{lemma}[Handling]\label{lem:handle-op-gen-cont} \begin{lemma}[Handling]\label{lem:handle-op-gen-cont}
Suppose $\ell \notin BL(\EC)$ and $\hell = \{\ell\,p\,r \mapsto N_\ell\}$. If $H$ is deep then Suppose $\ell \notin BL(\EC)$ and $\hell = \{\ell\,p\,r \mapsto N_\ell\}$. If $H$ is deep then
% %
% \[
% \bl
% \cps{\Do\;\ell\;V} \sapp (\cps{\EC} \sapp (\sRecord{\snil, \cps{H}} \scons \sRecord{\sV_{fs},\sRecord{\sV_{\mret},\sV_{\mops}}} \scons \sW)) \reducesto^+ \\
% \quad (\cps{N_\ell} \sapp \sRecord{\sV_{fs},\sRecord{\sV_{\mret},\sV_{\mops}}} \scons \sW)\\
% \qquad \quad [\cps{V}/p,
% \dlam x\,\dhk.\bl
% \Let\;\dRecord{fs, \dRecord{\vhret, \vhops}} \dcons \dhk' = \dhk\;\In\;\\
% \cps{\Return\;x} \sapp (\cps{\EC} \sapp (\sRecord{\snil, \cps{H}} \scons \sRecord{\reflect \dlk, \sRecord{\reflect \vhret, \reflect \vhops}} \scons \reflect\dhk'))/r]. \\
% \el\\
% \el
% \]
\[ \[
\bl \bl
\cps{\Do\;\ell\;V} \sapp (\cps{\EC} \sapp (\sRecord{\snil, \cps{H}} \scons \sRecord{\sV_{fs},\sRecord{\sV_{\mret},\sV_{\mops}}} \scons \sW)) \reducesto^+ \\
\quad (\cps{N_\ell} \sapp \sRecord{\sV_{fs},\sRecord{\sV_{\mret},\sV_{\mops}}} \scons \sW)\\
\qquad \quad [\cps{V}/p,
\cps{\Do\;\ell\;V} \sapp (\cps{\EC} \sapp (\sRecord{\snil, \cps{H}} \scons \sV_f \scons \sW)) \reducesto^+ \\
\quad (\cps{N_\ell} \sapp (\sV_f \scons \sW))
[\cps{V}/p,
\dlam x\,\dhk.\bl \dlam x\,\dhk.\bl
\Let\;\dRecord{fs, \dRecord{\vhret, \vhops}} \dcons \dhk' = \dhk\;\In\;\\
\cps{\Return\;x} \sapp (\cps{\EC} \sapp (\sRecord{\snil, \cps{H}} \scons \sRecord{\reflect \dlk, \sRecord{\reflect \vhret, \reflect \vhops}} \scons \reflect\dhk'))/r]. \\
\Let\;\dRecord{fs, \dRecord{\vhret, \vhops}} \dcons \dhk' = \dhk\;\In\;
\cps{\Return\;x}\\
\sapp (\cps{\EC} \sapp (\sRecord{\snil, \cps{H}} \scons \sRecord{\reflect \dlk, \sRecord{\reflect \vhret, \reflect \vhops}} \scons \reflect\dhk'))/r]. \\
\el\\ \el\\
\el \el
\] \]
% %
Otherwise if $H$ is shallow then Otherwise if $H$ is shallow then
% %
\[
% \[
% \bl
% \cps{\Do\;\ell\;V} \sapp (\cps{\EC} \sapp (\sRecord{\snil, \cps{H}^\dagger} \scons \sRecord{\sV_{fs},\sRecord{\sV_{\mret},\sV_{\mops}}} \scons \sW)) \reducesto^+ \\
% \quad (\cps{N_\ell} \sapp \sRecord{\sV_{fs},\sRecord{\sV_{\mret},\sV_{\mops}}} \scons \sW)\\
% \qquad [\cps{V}/p, \dlam x\,\dhk. \bl
% \Let\;\dRecord{\dlk, \dRecord{\vhret, \vhops}} \dcons \dhk' = \dhk \;\In \\
% \cps{\Return\;x} \sapp (\cps{\EC} \sapp (\sRecord{\reflect \dlk, \sRecord{\reflect \vhret, \reflect \vhops}} \scons \reflect\dhk'))/r]. \\
% \el \\
% \el
% \]
\[
\bl \bl
\cps{\Do\;\ell\;V} \sapp (\cps{\EC} \sapp (\sRecord{\snil, \cps{H}^\dagger} \scons \sRecord{\sV_{fs},\sRecord{\sV_{\mret},\sV_{\mops}}} \scons \sW)) \reducesto^+ \\
\quad (\cps{N_\ell} \sapp \sRecord{\sV_{fs},\sRecord{\sV_{\mret},\sV_{\mops}}} \scons \sW)\\
\qquad [\cps{V}/p, \dlam x\,\dhk. \bl
\Let\;\dRecord{\dlk, \dRecord{\vhret, \vhops}} \dcons \dhk' = \dhk \;\In \\
\cps{\Return\;x} \sapp (\cps{\EC} \sapp (\sRecord{\reflect \dlk, \sRecord{\reflect \vhret, \reflect \vhops}} \scons \reflect\dhk'))/r]. \\
\cps{\Do\;\ell\;V} \sapp (\cps{\EC} \sapp (\sRecord{\snil, \cps{H}^\dagger} \scons \sV_f \scons \sW)) \reducesto^+ \\
\quad (\cps{N_\ell} \sapp (\sV_f \scons \sW))
[\cps{V}/p, \dlam x\,\dhk. \bl
\Let\;\dRecord{\dlk, \dRecord{\vhret, \vhops}} \dcons \dhk' = \dhk \;\In\;\cps{\Return\;x}\\
\sapp (\cps{\EC} \sapp (\sRecord{\reflect \dlk, \sRecord{\reflect \vhret, \reflect \vhops}} \scons \reflect\dhk'))/r]. \\
\el \\ \el \\
\el \el
\] \]
@ -10257,8 +10293,9 @@ Suppose $\ell \notin BL(\EC)$ and $\hell = \{\ell\,p\,r \mapsto N_\ell\}$. If $H
\medskip \medskip
Now the main result for the translation: a simulation result in the
style of \citet{Plotkin75}.
With the aid of the above lemmas we can state and prove the main
result for the translation: a simulation result in the style of
\citet{Plotkin75}.
% %
\begin{theorem}[Simulation] \begin{theorem}[Simulation]
\label{thm:ho-simulation-gen-cont} \label{thm:ho-simulation-gen-cont}
@ -10319,15 +10356,15 @@ $M \reducesto^\ast V$ if and only if $\pcps{M} \reducesto^\ast \pcps{V}$.
\textbf{Computations} \textbf{Computations}
% %
\begin{equations} \begin{equations}
\cps{-} &:& \CompCat \to \UCompCat\\
\cps{\Let~x \revto M~\In~N} &\defas&
\bl\slam \sRecord{\shf, \sRecord{\xi, \svhret, \svhops}} \scons \shk.
\ba[t]{@{}l}
\cps{M} \sapp (\sRecord{\bl\reflect((\dlam x\,\dhk.\bl\Let\;(\dk \dcons \dhk') = \dhk\;\In\\
\cps{N} \sapp (\reflect\dk \scons \reflect \dhk')) \el\\
\dcons \reify\shf), \sRecord{\xi, \svhret, \svhops}} \scons \shk)\el
\ea
\el\\
\cps{-} &:& \CompCat \to \SValCat^\ast \to \UCompCat\\
% \cps{\Let~x \revto M~\In~N} &\defas&
% \bl\slam \sRecord{\shf, \sRecord{\xi, \svhret, \svhops}} \scons \shk.
% \ba[t]{@{}l}
% \cps{M} \sapp (\sRecord{\bl\reflect((\dlam x\,\dhk.\bl\Let\;(\dk \dcons \dhk') = \dhk\;\In\\
% \cps{N} \sapp (\reflect\dk \scons \reflect \dhk')) \el\\
% \dcons \reify\shf), \sRecord{\xi, \svhret, \svhops}} \scons \shk)\el
% \ea
% \el\\
\cps{\Do\;\ell\;V} &\defas& \cps{\Do\;\ell\;V} &\defas&
\slam \sRecord{\shf, \sRecord{\xi, \svhret, \svhops}} \scons \shk.\, \slam \sRecord{\shf, \sRecord{\xi, \svhret, \svhops}} \scons \shk.\,
\reify\svhops \bl\dapp \dRecord{\reify\xi, \ell, \reify\svhops \bl\dapp \dRecord{\reify\xi, \ell,
@ -10420,20 +10457,20 @@ $\vhops$ such that the next activation of the handler gets the
parameter value $q'$ rather than $q$. parameter value $q'$ rather than $q$.
The CPS translation is updated accordingly to account for the triple The CPS translation is updated accordingly to account for the triple
effect continuation structure. This involves updating all the parts
that previously dynamically decomposed and statically recomposed
effect continuation frames to now include the additional state
parameter. The cases that need to be updated are shown in
effect continuation structure. This involves updating the cases that
scrutinise the effect continuation structure as it now includes the
additional state value. The cases that need to be updated are shown in
Figure~\ref{fig:param-cps}. We write $\xi$ to denote static handler Figure~\ref{fig:param-cps}. We write $\xi$ to denote static handler
parameters. parameters.
% %
The translation of $\Let$ unpacks and repacks the effect continuation
to maintain the continuation length invariant. The translation of
$\Do$ invokes the effect continuation $\reify \svhops$ with a triple
consisting of the value of the handler parameter, the operation, and
the operation payload. The parameter is also pushed onto the reversed
resumption stack. This is necessary to account for the case where the
effect continuation $\reify \svhops$ does not handle operation $\ell$.
% The translation of $\Let$ unpacks and repacks the effect continuation
% to maintain the continuation length invariant.
The translation of $\Do$ invokes the effect continuation
$\reify \svhops$ with a triple consisting of the value of the handler
parameter, the operation, and the operation payload. The parameter is
also pushed onto the reversed resumption stack. This is necessary to
account for the case where the effect continuation $\reify \svhops$
does not handle operation $\ell$.
% An alternative option is to push the parameter back % An alternative option is to push the parameter back
% on the resumption stack during effect forwarding. However that means % on the resumption stack during effect forwarding. However that means
% the resumption stack will be nonuniform as the top element sometimes % the resumption stack will be nonuniform as the top element sometimes
@ -10454,6 +10491,10 @@ by both the pure continuation and effect continuation.% The amended
% CPS translation for parameterised handlers is not a zero cost % CPS translation for parameterised handlers is not a zero cost
% translation for shallow and ordinary deep handlers as they will have % translation for shallow and ordinary deep handlers as they will have
% to thread a ``dummy'' parameter value through. % to thread a ``dummy'' parameter value through.
We can avoid the use of such values entirely if the target language
had proper sums to tag effect continuation frames
accordingly. Obviously, this entails performing a case analysis every
time an effect continuation frame is deconstructed.
\section{Related work} \section{Related work}
\label{sec:cps-related-work} \label{sec:cps-related-work}

Write Preview
Loading…
Cancel
Save