Tidy up HO translation.

thesis.tex

@@ -860,8 +860,9 @@ given term.
 The function computes the set of free variables bottom-up. Most cases
 are homomorphic on the syntax constructors. The interesting cases are
 those constructs which feature term binders: lambda abstraction, let
-bindings, pair destructing, and case splitting. In each of those cases
-we subtract the relevant binder(s) from the set of free variables.
+bindings, pair deconstructing, and case splitting. In each of those
+cases we subtract the relevant binder(s) from the set of free
+variables.
 
 \subsection{Typing rules}
 \label{sec:base-language-type-rules}
@@ -1007,7 +1008,7 @@ application $V\,A$ is well-typed whenever the abstractor term $V$ has
 the polymorphic type $\forall \alpha^K.C$ and the type $A$ has kind
 $K$. This rule makes use of type substitution.
 %
-The \tylab{Split} rule handles typing of record destructing. When
+The \tylab{Split} rule handles typing of record deconstructing. When
 splitting a record term $V$ on some label $\ell$ binding it to $x$ and
 the remainder to $y$. The label we wish to split on must be present
 with some type $A$, hence we require that
@@ -1566,9 +1567,9 @@ effect handlers which are an alternative to deep effect handlers.
 %
 Programming with effect handlers is a dichotomy of \emph{performing}
 and \emph{handling} of effectful operations -- or alternatively a
-dichotomy of \emph{constructing} and \emph{destructing}. An operation
+dichotomy of \emph{constructing} and \emph{deconstructing}. An operation
 is a constructor of an effect without a predefined semantics. A
-handler destructs effects by pattern-matching on their operations. By
+handler deconstructs effects by pattern-matching on their operations. By
 matching on a particular operation, a handler instantiates the said
 operation with a particular semantics of its own choosing. The key
 ingredient to make this work in practice is \emph{delimited
@@ -2534,28 +2535,12 @@ 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.
 
 \subsection{Higher-order translation for deep effect handlers}
 \label{sec:higher-order-uncurried-deep-handlers-cps}
 %
 \begin{figure}
 %
-% \textbf{Static patterns and static lists}
-% %
-% \begin{syntax}
-% \slab{Static patterns} &\sP& ::= & \sk \scons \sP \mid \sks \\
-% \slab{Static lists} &\VS& ::= & V \scons \VS \mid \reflect V \\
-% \end{syntax}
-% %
-% \textbf{Reification}
-% %
-% \begin{equations}
-% \reify (V \scons \VS) &\defas& V \dcons \reify \VS \\
-% \reify \reflect V     &\defas& V \\
-% \end{equations}
-%
 \textbf{Values}
 %
 \begin{displaymath}
@@ -2594,19 +2579,6 @@ resumption stack with the current continuation pair.
 \cps{-} &:& \HandlerCat \to \UCompCat\\
 \cps{\{\Return \; x \mapsto N\}} &\defas& \dlam x\, ks.\Let\; (h \dcons ks') = ks \;\In\; \cps{N} \sapp \reflect ks'
 \\
-% \cps{\{(\ell \; p \; r \mapsto N_\ell)_{\ell \in \mathcal{L}}\}}
-% &\defas&
-% \bl
-% \dlam z \, ks.\Case \;z\; \{
-%       \bl
-%       (\ell~\Record{p, s} \mapsto \dLet\;r=\Fun\,s \;\dIn\; \cps{N_{\ell}} \sapp \reflect ks)_{\ell \in \mathcal{L}};\,
-%       y \mapsto \hforward \} \\
-%       \el \\
-% \el \\
-% \hforward &\defas& \bl
-%               \dLet\; (k' \dcons h' \dcons ks') = ks \;\dIn\; \\
-%               \Vmap\,(\dlam\Record{p, s}\,(k \dcons ks).k\,\Record{p, h' \dcons k' \dcons s}\,ks)\,y\,(h' \dcons ks') \\
-%               \el\\
 \cps{\{(\ell \; p \; r \mapsto N_\ell)_{\ell \in \mathcal{L}}\}}
      &\defas& \bl
                 \dlam \Record{z,\Record{p,rs}}\,ks.\Case \;z\; \{
@@ -2666,15 +2638,6 @@ alternating lists of pure continuation functions and effect
 continuation functions. To ease notation we are going make use of
 pattern matching notation. The static meta language is generated by
 the following productions.
-% Static constructs are marked in
-% {\color{blue}$\overline{\text{static blue}}$}, and their redexes are
-% reduced as part of the translation (at compile time).  We make use of
-% static lambda abstractions, pairs, and lists. Reflection of dynamic
-% language values into the static language is written as $\reflect V$.
-% %
-% We use $\shk$ for variables representing statically known
-% continuations (frame stacks), $\shf$ for variables representing pure
-% frame stacks, and $\chi$ for variables representing handlers.
 %
 \begin{syntax}
   \slab{Static patterns} &\sP \in \SPatCat &::=& \sks \mid \sk \scons \sP\\
@@ -2682,8 +2645,8 @@ the following productions.
   \slab{Static computations} & \sM \in \SCompCat &::=& \sV \sapp \sW \mid \sV \dapp V \dapp W
 \end{syntax}
 %
-The patterns comprise only static list destructing. We let $\sP$ range
-over static patterns.
+The patterns comprise only static list deconstructing. We let $\sP$
+range over static patterns.
 %
 The static values comprise dynamic values, reflected dynamic values,
 static lists, and static lambda abstractions. We let $\sV, \sW$ range
@@ -2706,8 +2669,8 @@ Static computations are subject to the following equational axioms.
 The first equation is static $\beta$-equivalence, it states that
 applying a static lambda abstraction with binder $\sks$ and body $\sM$
 to a static value $\sV$ is equal to substituting $\sV$ for $\sks$ in
-$\sM$. The second equation allows us to apply a static list
-component-wise.
+$\sM$. The second equation provides a means for applying a static
+lambda abstraction to a static list component-wise.
 %
 \dhil{What about $\eta$-equivalence?}
 
@@ -2720,32 +2683,38 @@ $\reify \sV$ by induction on their structure.
     &\reify (\sV \scons \sW) \defas \reify \sV \dcons \reify \sW
   \ea
 \]
-
-
+%
+\dhil{Need to spell out that static pattern matching may induce dynamic (administrative) reductions}
+%
 \paragraph{Higher-order translation}
-The CPS translation is given in
-Figure~\ref{fig:cps-higher-order-uncurried}. In essence, it is the
-same as the CPS translation for deep and shallow handlers we described
-in Section~\ref{sec:pure-as-stack}, albeit separated into static and
-dynamic parts. A major difference that has a large cosmetic effect on
-the presentation of the translation is that we maintain the invariant
-that the statically known stack ($\sk$) always contains at least one
-frame, consisting of a triple
-$\sRecord{\reflect V_{fs}, \sRecord{\reflect V_{ret}, \reflect
-    V_{ops}}}$ of reflected dynamic pure frame stacks, return
-handlers, and operation handlers. Maintaining this invariant ensures
-that all translations are uniform in whether they appear statically
-within the scope of a handler or not, and this simplifies our
-correctness proof.  To maintain the invariant, any place where a
-dynamically known stack is passed in (as a continuation parameter
-$k$), it is immediately decomposed using a dynamic language $\Let$ and
-repackaged as a static value with reflected variable
-names. Unfortunately, this does add some clutter to the translation
-definition, as compared to the translations above. However, there is a
-payoff in the removal of administrative reductions at run time.
-%
-\dhil{Rewrite the above.}
 %
+The complete CPS translation is given in
+Figure~\ref{fig:cps-higher-order-uncurried}. In essence, it is the
+same as the refined first-order uncurried CPS translation, although
+the notation is slightly more involved due to the separation of static
+and dynamic parts.
+%
+The translation on values is mostly homomorphic on the syntax
+constructors, except for $\lambda$- and $\Lambda$-abstractions which
+are translated in the exact same way, because the target calculus has
+no notion of types. As per usual continuation passing style practice,
+the translation of a lambda abstraction yields a dynamic binary lambda
+abstraction, where the second parameter is intended to be the
+continuation parameter. However, the translation slightly diverge from
+the usual practice in the translation of the body as the result of
+$\cps{M}$ is applied statically, rather than dynamically, to the
+(reflected) continuation parameter.
+%
+The reason is that the translation on computations is staged: for any
+given computation term the translation yields a static function, which
+can be applied to a static continuation to ultimately produce a
+$\UCalc$-computation term. This staging is key to eliminating static
+administrative redexes as any static function may perform static
+computation by manipulating its provided static continuation, as is
+for instance done in the translation of $\Let$.
+%
+\dhil{Spell out why this translation qualifies as `higher-order'.}
+
 Let us again revisit the example from
 Section~\ref{sec:first-order-curried-cps} to see that the higher-order
 translation eliminates the static redex at translation time.
@@ -2758,15 +2727,19 @@ translation eliminates the static redex at translation time.
 \end{equations}
 %
 In contrast with the previous translations, the image of this
-translation admits only a single dynamic reduction.
+translation admits only a single dynamic reduction (disregarding the
+dynamic administrative reductions arising from continuation
+construction and deconstruction).
 
 \subsubsection{Correctness}
 \label{sec:higher-order-cps-deep-handlers-correctness}
 
-In order to prove the correctness of the higher-order uncurried CPS
-translation (Theorem~\ref{thm:ho-simulation}), we first state several
-auxiliary lemmas describing how translated terms behave. First, the
-higher-order CPS translation commutes with substitution.
+We establish the correctness of the higher-order uncurried CPS
+translation via a simulation result in style of
+Plotkin~\cite{Plotkin75} (Theorem~\ref{thm:ho-simulation}). However,
+before we can state and prove this result, we first several auxiliary
+lemmas describing how translated terms behave. First, the higher-order
+CPS translation commutes with substitution.
 %
 \begin{lemma}[Substitution]\label{lem:ho-cps-subst}
   %
@@ -2811,8 +2784,8 @@ It follows as a corollary that top-level substitution is well-behaved.
   Lemma~\ref{lem:ho-cps-subst}.
 \end{proof}
 %
-In order to reason about the behaviour of the \semlab{Op} rule,
-which is defined in terms of an evaluation context, we extend the CPS
+In order to reason about the behaviour \semlab{Op} rule, which is
+defined in terms of an evaluation context, we need to extend the CPS
 translation to evaluation contexts.
 %
 \begin{equations}
@@ -2825,8 +2798,9 @@ translation to evaluation contexts.
 The following lemma is the characteristic property of the CPS
 translation on evaluation contexts.
 %
-This allows us to focus on the computation contained within
-an evaluation context.
+It provides a means for decomposing an evaluation context, such that
+we can focus on the computation contained within the evaluation
+context.
 %
 \begin{lemma}[Decomposition]
 \label{lem:decomposition}
@@ -2841,26 +2815,27 @@ an evaluation context.
   Proof by structural induction on the evaluation context $\EC$.
 \end{proof}
 %
-Though we have eliminated the static administrative redexes, we are
-still left with one form of administrative redex that cannot be
-eliminated statically because it only appears at run-time. These arise
-from pattern matching against a reified stack of continuations and are
-given by the $\usemlab{SplitList}$ rule.
+Even though we have eliminated the static administrative redexes, we
+still need to account for the dynamic administrative redexes that
+arise from pattern matching against a reified continuation. To
+properly account for these administrative redexes it is convenient to
+treat list pattern matching as a primitive in $\UCalc$, therefore we
+introduce a new reduction rule $\usemlab{SplitList}$ in $\UCalc$.
 %
 \begin{reductions}
 \usemlab{SplitList} & \Let\; (k \dcons ks) = V \dcons W \;\In\; M &\reducesto& M[V/k, W/ks] \\
 \end{reductions}
 %
-This is isomorphic to the \usemlab{Split} rule, but we now treat lists
-and \usemlab{SplitList} as distinct from pairs, unit, and
-\usemlab{Split} in the higher-order translation so that we can
-properly account for administrative reduction.
+Note this rule is isomorphic to the \usemlab{Split} rule with lists
+encoded as right nested pairs using unit to denote nil.
 %
 We write $\areducesto$ for the compatible closure of
 \usemlab{SplitList}.
 
-By definition, $\reify \reflect V = V$, but we also need to reason
-about the inverse composition.
+We also need to be able to reason about the computational content of
+reflection after reification. By definition we have that
+$\reify \reflect V = V$, the following lemma lets us reason about the
+inverse composition.
 %
 \begin{lemma}[Reflect after reify]
 \label{lem:reflect-after-reify}
@@ -2917,10 +2892,10 @@ Follows from Lemmas~\ref{lem:decomposition},
 \ref{lem:reflect-after-reify}, and \ref{lem:forwarding}.
 \end{proof}
 %
-We now turn to our main result which is a simulation result in style
-of Plotkin~\cite{Plotkin75}. The theorem shows that the only extra
-behaviour exhibited by a translated term is the bureaucracy of
-deconstructing the continuation stack.
+Finally, we have the ingredients to state and prove the simulation
+result. The following theorem shows that the only extra behaviour
+exhibited by a translated term is the bureaucracy of deconstructing
+the continuation stack.
 %
 \begin{theorem}[Simulation]
 \label{thm:ho-simulation}
@@ -2933,18 +2908,18 @@ If $M \reducesto N$ then $\pcps{M} \reducesto^+ \areducesto^* \pcps{N}$.
   follows from Lemma~\ref{lem:handle-op}.
 \end{proof}
 %
-In common with most CPS translations, full abstraction does not
-hold. However, as our semantics is deterministic it is straightforward
-to show a backward simulation result.
-%
-\begin{corollary}[Backwards simulation]
-If $\pcps{M} \reducesto^+ \areducesto^* V$ then there exists $W$ such that
-$M \reducesto^* W$ and $\pcps{W} = V$.
-\end{corollary}
-%
-\begin{proof}
-  TODO\dots
-\end{proof}
+% In common with most CPS translations, full abstraction does not
+% hold. However, as our semantics is deterministic it is straightforward
+% to show a backward simulation result.
+% %
+% \begin{corollary}[Backwards simulation]
+% If $\pcps{M} \reducesto^+ \areducesto^* V$ then there exists $W$ such that
+% $M \reducesto^* W$ and $\pcps{W} = V$.
+% \end{corollary}
+% %
+% \begin{proof}
+%   TODO\dots
+% \end{proof}
 %
 \chapter{Abstract machine semantics}