From 566e5840d26311b10fe147d34c331c010c70b0a2 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Daniel=20Hillerstr=C3=B6m?= Date: Thu, 16 Jul 2020 01:23:58 +0100 Subject: [PATCH] Begin CPS chapter --- macros.tex | 78 ++++++++++- thesis.tex | 380 ++++++++++++++++++++++++++++++++++++++++++++++++++++- 2 files changed, 456 insertions(+), 2 deletions(-) diff --git a/macros.tex b/macros.tex index d15f8a1..6594bce 100644 --- a/macros.tex +++ b/macros.tex @@ -104,6 +104,7 @@ \newcommand{\rulelabel}[2]{\ensuremath{\mathsf{#1\textrm{-}#2}}} \newcommand{\klab}[1]{\rulelabel{K}{#1}} \newcommand{\semlab}[1]{\rulelabel{S}{#1}} +\newcommand{\usemlab}[1]{\rulelabel{U}{#1}} \newcommand{\tylab}[1]{\rulelabel{T}{#1}} \newcommand{\mlab}[1]{\rulelabel{M}{#1}} \newcommand{\siglab}[1]{\rulelabel{Sig}{#1}} @@ -114,6 +115,8 @@ %% \newcommand{\CatName}[1]{\textrm{#1}} \newcommand{\CompCat}{\CatName{Comp}} +\newcommand{\UCompCat}{\CatName{UComp}} +\newcommand{\UValCat}{\CatName{UVal}} \newcommand{\ValCat}{\CatName{Val}} \newcommand{\VarCat}{\CatName{Var}} \newcommand{\ValTypeCat}{\CatName{VType}} @@ -130,6 +133,7 @@ \newcommand{\TyEnvCat}{\CatName{TyEnv}} \newcommand{\KindEnvCat}{\CatName{KindEnv}} \newcommand{\EvalCat}{\CatName{Cont}} +\newcommand{\UEvalCat}{\CatName{UCont}} \newcommand{\HandlerCat}{\CatName{HDef}} %% @@ -166,4 +170,76 @@ %% %% Partiality %% -\newcommand{\pto}[0]{\ensuremath{\rightharpoonup}} \ No newline at end of file +\newcommand{\pto}[0]{\ensuremath{\rightharpoonup}} + +%% +%% Lists +%% +\newcommand{\nil}{\ensuremath{[]}} +\newcommand{\cons}{\ensuremath{::}} + +\newcommand{\concat}{\mathbin{+\!\!+}} +\newcommand{\revconcat}{\mathbin{\widehat{\concat}}} + +%% +%% CPS notation +%% +% static / dynamic stuff +\newcommand{\scol}[1]{{\color{blue}#1}} +\newcommand{\dcol}[1]{{\color{red}#1}} + +\newcommand{\static}[1]{\scol{\overline{#1}}} +\newcommand{\dynamic}[1]{\dcol{\underline{#1}}} +\newcommand{\nary}[1]{\overline{#1}} + +\newcommand{\slam}{\static{\lambda}} +\newcommand{\dlam}{\dynamic{\lambda}} +\newcommand{\sapp}{\mathbin{\static{@}}} +\newcommand{\dapp}{\mathbin{\dynamic{@}}} + +\newcommand{\reify}{\mathord{\downarrow}} +\newcommand{\reflect}{\mathord{\uparrow}} + +\newcommand{\scons}{\mathbin{\static{\cons}}} +\newcommand{\dcons}{\mathbin{\dynamic{\cons}}} + +\newcommand{\snil}{\static{\nil}} +\newcommand{\dnil}{\dynamic{\nil}} + +\newcommand{\sRecord}[1]{\static{\langle}#1\static{\rangle}} +\newcommand{\dRecord}[1]{\dynamic{\langle}#1\dynamic{\rangle}} + +%\newcommand{\sP}{\mathcal{P}} +\newcommand{\sQ}{\mathcal{Q}} +\newcommand{\sV}{\mathcal{V}} +\newcommand{\sW}{\mathcal{W}} + +\newcommand{\sM}{\mathcal{M}} +\renewcommand{\snil}{\reflect \dnil} + +\newcommand{\cps}[1]{\ensuremath{\llbracket #1 \rrbracket}} +\newcommand{\pcps}[1]{\top\cps{#1}} + +\newcommand{\hforward}{M_{\textrm{forward}}} +\newcommand{\hid}{V_{\textrm{id}}} + +%%% Continuation names +%%% The following set of macros are a bit more consistent with those +%%% currently used by the abstract machine, and don't use the plural +%%% convention of functional programming. + +% dynamic +\newcommand{\dlf}{f} % let frames +\newcommand{\dlk}{s} % let continuations +\newcommand{\dhf}{q} % handler frames +\newcommand{\dhk}{k} % handler continuations +\newcommand{\dhkr}{rk} % reverse handler continuations + +% static +\newcommand{\slf}{\phi} % let frames +\newcommand{\slk}{\sigma} % let continuations +\newcommand{\shf}{\theta} % handler frames +\newcommand{\shk}{\kappa} % handler continuations + +\newcommand{\sP}{\mathcal{P}} +\newcommand{\VS}{VS} diff --git a/thesis.tex b/thesis.tex index 3eb4fee..0258c81 100644 --- a/thesis.tex +++ b/thesis.tex @@ -1890,7 +1890,385 @@ getting stuck on an unhandled operation. \part{Implementation} -\chapter{Continuation passing styles} +\chapter{Continuation-passing styles} +\label{ch:cps} + +Continuation-passing style (CPS) is a \emph{canonical} program +notation that makes every facet of control flow and data flow +explicit. In CPS every function takes an additional function-argument +called the \emph{continuation}, which represents the next computation +in evaluation position. CPS is canonical in the sense that is +definable in pure $\lambda$-calculus with any primitives. As an +informal illustration of CPS consider the rudimentary factorial +function in \emph{direct-style}: +% +\[ + \bl + \dec{fac} : \Int \to \Int\\ + \dec{fac} \defas \lambda n. + \ba[t]{@{~}l} + \If\;n = 0\;\Then\;\Return\;1\\ + \Else\; + \ba[t]{@{~}l} + \Let\; n' \revto n - 1\;\In\\ + \Let\; res \revto \dec{fac}~n'\;\In\\ + n * res + \ea + \ea + \el +\] +% +In CPS notation the function becomes +% +\[ + \bl + \dec{fac}_{\dec{cps}} : \Int \to (\Int \to \alpha) \to \alpha\\ + \dec{fac}_{\dec{cps}} \defas \lambda n.\lambda k. + \ba[t]{@{~}l} + \If\;n = 0\;\Then\; k~1\\ + \Else\; + -_{\dec{cps}}~n~1~(\lambda n'. \dec{fac}_{cps}~n'~(\lambda res. k~(n * res))) + \ea + \el +\] + + +\section{Target calculus} +\label{sec:target-cps} + +The target calculus is given in Fig.~\ref{fig:cps-cbv-target}. +% +As in $\BCalc$ there is a syntactic distinction between values ($V$) +and computations ($M$). +% +Values ($V$) comprise: lambda abstractions ($\lambda x.M$); recursive +functions ($\Rec\,g\,x.M$); empty tuples ($\Record{}$); pairs +($\Record{V,W}$); and first-class labels ($\ell$). In +Section~\ref{sec:first-order-explicit-resump}, we will extend the values to +also include convenience constructors for building resumptions and +invoking structured continuations. +% +Computations ($M$) comprise: values ($V$); applications ($M \; V$); +pair elimination ($\Let\; \Record{x, y} = V \;\In\; N$); label +elimination ($\Case\; V \;\{\ell \mapsto M; x \mapsto N\}$); and +explicit marking of unreachable code ($\Absurd$). We permit the +function position of an application to be a computation (i.e., the +application form is $M~W$ rather than $V~W$). This relaxation is used +in our initial CPS translations, but will be ruled out in our final +translation when we start to use explicit lists to represent stacks of +handlers in Section~\ref{sec:first-order-uncurried-cps}. + +The reductions for functions, pairs, and first-class labels are +standard. + +We define syntactic sugar for variant values, record values, list +values, let binding, variant eliminators, and record eliminators. We +assume standard $n$-ary generalisations and use pattern matching +syntax for deconstructing variants, records, and lists. For desugaring +records, we assume a failure constant $\ell_\bot$ (e.g. a divergent +term) to cope with the case of pattern matching failure. + +\begin{figure} + \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 + \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 \\ + \end{syntax} + + \textbf{Reductions} + \begin{reductions} + \usemlab{App} & (\lambda x . \, M) V &\reducesto& M[V/x] \\ + \usemlab{Rec} & (\Rec\,g\,x.M) V &\reducesto& M[\Rec\,g\,x.M/g,V/x]\\ + \usemlab{Split} & \Let \; \Record{x,y} = \Record{V,W} \; \In \; N &\reducesto& N[V/x,W/y] \\ + \usemlab{Case_1} & + \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} + + \textbf{Syntactic sugar} +\[ + \begin{eqs} + \Let\;x=V\;\In\;N &\equiv & N[V/x]\\ + \ell \; V & \equiv & \Record{\ell; V}\\ + \Record{} & \equiv & \ell_{\Record{}} \\ + \Record{\ell = V; W} & \equiv & \Record{\ell, \Record{V, W}}\\ + \nil &\equiv & \ell_{\nil} \\ + V \cons W & \equiv & \Record{\ell_{\cons}, \Record{V, W}}\\ + \Case\;V\;\{\ell\;x \mapsto M; y \mapsto N \} &\equiv& + \ba[t]{@{~}l} + \Let\;y = V\;\In\; \Let\;\Record{z,x} = y\;\In \\ + \Case\; z\;\{ \ell \mapsto M; z' \mapsto N \} + \ea\\ + \Let\; \Record{\ell=x;y} = V\;\In\;N &\equiv& + \ba[t]{@{~}l} + \Let\; \Record{z,z'} = V\;\In\;\Let\; \Record{x,y} = z'\;\In \\ + \Case\;z\;\{\ell \mapsto N; z'' \mapsto \ell_\bot \} + \ea + \end{eqs} +\] + +\caption{Untyped target calculus for the CPS translations.} +\label{fig:cps-cbv-target} +\end{figure} + +\section{CPS transform for fine-grain call-by-value} +\label{sec:cps-cbv} + +We start by giving a CPS translation of the operation and handler-free +subset of $\BCalc$ in Figure~\ref{fig:cps-cbv}. Fine-grain +call-by-value admits a particularly simple CPS translation due to the +separation of values and computations. All constructs from the source +language are translated homomorphically into the target language, +except for $\Return$, $\Let$, and type abstraction (the translation +performs type erasure). Lifting a value $V$ to a computation +$\Return~V$ is interpreted by passing the value to the current +continuation. Sequencing computations with $\Let$ is translated in the +usual continuation passing way. In addition, we explicitly +$\eta$-expand the translation of a type abstraction in order to ensure +that value terms in the source calculus translate to value terms in +the target. + +\begin{figure} +\flushleft +\textbf{Values} \\ +\[ +\bl + +\begin{eqs} + \cps{-} &:& \ValCat \to \UValCat\\ +\cps{x} &=& x \\ +\cps{\lambda x.M} &=& \lambda x.\cps{M} \\ +\cps{\Lambda \alpha.M} &=& \lambda k.\cps{M}~k \\ +\cps{\Rec\,g\,x.M} &=& \Rec\,g\,x.\cps{M}\\ +\cps{\Record{}} &=& \Record{} \\ +\cps{\Record{\ell = V; W}} &=& \Record{\ell = \cps{V}; \cps{W}} \\ +\cps{\ell~V} &=& \ell~\cps{V} \\ +\end{eqs} +\el +\] +\textbf{Computations} +\[ +\bl +\begin{eqs} +\cps{-} &:& \CompCat \to \UCompCat\\ +\cps{V\,W} &=& \cps{V}\,\cps{W} \\ +\cps{V\,T} &=& \cps{V} \\ +\cps{\Let\; \Record{\ell=x;y} = V \; \In \; N} &=& \Let\; \Record{\ell=x;y} = \cps{V} \; \In \; \cps{N} \\ +\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{\Let~x \revto M~\In~N} &=& \lambda k.\cps{M}(\lambda x.\cps{N}k) \\ +\end{eqs} +\el +\] +\caption{First-order CPS translation of fine-grain call-by-value.} +\label{fig:cps-cbv} +\end{figure} + +\subsection{First-Order CPS Translations of Handlers} +\label{sec:fo-cps} + +As is usual for CPS, the translation of a computation term by the +basic CPS translation in Section~\ref{sec:cps-cbv} takes a single +continuation parameter that represents the context. +% +With effects and handlers in the source language, we must now keep +track of two kinds of context in which each computation executes: a +\emph{pure context} that tracks the state of pure computation in the +scope of the current handler, and an \emph{effect context} that +describes how to handle operations in the scope of the current +handler. +% +Correspondingly, we have both \emph{pure continuations} ($k$) and +\emph{effect continuations} ($h$). +% +As handlers can be nested, each computation executes in the context of +a \emph{stack} of pairs of pure and effect continuations. + +On entry into a handler, the pure continuation is initialised to a +representation of the return clause and the effect continuation to a +representation of the operation clauses. As pure computation proceeds, +the pure continuation may grow, for example when executing a +$\Let$. If an operation is encountered then the effect continuation is +invoked. +% +The current continuation pair ($k$, $h$) is packaged up as a +\emph{resumption} and passed to the current handler along with the +operation and its argument. The effect continuation then either +handles the operation, invoking the resumption as appropriate, or +forwards the operation to an outer handler. In the latter case, the +resumption is modified to ensure that the context of the original +operation invocation can be reinstated when the resumption is invoked. + +The translations introduced in this subsection differ in how they +represent stacks of pure and effect continuations, and how they +represent resumptions. +% +The first translation represents the stack of continuations using +currying, and resumptions as functions +(Section~\ref{sec:first-order-curried-cps}). +% +Currying obstructs proper tail-recursion, so we move to an explicit +representation of the stack +(Section~\ref{sec:first-order-uncurried-cps}). Then, in order to avoid +administrative reductions in our final higher-order one-pass +translation we use an explicit representation of resumptions +(Section~\ref{sec:first-order-explicit-resump}). Finally, in order to +support shallow handlers, we will use an explicit stack representation +for pure continuations (Section~\ref{sec:pure-as-stack}). + +\subsubsection{Curried Translation} +\label{sec:first-order-curried-cps} + +Our first translation builds upon the CPS 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 than accepting +a single continuation, translated computation terms now accept an +arbitrary even number of arguments representing the stack of pure and +effect continuations. Thus, the translation of core constructs remain +exactly the same as in Figure~\ref{fig:cps-cbv}, where we imagine +there being some number of extra continuation arguments that have been +$\eta$-reduced. The translation of operations and handlers is as +follows: +% +\begin{equations} +\cps{\Do\;\ell\;V} &=& \lambda k.\lambda h.h~\Record{\ell,\Record{\cps{V}, \lambda x.k~x~h}} \\ +\cps{\Handle \; M \; \With \; H} &=& \cps{M}~\cps{\hret}~\cps{\hops}, ~\text{where} \smallskip\\ +\multicolumn{3}{@{}l@{}}{ +\begin{eqs} +\qquad +\cps{\{ \Return \; x \mapsto N \}} &=& \lambda x . \lambda h . \cps{N} \\ +\cps{\{ \ell~p~r \mapsto N_\ell \}_{\ell \in \mathcal{L}}} +&=& +\lambda \Record{z,\Record{p,r}}. \Case~z~ + \{ (\ell \mapsto \cps{N_\ell})_{\ell \in \mathcal{L}}; y \mapsto \hforward(y,p,r) \} \\ + \hforward(y,p,r) &=& \lambda k. \lambda h. h\,\Record{y,\Record{p, \lambda x.\,r\,x\,k\,h}} +\end{eqs} +} +\end{equations} +% +The translation of $\Do\;\ell\;V$ abstracts over the current pure +($k$) and effect ($h$) continuations passing an encoding of the +operation into the latter. The operation is encoded as a triple +consisting of the name $\ell$, parameter $\cps{V}$, and resumption +$\lambda x.k~x~h$, which ensures that any subsequent operations are +handled by the same effect continuation $h$. + +The translation of $\Handle~M~\With~H$ invokes the translation of $M$ +with new pure and effect continuations for the return and operation +clauses of $H$. +% +The translation of a return clause is a term which garbage collects +the current effect continuation $h$. +% +The translation of a set of operation clauses is a function which +dispatches on encoded operations, and in the default case forwards to +an outer handler. +% +In the forwarding case, the resumption is extended by the parent +continuation pair in order to reinstate the handler stack, thereby +ensuring subsequent invocations of the same operation are handled +uniformly. + +The translation of complete programs feeds the translated term the +identity pure continuation (which discards its handler argument), and +an effect continuation that is never intended to be called: +\begin{equations} +\pcps{M} &=& \cps{M}~(\lambda x.\lambda h.x)~(\lambda \Record{z,\_}.\Absurd~z) \\ +\end{equations} +Conceptually, this translation encloses the translated program in a +top-level handler with an empty collection of operation clauses and an +identity return clause. + +There are three shortcomings of this initial translation that we +address below. + +\begin{itemize} +\item First, it is not \emph{properly tail-recursive}~\citep{DanvyF92, + Steele78} due to the curried representation of the continuation + stack, as a result the image of the translation is not stackless, + which makes it problematic to implement using a trampoline in, say, + JavaScript. (Properly tail-recursion CPS translations ensure that + all calls to functions and continuations are in tail position, hence + there is no need to maintain a stack.) We rectify this issue with an + explicit list representation in the next subsection. + +\item Second, it yields administrative redexes (redexes that could be + reduced statically). We will rectify this with a higher-order + one-pass translation in + Section~\ref{sec:higher-order-uncurried-cps}. + +\item Third, this translation cannot cope with shallow handlers. The + pure continuations $k$ are abstract and include the return clause of + the corresponding handler. Shallow handlers require that the return + clause of a handler is discarded when one of its operations is + invoked. We will fix this in Section~\ref{sec:pure-as-stack}, where we + will represent pure continuations as explicit stacks. +\end{itemize} + +To illustrate the first two issues, consider the following example: +\begin{equations} +\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)\\ + &\reducesto& \Record{} \\ +\end{equations} +The first reduction is administrative: it has nothing to do with the +dynamic semantics of the original term and there is no reason not to +eliminate it statically. The second and third reductions simulate +handling $\Return\;\Record{}$ at the top level. The second reduction +partially applies $\lambda x.\lambda h.x$ to $\Record{}$, which must +return a value so that the third reduction can be applied: evaluation +is not tail-recursive. +% +The lack of tail-recursion is also apparent in our relaxation of +fine-grain call-by-value in Figure~\ref{fig:cps-cbv-target}: the +function position of an application can be a computation, and the +calculus makes use of evaluation contexts. + +\paragraph*{Remark} +We originally derived this curried CPS translation for effect handlers +by composing \citeauthor{ForsterKLP17}'s translation from effect +handlers to delimited continuations~\citeyearpar{ForsterKLP17} with +\citeauthor{MaterzokB12}'s CPS translation for delimited +continuations~\citeyearpar{MaterzokB12}. + +\medskip + +Because of the administrative reductions, simulation is not on the +nose, but instead up to congruence. +% +For reduction in the untyped target calculus we write +$\reducesto_{\textrm{cong}}$ for the smallest relation containing +$\reducesto$ that is closed under the term formation constructs. +% +\begin{theorem}[Simulation] + \label{thm:fo-simulation} + If $M \reducesto N$ then $\pcps{M} \reducesto_{\textrm{cong}}^+ + \pcps{N}$. +\end{theorem} + +\begin{proof} +The result follows by composing a call-by-value variant of +\citeauthor{ForsterKLP17}'s translation from effect handlers to +delimited continuations~\citeyearpar{ForsterKLP17} with +\citeauthor{MaterzokB12}'s CPS translation for delimited +continuations~\citeyearpar{MaterzokB12}. +\end{proof} + \chapter{Abstract machine semantics} \part{Expressiveness}