Rewording

macros.tex

@@ -6,6 +6,8 @@
 \newcommand{\BCalc}{\ensuremath{\lambda_{\mathsf{b}}}\xspace}
 \newcommand{\BCalcRec}{\ensuremath{\lambda_{\mathsf{b}+\mathsf{rec}}}\xspace}
 \newcommand{\HCalc}{\ensuremath{\lambda_{\mathsf{h}}}\xspace}
+\newcommand{\SCalc}{\ensuremath{\lambda_{\mathsf{h^\dagger}}}\xspace}
+\newcommand{\HSCalc}{\ensuremath{\lambda_{\mathsf{h^\delta}}}\xspace}
 \newcommand{\EffCalc}{\ensuremath{\lambda_{\mathsf{eff}}}\xspace}
 \newcommand{\UCalc}{\ensuremath{\lambda_{\mathsf{u}}}\xspace}
 
@@ -243,7 +245,7 @@
 \newcommand{\dlf}{f}    % let frames
 \newcommand{\dlk}{s}    % let continuations
 \newcommand{\dhf}{q}    % handler frames
-\newcommand{\dhk}{k}    % handler continuations
+\newcommand{\dhk}{ks}    % handler continuations
 \newcommand{\dhkr}{rk}  % reverse handler continuations
 \newcommand{\dLet}{\dynamic{\Let}}
 \newcommand{\dIn}{\dynamic{\In}}
@@ -274,3 +276,7 @@
 \newcommand{\vhops}{h^{\mathrm{ops}}}
 \newcommand{\svhret}{\chi^{\mathrm{ret}}}
 \newcommand{\svhops}{\chi^{\mathrm{ops}}}
+
+% \newcommand{\dk}{\dRecord{fs,\dRecord{\vhret,\vhops}}}
+\newcommand{\dk}{k}
+

thesis.tex

@@ -2629,14 +2629,14 @@ resumption stack with the current continuation pair.
                     \ea\\
 \cps{\Do\;\ell\;V}
      &\defas& \slam \sk \scons \sh \scons \sks.\reify \sh \dapp \Record{\ell,\Record{\cps{V}, \reify \sh \dcons \reify \sk \dcons \dnil}} \dapp \reify \sks\\
-\cps{\Handle \; M \; \With \; H} &\defas& \slam \sks . \cps{M} \sapp (\cps{\hret} \scons \cps{\hops} \scons \sks)
+\cps{\Handle \; M \; \With \; H} &\defas& \slam \sks . \cps{M} \sapp (\reflect \cps{\hret} \scons \reflect \cps{\hops} \scons \sks)
 %
 \end{equations}
 %
 \textbf{Handler definitions}
 %
 \begin{equations}
-\cps{-} &:& \HandlerCat \to \UCompCat\\
+\cps{-} &:& \HandlerCat \to \UValCat\\
 \cps{\{\Return \; x \mapsto N\}} &\defas& \dlam x\, ks.
    \ba[t]{@{~}l}
       \Let\; (h \dcons k \dcons h' \dcons ks') = ks \;\In\\
@@ -3195,12 +3195,100 @@ If $M \reducesto N$ then $\pcps{M} \reducesto^+ \areducesto^* \pcps{N}$.
 % \end{proof}
 %
 
+\section{A simultaneous CPS transform for deep and shallow handlers}
+\label{sec:cps-deep-shallow}
+
+\begin{figure}
+%
+\textbf{Values}
+%
+\begin{equations}
+  \cps{-}                    &:& \ValCat \to \UValCat\\
+  % \cps{x}                    &\defas& x\\
+  \cps{\lambda x.M}          &\defas& \dlam x\,\dhk.\Let\;(\dk \dcons \dhk') = \dhk\;\In\;\cps{M} \sapp (\reflect\dk \scons \reflect \dhk') \\
+  \cps{\Lambda \alpha.M}     &\defas& \dlam \Unit\,\dhk.\Let\;(\dk \dcons \dhk') = \dhk\;\In\;\cps{M} \sapp (\reflect\dk \scons \reflect \dhk') \\
+  \cps{\Rec\,g\,x.M} &\defas& \Rec\,g\,x\,\dhk.\Let\;(\dk \dcons \dhk') = \dhk\;\In\;\cps{M} \sapp (\reflect\dk \scons \reflect \dhk') \\
+  % \multicolumn{3}{c}{
+  % \cps{\Record{}} \defas \Record{}
+  % \qquad
+  % \cps{\Record{\ell = \!\!V; W}} \defas \Record{\ell = \!\cps{V}; \cps{W}}
+  % \qquad
+  % \cps{\ell\,V} \defas \ell\,\cps{V}
+  % }
+\end{equations}
+%
+\textbf{Computations}
+%
+\begin{equations}
+\cps{-}                                          &:& \CompCat \to \SValCat^\ast \to \UCompCat\\
+% \cps{V\,W}                                       &\defas& \slam \shk.\cps{V} \dapp \cps{W} \dapp \reify \shk \\
+% \cps{V\,T}                                       &\defas& \slam \shk.\cps{V} \dapp \Record{} \dapp \reify \shk \\
+% \cps{\Let\; \Record{\ell=x;y} = V \; \In \; N}   &\defas& \slam \shk.\Let\; \Record{\ell=x;y} = \cps{V} \; \In \; \cps{N} \sapp \shk \\
+% \cps{\Case~V~\{\ell~x \mapsto M; y \mapsto N\}}  &\defas&
+%   \slam \shk.\Case~\cps{V}~\{\ell~x \mapsto \cps{M} \sapp \shk; y \mapsto \cps{N} \sapp \shk\} \\
+% \cps{\Absurd~V}                                  &\defas& \slam \shk.\Absurd~\cps{V} \\
+% \end{equations}
+% \begin{equations}
+\cps{\Return\,V} &\defas& \slam \shk.\kapp\;(\reify \shk)\;\cps{V} \\
+\cps{\Let~x \revto M~\In~N} &\defas&
+   \bl\slam \sRecord{\shf,  \sRecord{\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{\svhret, \svhops}} \scons \shk)\el
+      \ea
+  \el\\
+\cps{\Do\;\ell\;V} &\defas&
+  \slam \sRecord{\shf, \sRecord{\svhret, \svhops}} \scons \shk.\,
+        \reify\svhops \bl\dapp \dRecord{\ell,\dRecord{\cps{V}, \dRecord{\reify \shf, \dRecord{\reify\svhret, \reify\svhops}} \dcons \dnil}}\\
+                         \dapp \reify \shk\el \\
+\cps{\Handle^\depth \, M \; \With \; H} &\defas&
+\slam \shk . \cps{M} \sapp (\sRecord{\snil, \sRecord{\reflect \cps{\hret}, \reflect \cps{\hops}^\depth}} \scons \shk) \\
+\end{equations}
+%
+\textbf{Handler definitions}
+%
+\begin{equations}
+\cps{-}                    &:& \HandlerCat \to \UValCat\\
+% \cps{H}^\depth &=& \sRecord{\reflect \cps{\hret}, \reflect \cps{\hops}^\depth}\\
+\cps{\{\Return \; x \mapsto N\}} &\defas& \dlam x\,\dhk.\Let\;(\dk \dcons \dhk') = \dhk\;\In\;\cps{N} \sapp (\reflect\dk \scons \reflect \dhk') \\
+\cps{\{(\ell \; p \; r \mapsto N_\ell)_{\ell \in \mathcal{L}}\}}^\depth
+&\defas&
+\dlam \dRecord{z,\dRecord{p,\dhkr}}\,\dhk.
+              \Case \;z\; \{
+               \ba[t]{@{}l@{}c@{~}l}
+                (&\ell &\mapsto
+                   \ba[t]{@{}l}
+                      \Let\;r=\Res^\depth\,\dhkr\;\In\;  \\
+                      \Let\;(\dk \dcons \dhk') = \dhk\;\In\\
+                      \cps{N_{\ell}} \sapp (\reflect\dk \scons \reflect \dhk'))_{\ell \in \mathcal{L}}
+                    \ea\\
+                  &y     &\mapsto \hforward((y, p, \dhkr), \dhk) \} \\
+                \ea \\
+\hforward((y, p, \dhkr), \dhk) &\defas& \bl
+              \Let\; \dRecord{fs, \dRecord{\vhret, \vhops}} \dcons \dhk' = \dhk \;\In \\
+              % \Let\; rk' = \dRecord{fs, \dRecord{\vhret, \vhops}} \dcons \dhkr\;\In\\
+              \vhops \dapp \dRecord{y,\dRecord{p, \dRecord{fs, \dRecord{\vhret, \vhops}} \dcons \dhkr}} \dapp \dhk' \\
+              \el
+\end{equations}
+
+\textbf{Top-level program}
+%
+\begin{equations}
+\pcps{-}                    &:& \CompCat \to \UCompCat\\
+\pcps{M} &\defas& \cps{M} \sapp (\sRecord{\snil, \sRecord{\reflect \dlam x\,\dhk. x, \reflect \dlam \dRecord{z,\dRecord{p,rk}}\,\dhk.\Absurd~z}} \scons \snil) \\
+\end{equations}
+%
+\caption{Adjustments to the higher-order uncurried CPS translation.}
+\label{fig:cps-higher-order-uncurried}
+\end{figure}
+
 \section{Related work}
 \label{sec:cps-related-work}
 
 \paragraph{Plotkin's colon translation}
 
-The defacto standard method for proving the correctness of a CPS
+The traditional method for proving the correctness of a CPS
 translation is by way of a simulation result. Simulation states that
 every reduction sequence in a given source program is mimicked by its
 CPS transformation.
@@ -3212,10 +3300,10 @@ arise in the source program.
 \citet{Plotkin75} uses the so-called \emph{colon translation} to
 overcome static administrative reductions.
 %
-Informally, it is defined such that given a source term $M$ and a
+Informally, it is defined such that given some source term $M$ and
-continuation $k$, the term $M : k$ is the result of performing all
+some continuation $k$, then the term $M : k$ is the result of
-static administrative reductions on $\cps{M}\,k$, that is
+performing all static administrative reductions on $\cps{M}\,k$, that
-$\cps{M}\,k \reducesto^\ast M : k$.
+is to say $\cps{M}\,k \areducesto^* M : k$.
 %
 Thus this translation makes it possible to bypass administrative
 reductions and instead focus on the reductions inherited from the