From 0719961a3f03ddb3325d6a6dad55696f0e138328 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Daniel=20Hillerstr=C3=B6m?= Date: Tue, 28 Jul 2020 15:41:22 +0100 Subject: [PATCH] Uncurried CPS translation --- thesis.bib | 34 ++++++++++- thesis.tex | 161 +++++++++++++++++++++++++---------------------------- 2 files changed, 108 insertions(+), 87 deletions(-) diff --git a/thesis.bib b/thesis.bib index cb593b6..c5cc28f 100644 --- a/thesis.bib +++ b/thesis.bib @@ -169,7 +169,7 @@ Matija Pretnar}, title = {On the Expressive Power of User-Defined Effects: Effect Handlers, Monadic Reflection, Delimited Control}, - journal = {Proc. ACM Program. Lang.}, + journal = {{PACMPL}}, volume = {1}, number = {ICFP}, articleno = {13}, @@ -178,6 +178,19 @@ year = {2017} } +@article{ForsterKLP19, + author = {Yannick Forster and + Ohad Kammar and + Sam Lindley and + Matija Pretnar}, + title = {On the expressive power of user-defined effects: Effect handlers, + monadic reflection, delimited control}, + journal = {J. Funct. Program.}, + volume = {29}, + pages = {e15}, + year = {2019} +} + # Eff @article{BauerP15, author = {Andrej Bauer and @@ -538,6 +551,14 @@ year = {1975} } +@techreport{Steele78, + title = {{RABBIT}: A Compiler for {SCHEME}}, + author = {Guy Steele}, + number = {AITR-474}, + institution = {{INRIA}}, + year = {1978}, +} + @inproceedings{DanvyF90, author = {Olivier Danvy and Andrzej Filinski}, @@ -547,6 +568,17 @@ year = {1990} } +@article{DanvyF92, + author = {Olivier Danvy and + Andrzej Filinski}, + title = {Representing Control: {A} Study of the {CPS} Transformation}, + journal = {Mathematical Structures in Computer Science}, + volume = {2}, + number = {4}, + pages = {361--391}, + year = {1992} +} + @book{Appel92, author = {Andrew W. Appel}, title = {Compiling with Continuations}, diff --git a/thesis.tex b/thesis.tex index b4a58df..706ec5c 100644 --- a/thesis.tex +++ b/thesis.tex @@ -2121,7 +2121,7 @@ translate to value terms in the target. \label{fig:cps-cbv} \end{figure} -\subsection{First-order CPS translations of effect handlers} +\section{First-order CPS translations of effect handlers} \label{sec:fo-cps} The translation of a computation term by the basic CPS translation in @@ -2157,7 +2157,7 @@ resumption is modified to ensure that the context of the original operation invocation can be reinstated when the resumption is invoked. % -\subsubsection{Curried translation} +\subsection{Curried translation} \label{sec:first-order-curried-cps} We first consider a curried CPS translation that builds the @@ -2173,19 +2173,14 @@ 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{\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{\{ \Return \; x \mapsto N \}} &\defas& \lambda x . \lambda h . \cps{N} \\ \cps{\{ \ell~p~r \mapsto N_\ell \}_{\ell \in \mathcal{L}}} -&=& +&\defas& \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} -} +\hforward(y,p,r) &\defas& \lambda k. \lambda h. h\,\Record{y,\Record{p, \lambda x.\,r\,x\,k\,h}} \end{equations} % The translation of $\Do\;\ell\;V$ abstracts over the current pure @@ -2207,9 +2202,8 @@ 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. +continuation pair to ensure that an eventual invocation of the +resumption reinstates the handler stack. The translation of complete programs feeds the translated term the identity pure continuation (which discards its handler argument), and @@ -2223,52 +2217,72 @@ 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. +We may regard this particular CPS translation as being simple, because +it requires virtually no extension to the CPS translation for +$\BCalc$. However, this translation suffers from two deficiencies +which makes it unviable in practice. + +\begin{enumerate} + \item The image of the translation is not \emph{properly + tail-recursive}~\citep{DanvyF92,Steele78}, and as a result the + image is not stackless, meaning it cannot readily be used as the + 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 + administrative redexes, i.e. redexes that could be reduced + statically. This is a classic problem with CPS translation, which + is typically dealt with by introducing a second pass to clean up + the image~\cite{DanvyF92}. +\end{enumerate} + +The following example readily illustrates both issues. +% +\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. We will address this issue in +Section~\ref{sec:higher-order-cps}. 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. We will address this issue in +Section~\ref{sec:first-order-uncurried-cps}. +% +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. + +Nevertheless, we can show that the image of this CPS translation +simulates the preimage. Due to the presence of administrative +reductions, the 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{ForsterKLP19}'s translation from effect handlers to +delimited continuations~\citeyearpar{ForsterKLP19} with +\citeauthor{MaterzokB12}'s CPS translation for delimited +continuations~\citeyearpar{MaterzokB12}. +\end{proof} % \paragraph*{Remark} % We originally derived this curried CPS translation for effect handlers @@ -2277,31 +2291,6 @@ identity return clause. % \citeauthor{MaterzokB12}'s CPS translation for delimited % continuations~\citeyearpar{MaterzokB12}. -% \medskip - -\dhil{Discuss deficiencies of the curried translation} -\dhil{State simulation result} -% 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}