Define the parity of a continuation

thesis.tex

@@ -2286,15 +2286,13 @@ unviable in practice.
 
 The following minimal example readily illustrates both issues.
 %
-\begin{equations}
+\begin{align*}
 \pcps{\Return\;\Record{}}
-     &=         & (\lambda k.k\,\Record{})\,(\lambda x.\lambda h.x)\,(\lambda \Record{z,\_}.\Absurd\,z)  \\
-     &\reducesto& ((\lambda x.\lambda h.x)\,\Record{})\,(\lambda \Record{z,\_}.\Absurd\,z) \\
-     &\reducesto& (\lambda h.\Record{})\,(\lambda \Record{z,\_}.\Absurd\,z) \numberthis\label{eq:cps-admin-reduct} \\
-     &\reducesto& \Record{} \\
-\end{equations}
-%
-\dhil{Mark the second reduction, so that it can be referred back to}
+     =         & (\lambda k.k\,\Record{})\,(\lambda x.\lambda h.x)\,(\lambda \Record{z,\_}.\Absurd\,z)  \\
+     \reducesto& ((\lambda x.\lambda h.x)\,\Record{})\,(\lambda \Record{z,\_}.\Absurd\,z) \numberthis\label{eq:cps-admin-reduct-1}\\
+     \reducesto& (\lambda h.\Record{})\,(\lambda \Record{z,\_}.\Absurd\,z) \numberthis\label{eq:cps-admin-reduct-2}\\
+     \reducesto& \Record{}
+\end{align*}
 %
 The second and third reductions simulate handling $\Return\;\Record{}$
 at the top level. The second reduction partially applies the curried
@@ -2401,8 +2399,6 @@ These changes to $\UCalc$ immediately invalidate 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
@@ -2453,7 +2449,7 @@ 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
 extract the top continuation $k$ and manipulate it analogously to the
-original translation in Figure\ \ref{fig:cps-cbv}. For $\Do$, we
+original translation in Figure~\ref{fig:cps-cbv}. For $\Do$, we
 extract the top pure continuation $k$ and effect continuation $h$ and
 invoke $h$ in the same way as the curried translation, except that we
 explicitly maintain the stack $ks$ of additional continuations. The
@@ -2477,7 +2473,7 @@ 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) \numberthis\label{eq:cps-admin-reduct-2}\\
+     &\reducesto& (\lambda x.\lambda ks.x)\,\Record{}\,((\lambda \Record{z,\_}.\lambda ks.\Absurd\,z) \cons \nil)\\
      &\reducesto& \Record{}
 \end{equations}
 %
@@ -2485,11 +2481,11 @@ The reduction sequence in the image of this uncurried translation has
 one fewer steps (disregarding the administrative steps induced by
 pattern matching) than in the image of the curried translation. The
 `missing' step is precisely the reduction marked
-(\ref{eq:cps-admin-reduct}), which was a partial application of the
+\eqref{eq:cps-admin-reduct-2}, which was a partial application of the
 initial pure continuation function that was not in tail
-position. Note, however, that the first reduction
-(\ref{eq:cps-admin-reduct-2}) remains administrative, the reduction is
-entirely static, and as such, it can be dealt with as part of the
+position. Note, however, that the first reduction (corresponding to
+\eqref{eq:cps-admin-reduct-1}) remains administrative, the reduction
+is entirely static, and as such, it can be dealt with as part of the
 translation.
 %
 
@@ -2756,66 +2752,94 @@ $\reify \sV$ by induction on their structure.
   \ea
 \]
 %
-%\dhil{Need to spell out that static pattern matching may induce dynamic (administrative) reductions}
-%
+
 \paragraph{Higher-order translation}
 %
+As we shall see this translation manipulates the continuation
+intricate ways; and since we maintain the interpretation of the
+continuation as an alternating list of pure continuation functions and
+effect continuation functions it is useful to define the `parity' of a
+continuation as follows:
+%
+a continuation is said to be \emph{odd} if the top element is an
+effect continuation function, otherwise it is said to \emph{even}.
+
+%
+
 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 almost homomorphic on the syntax
-constructors. The notable exceptions are the translations of
-$\lambda$-abstractions and $\Lambda$-abstractions. The former gives
-rise to dynamic computation at runtime, and thus, the translation
-emits a dynamic $\dlam$-abstraction with two formal parameters: the
-function parameter, $x$, and the continuation parameter, $ks$. The
-body of the $\dlam$-abstraction is somewhat anomalous as the
-continuation $ks$ is subject to immediate dynamic deconstruction just
-to be reconstructed again and used as a static argument to the
-translation of the original body computation $M$. This deconstruction
-and reconstruction may at first glance appear to be rather pointless,
-however, a closer look reveals that it performs a critical role as it
-ensures that the translation on computation terms has immediate access
-to the next pure and effect continuation functions. In fact, the
-translation is set up such that every generated dynamic
-$\dlam$-abstraction deconstructs its continuation argument
-appropriately to expose just enough (static) continuation structure in
-order to guarantee that static pattern matching never fails.
-%
-(The translation is somewhat unsatisfactory regarding this
-deconstruction of dynamic continuations as the various generated
-dynamic lambda abstractions do not deconstruct their continuation
-arguments uniformly.)
-%
-Since the target language is oblivious to types any
-$\Lambda$-abstraction gets translated in a similar way to
-$\lambda$-abstraction, where the first parameter becomes a placeholder
-for a ``dummy'' unit argument.
+As before, the translation comprises three translation functions, one
+for each syntactic category: values, computations, and handler
+definitions. Amongst the three functions, the translation function for
+computations stands out, because it is the only one that operates on
+static continuations. Its type signature,
+$\cps{-} : \CompCat \to \SValCat^\ast \to \UCompCat$, signifies that
+it is a binary function, taking a $\HCalc$-computation term as its
+first argument and a static continuation (a list of static values) as
+its second argument, and ultimately produces a $\UCalc$-computation
+term. Thus the computation translation function is able to manipulate
+the continuation. In fact, the translation is said to be higher-order
+because the continuation parameter is a higher-order: it is a list of
+functions.
 
-The translation of computation terms is more interesting. Note the
-type of the translation function,
-$\cps{-} : \CompCat \to \SValCat^\ast \to \UCompCat$. It is a binary
-function, taking a $\HCalc$-computation term as its first argument and
-a static continuation as its second argument, and ultimately produces
-a $\UCalc$-computation term. The static continuation may be
-manipulated during the translation as is done in the translations of
-$\Return$, $\Let$, $\Do$, and $\Handle$. The translation of $\Return$
-consumes the next pure continuation function $\sk$ and applies it
-dynamically to the translation of $V$ and the reified remainder,
-$\sks$, of the static continuation. Keep in mind that the translation
-of $\Return$ only consumes one of the two guaranteed available
-continuation functions from the provided continuation argument; as a
-consequence the next continuation function in $\sks$ is an effect
-continuation. This consequence is accounted for in the translations of
-$\Let$ and $\Return$-clauses, which are precisely the two possible
-(dynamic) origins of $\sk$. For instance, the translation of $\Let$
+To ensure that static continuation manipulation is well-defined the
+translation maintains the invariant that the statically known
+continuation stack ($\sk$) always contains at least two continuation
+functions, i.e. a complete continuation pair consisting of a pure
+continuation function and an effect continuation function.
+%
+This invariant guarantees that all translations are uniform in whether
+they appear statically within the scope of a handler or not, and this
+also simplifies the correctness proof
+(Theorem~\ref{thm:ho-simulation}).
+%
+Maintaining this invariant has a cosmetic effect on the presentation
+of the translation. This effect manifests in any place where a
+dynamically known continuation stack is passed in (as a continuation
+parameter $\dhk$), as it must be deconstructed using a dynamic
+language $\Let$ to expose the continuation structure and subsequently
+reconstructed as a static value with reflected variable names.
+
+The translation of $\lambda$-abstractions provides an example of this
+deconstruction and reconstruction in action. The dynamic continuation
+$\dhk$ is deconstructed to expose to the next pure continuation
+function $\dk$ and effect continuation $h$, and the remainder of the
+continuation $\dhk'$; these names are immediately reflected and put
+back together to form a static continuation that is provided to the
+translation of the body computation $M$.
+
+The only translation rule that consumes a complete reflected
+continuation pair is the translation of $\Do$. The effect continuation
+function, $\sh$, is dynamically applied to an operation package and
+the reified remainder of the continuation $\sks$. As usual, the
+operation package contains the payload and the resumption, which is
+represented as a reversed continuation slice.
+%
+The only other translation rules that manipulate the continuation are
+$\Return$ and $\Let$, which only consume the pure continuation
+function $\sk$. For example, the translation of $\Return$ is a dynamic
+application of $\sk$ to the translation of the value $V$ and the
+remainder of the continuation $\sks$.
+%
+The shape of $\sks$ is odd, meaning that the top element is an effect
+continuation function. Thus the pure continuation $\sk$ has to account
+for this odd shape. Fortunately, the possible instantiations of the
+pure continuation are few. We can derive the all possible
+instantiations systematically by using the operational semantics of
+$\HCalc$. According to the operational semantics the continuation of a
+$\Return$-computation is either the continuation of a
+$\Let$-expression or a $\Return$-clause (a bare top-level
+$\Return$-computation is handled by the $\pcps{-}$ translation).
+%
+The translations of $\Let$-expressions and $\Return$-clauses each
+account for odd continuations. For example, the translation of $\Let$
 consumes the current pure continuation function and generates a
 replacement: a pure continuation function which expects an odd dynamic
-continuation $ks$, which it deconstructs to expose the effect
+continuation $\dhk$, which it deconstructs to expose the effect
 continuation $h$ along with the current pure continuation function in
 the translation of $N$. The modified continuation is passed to the
 translation of $M$.
@@ -2880,110 +2904,23 @@ continuation in order to bind the current effect continuation function
 to the name $h$, which would have been used during the translation of
 $N$.
 
-The translation of $\Do$ consumes both the current pure continuation
-function and current effect continuation function. It applies the
-effect continuation function dynamically to an operation package and
-the reified remainder of the continuation. As usual, the operation
-package contains the payload and the resumption, which is a reversed
-slice of the provided continuation. The translation of $\Handle$
-applies the translation of $M$ to the current continuation extended
-with the translation of the $\Return$-clause, acting as a pure
-continuation function, and the translation of operation-clauses,
-acting as an effect continuation function.
-
-The translation of a return clause $\hret$ of some handler $H$
-generates a dynamic lambda abstraction, which expects an odd
-continuation. In its body it extracts three elements from the
-continuation parameter $ks$. The first element is discarded as it is
-the effect continuation corresponding to the translation of
-$\hops$. The other two elements are used to statically expose the next
-pure and effect continuation functions in the translation of $N$.
+The translation of $\Handle$ applies the translation of $M$ to the
+current continuation extended with the translation of the
+$\Return$-clause, acting as a pure continuation function, and the
+translation of operation-clauses, acting as an effect continuation
+function.
 %
-The translation of $\hops$ also generates a dynamic lambda
-abstraction, which unpacks the operation package to perform a
-case-split on the operation label $z$. The continuation $ks$ is
-deconstructed in the branch for $\ell$ in order to expose the
+The translation of a $\Return$-clause discards the effect continuation
+$h$ and in addition exposes the next pure continuation $\dk$ and
+effect continuation $h'$ which are reflected to form a static
+continuation for the translation of $N$.
+%
+The translation of operation clauses unpacks the provided operation
+package to perform a case-split on the operation label $z$. The branch
+for $\ell$ deconstructs the continuation $\dhk$ in order to expose the
 continuation structure. The forwarding branch also deconstructs the
-continuation, however, for a different purpose, namely, to augment the
-resumption $rs$ the next pure and effect continuation functions.
-%
-\dhil{Remark that an alternative to cluttering the translations with
-  unpacking and repacking of continuations would be to make static
-  pattern generate dynamic let bindings whenever necessary. While it
-  may reduce the dynamic administrative reductions, it makes the
-  simulation proof more complicated.}
-
-% : the $\dlam$-abstractions generated by translating $\lambda$-abstractions, $\Lambda$-abstractions, and operation clauses expose the next two continuation functions, whilst the dynamic lambda abstraction generated by translating $\Let$ only expose the next continuation, others expose only the next one, and the translation of
-% $\lambda$-abstractions expose the next two continuation functions, 
-
-
-
-% The translation on values and handler definitions generates dynamic
-% lambda abstractions. Whilst the translation on computations generates
-% static lambda abstractions.
-
-% Static continuation application corresponds to
-
-% The translation function for computation terms is staged: for any
-% given computation term the translation yields a static function, which
-% can be applied to a static continuation to ultimately yield a
-% $\UCalc$-computation term. Staging is key to eliminating static
-% administrative redexes as any static function may perform static
-% computation by manipulating its provided static continuation
-
-
-% a binary higher-order
-% function; it is higher-order because its second parameter is a list of
-% static continuation functions.
-
-% 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. The
-% translations presented by \citet{HillerstromLAS17} and
-% \citet{HillerstromL18} did not do this decomposition and repackaging
-% step, which resulted in additional administrative reductions in the
-% translation due to the translations of $\Let$ and $\Do$ being passed
-% dynamic continuations when they were expecting statically known ones.
-%
-
-% The translation on values is mostly homomorphic on the syntax
-% constructors, except for $\lambda$-abstractions 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'.}
+continuation, but for a different purpose; it augments the resumption
+$\dhkr$ with the next pure and effect continuation functions.
 
 Let us revisit the example from
 Section~\ref{sec:first-order-curried-cps} to see that the higher-order
@@ -2996,10 +2933,38 @@ translation eliminates the static redex at translation time.
     &\reducesto& \Record{}
 \end{equations}
 %
-In contrast with the previous translations, the image of this
-translation admits only a single dynamic reduction (disregarding the
-dynamic administrative reductions arising from continuation
-construction and deconstruction).
+In contrast with the previous translations, the reduction sequence in
+the image of this translation contains only a single dynamic reduction
+(disregarding the dynamic administrative reductions arising from
+continuation construction and deconstruction); both
+\eqref{eq:cps-admin-reduct-1} and \eqref{eq:cps-admin-reduct-2}
+reductions have been eliminated as part of the translation.
+
+The elimination of static redexes coincides with a refinements of the
+target calculus. Unary application is no longer a necessary
+primitive. Every unary application dealt with by the metalanguage,
+i.e. all unary applications are static.
+
+\paragraph{Implicit lazy continuation deconstruction}
+%
+An alternative to the explicit deconstruction of continuations is to
+implicitly deconstruct continuations on demand when static pattern
+matching fails. This was the approach taken by
+\citet*{HillerstromLAS17}. On one hand this approach leads to a
+slightly slicker presentation. On the other hand it complicates the
+proof of correctness as one must account for static pattern matching
+failure.
+%
+A practical argument in favour of the explicit eager continuation
+deconstruction is that it is more accessible from an implementation
+point of view. No implementation details are hidden away in side
+conditions.
+%
+Furthermore, it is not clear that lazy deconstruction has any
+advantage over eager deconstruction, as the translation must reify the
+continuation when it transitions from computations to values and
+reflect the continuation when it transitions from values to
+computations, in which case static pattern matching would fail.
 
 \subsubsection{Correctness}
 \label{sec:higher-order-cps-deep-handlers-correctness}
@@ -3120,7 +3085,7 @@ reductions, i.e.
 %
 \[
 \cps{M} \sapp (\sV_1 \scons \dots \sV_n \scons \reflect \reify \sW)
-  \areducesto^* \cps{M} \sapp (\sV_1 \scons \dots \sV_n \scons \sW)
+  \areducesto^\ast \cps{M} \sapp (\sV_1 \scons \dots \sV_n \scons \sW)
 \]
 \end{lemma}
 %
@@ -3406,53 +3371,6 @@ interpretation of continuations.
 Although it is seductive to program with lists, it quickly gets
 unwieldy.
 
-% The underlying issue is that the continuation structure is still too
-% extensional. The need for a more intensional structure is evident in
-% the insertion of $\kid$ in the translation of $\Handle$ as a
-% placeholder for the empty pure continuation. Another telltale for a
-% more general notion of continuation is that continuation
-% deconstructions are non-uniform due to the single flat list
-% continuation representation. While stuffing everything into lists is
-% seductive, it quickly gets unwieldy.
-
-% Instead of inserting dummy handlers, one may consider composing the
-% current pure continuation with the next pure continuation, meaning
-% that the current pure continuation would be handled accordingly by the
-% next handler. To retrieve the next pure continuation, we must reach
-% under the next handler, i.e. something along the lines of the
-% following.
-% %
-% \[
-%   \bl
-%     \Let\;(\_ \dcons \_ \dcons \dk \dcons \vhops \dcons \vhret \dcons \dk' \dcons rs') = rs\;\In\\
-%     \Let\;r = \Res\,(\vhops \dcons \vhret \dcons (\dk' \circ \dk) \dcons rs')\;\In\;\dots
-%   \el
-% \]
-% %
-% where $\circ$ is defined to be function composition in continuation
-% passing style.
-% %
-% \[
-%   g \circ f \defas \lambda x\,\dhk.
-%     \ba[t]{@{}l}
-%       \Let\;(\dk \dcons \dhk') = \dhk\; \In\\
-%       f \dapp x \dapp ((\lambda x\,\dhk. g \dapp x \dapp (\dk \dcons \dhk)) \dcons \dhk')
-%     \ea
-% \]
-% %
-% This idea is cute, but it reintroduces a variation of the dynamic
-% redexes we dealt with in
-% Section~\ref{sec:first-order-explicit-resump}.
-% %
-% Both solutions side step the underlying issue, namely, that the
-% continuation structure is still too extensional. The need for a more
-% intensional structure is evident in the insertion of $\kid$ in the
-% translation of $\Handle$ as a placeholder for the empty pure
-% continuation. Another telltale is that the disparity of continuation
-% deconstructions also gets bigger. The continuation representation
-% needs more structure. While it is seductive to program with lists, it
-% quickly gets unwieldy.
-
 \subsection{Generalised continuations}
 \label{sec:generalised-continuations}