Resumptions as explicit reversed stacks.

macros.tex

@@ -87,6 +87,8 @@
 
 \newcommand{\dom}{\ensuremath{\mathsf{dom}}}
 
+\newcommand{\Res}{\keyw{res}}
+
 %% Handler projections.
 \newcommand{\hret}{H^{\mathrm{ret}}}
 \newcommand{\hval}{\hret}

thesis.tex

@@ -55,6 +55,28 @@
 \hfsetfillcolor{gray!40}
 \hfsetbordercolor{gray!40}
 
+% Cancelling
+\newif\ifCancelX
+\tikzset{X/.code={\CancelXtrue}}
+\newcommand{\Cancel}[2][]{\relax
+\ifmmode%
+  \tikz[baseline=(X.base),inner sep=0pt] {\node (X) {$#2$};
+  \tikzset{#1}
+  \draw[#1,overlay,shorten >=-2pt,shorten <=-2pt] (X.south west) -- (X.north east);
+  \ifCancelX
+    \draw[#1,overlay,shorten >=-2pt,shorten <=-2pt] (X.north west) -- (X.south east);
+  \fi}
+\else
+  \tikz[baseline=(X.base),inner sep=0pt] {\node (X) {#2};
+  \tikzset{#1}
+  \draw[#1,overlay,shorten >=-2pt,shorten <=-2pt] (X.south west) -- (X.north east);
+  \ifCancelX
+    \draw[#1,overlay,shorten >=-2pt,shorten <=-2pt] (X.north west) -- (X.south east);
+  \fi}%
+\fi}
+
+\newcommand{\XCancel}[1]{\Cancel[red,X,line width=1pt]{#1}}
+
 %%
 %% Theorem environments
 %%
@@ -1890,7 +1912,7 @@ getting stuck on an unhandled operation.
 
 \part{Implementation}
 
-\chapter{Continuation-passing styles}
+\chapter{Continuation-passing style}
 \label{ch:cps}
 
 Continuation-passing style (CPS) is a \emph{canonical} program
@@ -1977,9 +1999,9 @@ consume stack space.
 \dhil{The focus of the introduction should arguably not be to explain CPS.}
 \dhil{Justify CPS as an implementation technique}
 \dhil{Give a side-by-side reduction example of $\dec{fac}$ and $\dec{fac}_{\dec{cps}}$.}
+\dhil{Define desirable properties of a CPS translation: properly tail-recursive, no static administrative redexes}
 
-
+\section{Initial target calculus}
-\section{Target calculus}
 \label{sec:target-cps}
 
 The syntax, semantics, and syntactic sugar for the target calculus
@@ -2016,13 +2038,12 @@ term) to cope with the case of pattern matching failure.
   \flushleft
   \textbf{Syntax}
   \begin{syntax}
-    \slab{Values}  &V, W \in \UValCat &::= &  x \mid \lambda x.M \mid \Rec\,g\,x.M \mid \Record{} \mid \Record{V, W} \mid \ell
+    \slab{Values}  &U, V, W \in \UValCat &::= &  x \mid \lambda x.M \mid \Rec\,g\,x.M \mid \Record{} \mid \Record{V, W} \mid \ell
     \smallskip \\
     \slab{Computations}  &M,N \in \UCompCat  &::= & V \mid M\,W \mid \Let\; \Record{x,y} = V \; \In \; N\\
                          &     &\mid& \Case\; V\, \{\ell \mapsto M; y \mapsto N\} \mid \Absurd\,V
-    % &    &\mid& \Vmap\;(x.M)\;V \\
     \smallskip \\
-    \slab{Evaluation contexts} &\EC \in \UEvalCat &::= & [~] \mid \EC\;W \\ %\mid \Let\; x \revto \EC \;\In\; N \\
+    \slab{Evaluation contexts} &\EC \in \UEvalCat &::= & [~] \mid \EC\;W \\
   \end{syntax}
 
   \textbf{Reductions}
@@ -2034,7 +2055,6 @@ term) to cope with the case of pattern matching failure.
     \Case \; \ell \; \{ \ell \mapsto M; y \mapsto N\} &\reducesto& M \\
     \usemlab{Case_2} &
     \Case \; \ell \; \{ \ell' \mapsto M; y \mapsto N\} &\reducesto& N[\ell/y], \hfill\quad \text{if } \ell \neq \ell' \\
-    % \usemlab{VMap}      & \Vmap\, (x.M) \,(\ell\, V) &\reducesto& \ell\, M[V/x] \\
     \usemlab{Lift} &
     \EC[M] &\reducesto& \EC[N], \hfill \text{if } M \reducesto N \\
   \end{reductions}
@@ -2112,8 +2132,8 @@ translate to value terms in the target.
 \cps{\Case~V~\{\ell~x \mapsto M; y \mapsto N\}} &=&
   \Case~\cps{V}~\{\ell~x \mapsto \cps{M}; y \mapsto \cps{N}\} \\
 \cps{\Absurd~V}                                 &=& \Absurd~\cps{V} \\
-\cps{\Return~V}                                 &=& \lambda k.k~\cps{V} \\
+\cps{\Return~V}                                 &=& \lambda k.k\,\cps{V} \\
-\cps{\Let~x \revto M~\In~N}                     &=& \lambda k.\cps{M}(\lambda x.\cps{N}k) \\
+\cps{\Let~x \revto M~\In~N}                     &=& \lambda k.\cps{M}(\lambda x.\cps{N}\,k) \\
 \end{eqs}
 \el
 \]
@@ -2121,7 +2141,7 @@ translate to value terms in the target.
 \label{fig:cps-cbv}
 \end{figure}
 
-\section{First-order CPS translations of effect handlers}
+\section{CPS transforming deep effect handlers}
 \label{sec:fo-cps}
 
 The translation of a computation term by the basic CPS translation in
@@ -2160,7 +2180,7 @@ operation invocation can be reinstated when the resumption is invoked.
 \subsection{Curried translation}
 \label{sec:first-order-curried-cps}
 
-We first consider a curried CPS translation that builds the
+We first consider a curried CPS translation that extends the
 translation of Figure~\ref{fig:cps-cbv}. The extension to operations
 and handlers is localised to the additional features because currying
 conveniently lets us get away with a shift in interpretation: rather
@@ -2174,7 +2194,7 @@ is as follows.
 %
 \begin{equations}
 \cps{\Do\;\ell\;V} &\defas& \lambda k.\lambda h.h~\Record{\ell,\Record{\cps{V}, \lambda x.k~x~h}} \\
-\cps{\Handle \; M \; \With \; H} &\defas& \cps{M}~\cps{\hret}~\cps{\hops}, ~\text{where} \smallskip\\
+\cps{\Handle \; M \; \With \; H} &\defas& \cps{M}~\cps{\hret}~\cps{\hops} \smallskip\\
 \cps{\{ \Return \; x \mapsto N \}} &\defas& \lambda x . \lambda h . \cps{N} \\
 \cps{\{ \ell~p~r \mapsto N_\ell \}_{\ell \in \mathcal{L}}}
 &\defas&
@@ -2229,11 +2249,11 @@ which makes it unviable in practice.
     basis for an implementation. This deficiency is essentially due to
     the curried representation of the continuation stack.
 
-  \item The image of the translation yields context independent
+  \item The image of the translation yields static administrative
-    administrative redexes, i.e. redexes that could be reduced
+    redexes, i.e. redexes that could be reduced statically. This is a
-    statically. This is a classic problem with CPS translation, which
+    classic problem with CPS translation, which is typically dealt
-    is typically dealt with by introducing a second pass to clean up
+    with by introducing a second pass to clean up the
-    the image~\cite{DanvyF92}.
+    image~\cite{DanvyF92}.
 \end{enumerate}
 
 The following minimal example readily illustrates both issues.
@@ -2297,11 +2317,68 @@ continuations~\citeyearpar{MaterzokB12}.
 
 \subsection{Uncurried translation}
 \label{sec:first-order-uncurried-cps}
+%
+%
+\begin{figure}
+  \flushleft
+  \textbf{Syntax}
+  \begin{syntax}
+    \slab{Computations}  &M,N \in \UCompCat  &::= & \cdots \mid \XCancel{M\,W} \mid V\,W \mid U\,V\,W \smallskip \\
+    \XCancel{\slab{Evaluation contexts}} &\XCancel{\EC \in \UEvalCat} &::= & \XCancel{[~] \mid \EC\;W} \\
+  \end{syntax}
 
-In this section we seek to refine the CPS translation for deep
+  \textbf{Reductions}
-handlers to be properly tail-recursive. As remarked in the previous
+  \begin{reductions}
-section, the crux of the problem is the curried representation of the
+    \usemlab{App_1}   & (\lambda x . M) V &\reducesto& M[V/x] \\
-continuation pair. To rectify this problem we can adapt the standard
+    \usemlab{App_2}   & (\lambda x . \lambda y. \, M) V\, W &\reducesto& M[V/x,W/y] \\
+    \XCancel{\usemlab{Lift}} & \XCancel{\EC[M]} &\reducesto& \XCancel{\EC[N], \hfill \text{if } M \reducesto N}
+  \end{reductions}
+  \caption{Adjustments to the syntax and semantics of $\UCalc$.}
+  \label{fig:refined-cps-cbv-target}
+\end{figure}
+%
+In this section we will refine the CPS translation for deep handlers
+to make it properly tail-recursive. As remarked in the previous
+section, the lack of tail-recursion is apparent in the syntax of the
+target calculus $\UCalc$ as it permits an arbitrary computation term
+in the function position of an application term.
+%
+
+As a first step we may impose a syntax restriction in target calculus
+such that the term in function position must be a value. With this
+restriction the syntax of $\UCalc$ implements the property that any
+term constructor features at most one computation term, and this
+computation term always appears in tail position. Thus this
+restriction suffices to ensure that every function application will be
+in tail-position.
+%
+Figure~\ref{fig:refined-cps-cbv-target} contains the adjustments to
+syntax and semantics of $\UCalc$. The target calculus now supports
+both unary and binary application forms. As we shall see shortly,
+binary application turns out be convenient when we enrich the notion
+of continuation. Both application forms are comprised only of value
+terms. As a result the dynamic semantics of $\UCalc$ no longer makes
+use of evaluation contexts, hence we remove them altogether. The
+reduction rule $\usemlab{App_1}$ applies to unary application and it
+is the same as the $\usemlab{App}$-rule in
+Figure~\ref{fig:cps-cbv-target}. The new $\usemlab{App_2}$-rule
+applies to binary application: it performs a simultaneous substitution
+of the arguments $V$ and $W$ for the parameters $x$ and $y$,
+respectively, in the function body $M$.
+%
+
+These changes to $\UCalc$ immediately invalidates the curried
+translation from the previous section as the image of the translation
+is no longer well-formed.
+%
+% The crux of the problem is the curried representation of the
+% continuation pair.
+The crux of the problem is that the curried interpretation of
+continuations causes the CPS translation to produce `large'
+application terms, e.g. the translation rule for effect forwarding
+produces three-argument application term.
+%
+To rectify this problem we can adapt the standard
 technique of \citet{MaterzokB12} to uncurry our CPS
 translation. Uncurrying necessitates a change of representation for
 continuations: a continuation is now an alternating list of pure
@@ -2314,13 +2391,12 @@ translation is adjusted as follows to account for the new
 representation of continuations.
 %
 \begin{equations}
-\cps{\Return~V}             &\defas& \lambda (k \cons ks).k~\cps{V}~ks \\
+\cps{\Return~V}             &\defas& \lambda (k \cons ks).k\,\cps{V}\,ks \\
-\cps{\Let~x \revto M~\In~N} &\defas& \lambda (k \cons ks).\cps{M}((\lambda x.\lambda ks.\cps{N}(k \cons ks)) \cons ks)
+\cps{\Let~x \revto M~\In~N} &\defas& \lambda (k \cons ks).\cps{M}((\lambda x.\lambda ks'.\cps{N}(k \cons ks')) \cons ks)
 \smallskip \\
-\cps{\Do\;\ell\;V} &\defas& \lambda (k \cons h \cons ks).h~\Record{\ell,\Record{\cps{V}, \lambda x.\lambda ks.k~x~(h \cons ks)}}~ks
+\cps{\Do\;\ell\;V} &\defas& \lambda (k \cons h \cons ks).h\,\Record{\ell,\Record{\cps{V}, \lambda x.\lambda ks'.k\,x\,(h \cons ks')}}\,ks
 \smallskip \\
-\cps{\Handle \; M \; \With \; H} &\defas& \lambda ks . \cps{M} (\cps{\hret} \cons \cps{\hops} \cons ks)
+\cps{\Handle \; M \; \With \; H} &\defas& \lambda ks . \cps{M} (\cps{\hret} \cons \cps{\hops} \cons ks) \smallskip\\
- , ~\text{where} \smallskip\\
 \cps{\{\Return \; x \mapsto N\}} &\defas& \lambda x.\lambda ks.\Let\; (h \cons ks') = ks \;\In\; \cps{N}\,ks'
 \\
 \cps{\{\ell \; p \; r \mapsto N_\ell\}_{\ell \in \mathcal{L}}}
@@ -2334,14 +2410,12 @@ representation of continuations.
               \Let\; (k' \cons h' \cons ks') = ks \;\In\; \\
               h'\,\Record{y, \Record{p, \lambda x.\lambda ks''.\,r\,x\,(k' \cons h' \cons ks'')}}\,ks'\\
               \el \smallskip\\
-\pcps{M} &\defas& \cps{M}~((\lambda x\,ks.x) \cons (\lambda \Record{z,\Record{p,r}}. \lambda ks.\,\Absurd~z) \cons \nil)
+\pcps{M} &\defas& \cps{M}~((\lambda x.\lambda ks.x) \cons (\lambda \Record{z,\Record{p,r}}. \lambda ks.\,\Absurd~z) \cons \nil)
 \end{equations}
 %
 The other cases are as in the original CPS translation in
-Figure~\ref{fig:cps-cbv}.  The stacks of continuations are now lists,
+Figure~\ref{fig:cps-cbv}.
-where pure continuations and effect continuations occupy alternating
+%
-positions.
-
 Since we now use a list representation for the stacks of
 continuations, we have had to modify the translations of all the
 constructs that manipulate continuations. For $\Return$ and $\Let$, we
@@ -2356,12 +2430,100 @@ is the same as before, except for explicit passing of the
 $ks$. Forwarding now pattern matches on the stack to extract the next
 continuation pair, rather than accepting them as arguments.
 %
-Proper tail recursion coincides with a refinement of the target
+% Proper tail recursion coincides with a refinement of the target
-syntax. Now applications are either of the form $V\,W$ or of the form
+% syntax. Now applications are either of the form $V\,W$ or of the form
-$U\,V\,W$. We could also add a rule for applying a two argument lambda
+% $U\,V\,W$. We could also add a rule for applying a two argument lambda
-abstraction to two arguments at once and eliminate the
+% abstraction to two arguments at once and eliminate the
-$\usemlab{Lift}$ rule, but we defer this until our higher order
+% $\usemlab{Lift}$ rule, but we defer this until our higher order
-translation in Section~\ref{sec:higher-order-uncurried-cps}.
+% translation in Section~\ref{sec:higher-order-uncurried-cps}.
+
+Let us revisit the example from
+Section~\ref{sec:first-order-curried-cps} to see first hand that our
+refined translation makes the example properly tail-recursive.
+%
+\begin{equations}
+\pcps{\Return\;\Record{}}
+     &=         & (\lambda (k \cons ks).k\,\Record{}\,ks)\,((\lambda x.\lambda ks.x) \cons (\lambda \Record{z, \_}.\lambda ks.\Absurd\,z) \cons \nil)  \\
+     &\reducesto& (\lambda x.\lambda ks.x)\,\Record{}\,((\lambda \Record{z,\_}.\lambda ks.\Absurd\,z) \cons \nil)\\
+     &\reducesto& \Record{}
+\end{equations}
+%
+The image of this uncurried translation admits three
+$\reducesto$-reduction steps (disregarding the administrative steps
+induced by pattern matching), which is one less step than admitted by
+the image of the curried translation. The `missing' step is precisely
+the partial application of the initial pure continuation function,
+which was not in tail position. Note, however, that the first
+reduction is still administrative. The involved redex is still static,
+meaning that it could be eliminated at translation time.
+%
+\dhil{Discuss dynamic and static administrative redex.}
+
+\subsection{Resumptions as explicit reversed stacks}
+\label{sec:first-order-explicit-resump}
+%
+\dhil{Show an example involving administrative redexes produced by resumptions}
+%
+Thus far resumptions have been represented as functions, and
+forwarding has been implemented using function composition. The
+composition of resumption gives rise to unnecessary dynamic
+administrative redexes as function composition necessitates the
+introduction of an additional lambda abstraction.
+%
+
+We can avert generating these administrative redexes by applying a
+variation of the technique that we used in the previous section to
+uncurry the curried CPS translation.
+%
+Rather than representing resumptions as functions, we move to an
+explicit representation of resumptions as \emph{reversed} stacks of
+pure and effect continuations. By choosing to reverse the order of
+pure and effect continuations, we can construct resumptions
+efficiently using regular cons-lists. We convert these reversed stacks
+to actual functions on demand using a special
+$\Let\;r=\Res\,V\;\In\;N$ computation term that reduces as follows.
+%
+\begin{reductions}
+  \usemlab{Res}
+  & \Let\;r=\Res\,(V_n \cons \dots \cons V_1 \cons \nil)\;\In\;N
+  & \reducesto
+  & N[\lambda x\,k.V_1\,x\,(V_2 \cons \dots \cons V_n \cons k)/r]
+\end{reductions}
+%
+This reduction rule reverses the stack, extracts the top continuation
+$V_1$, and prepends the remainder onto the current stack $W$. The
+stack representing a resumption and the remaining stack $W$ are
+reminiscent of the zipper data structure for representing cursors in
+lists~\cite{Huet97}. Thus we may think of resumptions as representing
+pointers into the stack of handlers.
+%
+The translations of $\Do$, handling, and forwarding need to be
+modified to account for the change in representation of
+resumptions.
+%
+\begin{equations}
+  \cps{\Do\;\ell\;V}
+     &\defas& \lambda k \cons h \cons ks.\,h\, \Record{\ell,\Record{\cps{V}, h \cons k \cons \nil}}\, ks
+  \\
+  \cps{\{(\ell \; p \; r \mapsto N_\ell)_{\ell \in \mathcal{L}}\}}
+     &\defas& \bl
+                \lambda \Record{z,\Record{p,rs}}.\lambda ks.\Case \;z\; \{
+                  \bl
+                   (\ell \mapsto \Let\;r=\Res\;rs \;\In\; \cps{N_{\ell}}\, ks)_{\ell \in \mathcal{L}};\,\\
+                   y \mapsto \hforward((y,p,rs),ks) \} \\
+                  \el \\
+             \el \\
+  \hforward((y,p,r),ks)
+    &\defas&\Let\; (k' \cons h' \cons ks') = ks \;\In\; h'\,\Record{y,\Record{p,h'::k'::r}} \,ks'
+\end{equations}
+%
+The translation of $\Do$ constructs an initial resumption stack,
+operation clauses extract and convert the current resumption stack
+into a function using the $\Res$, and $\hforward$ augments the current
+resumption stack with the current continuation pair.
+%
+% Since we have only changed the representation of resumptions, the
+% translation of top-level programs remains the same.
 
 \chapter{Abstract machine semantics}