From 95035458ece2c11d3c84b19725004ec3de1423c1 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Daniel=20Hillerstr=C3=B6m?= Date: Wed, 3 Mar 2021 14:22:56 +0000 Subject: [PATCH] CPS translation for parameterised handlers (figure) --- thesis.tex | 145 ++++++++++++++++++++++++++++++++++++++++++++++++++++- 1 file changed, 143 insertions(+), 2 deletions(-) diff --git a/thesis.tex b/thesis.tex index 58c56f0..13d4f15 100644 --- a/thesis.tex +++ b/thesis.tex @@ -9554,7 +9554,7 @@ If $M \reducesto N$ then $\pcps{M} \reducesto^+ \areducesto^* \pcps{N}$. % \end{proof} % -\section{CPS transforming shallow effect handlers} +\section{Transforming shallow effect handlers} \label{sec:cps-shallow} In this section we will continue to build upon the higher-order @@ -10285,13 +10285,154 @@ result. % \begin{lemma}[Backwards simulation] If $\pcps{M} \reducesto^+ V$ then there exists $W$ - such that $M \reducesto^* W$ and $\pcps{W} = V$. + such that $M \reducesto^\ast W$ and $\pcps{W} = V$. \end{lemma} % \begin{corollary} $M \reducesto^\ast V$ if and only if $\pcps{M} \reducesto^\ast \pcps{V}$. \end{corollary} +\section{Transforming parameterised handlers} + +\begin{figure}[t] +\textbf{Continuation reductions} +% +\begin{reductions} +\usemlab{KAppNil} & + \kapp \; (\dRecord{\dnil, \dRecord{q, v, e}} \dcons \dhk) \, V &\reducesto& v \dapp \dRecord{q,V} \dapp \dhk \\ +\usemlab{KAppCons} & + \kapp \; (\dRecord{\dlf \dcons \dlk, h} \dcons \dhk) \, V &\reducesto& \dlf \dapp V \dapp (\dRecord{\dlk, h} \dcons \dhk) \\ +\end{reductions} +% +\textbf{Resumption reductions} +% +\[ +\ba{@{}l@{\quad}l@{}} +\usemlab{Res}^\ddag & +\Let\;r=\Res(V_n \dcons \dots \dcons V_1 \dcons \dnil)\;\In\;N \reducesto \\ +&\quad N[\dlam x\,\dhk. \bl\Let\;\dRecord{fs, \dRecord{q,\vhret, \vhops}}\dcons \dhk' = \dhk\;\In\\ + \kapp\;(V_1 \dcons \dots \dcons V_n \dcons \dRecord{fs, \dRecord{q,\vhret, \vhops}} \dcons \dhk')\;x/r]\el +\\ +\ea +\] +% +\textbf{Computations} +% +\begin{equations} +\cps{-} &:& \CompCat \to \UCompCat\\ +\cps{\Let~x \revto M~\In~N} &\defas& + \bl\slam \sRecord{\shf, \sRecord{\xi, \svhret, \svhops}} \scons \shk. + \ba[t]{@{}l} + \cps{M} \sapp (\sRecord{\bl\reflect((\dlam x\,\dhk.\bl\Let\;(\dk \dcons \dhk') = \dhk\;\In\\ + \cps{N} \sapp (\reflect\dk \scons \reflect \dhk')) \el\\ + \dcons \reify\shf), \sRecord{\xi, \svhret, \svhops}} \scons \shk)\el + \ea + \el\\ +\cps{\Do\;\ell\;V} &\defas& + \slam \sRecord{\shf, \sRecord{\xi, \svhret, \svhops}} \scons \shk.\, + \reify\svhops \bl\dapp \dRecord{\reify\xi, \ell, + \dRecord{\bl + \cps{V}, \dRecord{\reify \shf, \dRecord{\reify\xi,\reify\svhret, \reify\svhops}}\\ + \dcons \dnil}} + \dapp \reify \shk\el\el \\ +\end{equations} +\begin{equations} +\cps{\ParamHandle \, M \; \With \; (q.H)(W)} &\defas& +\slam \shk . \cps{M} \sapp (\sRecord{\snil, \sRecord{\reflect\cps{W},\reflect \cps{\hret}^{\ddag}_q, \reflect \cps{\hops}^{\ddag}_q}} \scons \shk) \\ +\end{equations} +\textbf{Handler definitions} +% +\begin{equations} +\cps{-} &:& \HandlerCat \times \UValCat \to \UValCat\\ +% \cps{H}^\depth &=& \sRecord{\reflect \cps{\hret}, \reflect \cps{\hops}^\depth}\\ +\cps{\{\Return \; x \mapsto N\}}^{\ddag}_q &\defas& \dlam \dRecord{q,x}\,\dhk.\Let\;(\dk \dcons \dhk') = \dhk\;\In\;\cps{N} \sapp (\reflect\dk \scons \reflect \dhk') \\ +\cps{\{(\ell \; p \; r \mapsto N_\ell)_{\ell \in \mathcal{L}}\}}^{\ddag}_q +&\defas& +\dlam \dRecord{q,z,\dRecord{p,\dhkr}}\,\dhk. + \Case \;z\; \{ + \ba[t]{@{}l@{}c@{~}l} + (&\ell &\mapsto + \ba[t]{@{}l} + \Let\;r=\Res^\ddag\,\dhkr\;\In\; \\ + \Let\;(\dk \dcons \dhk') = \dhk\;\In\\ + \cps{N_{\ell}} \sapp (\reflect\dk \scons \reflect \dhk'))_{\ell \in \mathcal{L}} + \ea\\ + &y &\mapsto \hforward((y, p, \dhkr), \dhk) \} \\ + \ea \\ +\hforward((y, p, \dhkr), \dhk) &\defas& \bl + \Let\; \dRecord{fs, \dRecord{q, \vhret, \vhops}} \dcons \dhk' = \dhk \;\In \\ + \vhops \dapp \dRecord{q, y,\dRecord{p, \dRecord{fs, \dRecord{q,\vhret, \vhops}} \dcons \dhkr}} \dapp \dhk' \\ + \el +\end{equations} + +\textbf{Top-level program} +\begin{equations} +\pcps{M} &=& \cps{M} \sapp (\sRecord{\dnil, \sRecord{\reflect\dRecord{},\reflect \dlam \dRecord{q,x}\,\dhk. x, \reflect \dlam \dRecord{q,z}\,\dhk.\Absurd~z}} \scons \snil) \\ +\end{equations} + +\caption{CPS translation for parameterised handlers.} +\label{fig:param-cps} +\end{figure} + +\paragraph{Continuation Passing Style} To accommodate parameterised +handlers, we generalise the notion of continuations once more. A +continuation becomes a triple consisting of a pure continuation, +effect continuation, and the handler parameter. This effectively +amounts to explicit state passing as the parameter value gets threaded +through every function application. The pure continuation invocation +rule $\usemlab{KAppNil}$ is slightly modified to account for the third +component. +% +\[ + \kapp \; (\dRecord{\dnil, \dRecord{\vhret, \vhops, q}} \dcons \dhk) \, V \reducesto \vhret \dapp \Record{V,q} \dapp \dhk +\] +% +The pure continuation $v$ is now applied to a pair consisting of the +return value $V$ and the current value of the handler parameter +$q$. The resumption rule $\usemlab{Res}$ is adapted to update the +value of the handler parameter. +% +\[ + \bl + \Let\;r=\Res\,(\dRecord{\vhret,\vhops,\_} \dcons \dots \dcons \dhf_1 \dcons \dnil)\;\In\;N\reducesto\\ + \qquad N[\lambda \Record{x,p}\,\dhk.\kapp\;(\dhf_1 \dcons \dots \dcons \dRecord{\vhret,\vhops,p} \dcons \dhk)\;x/r] + \el +\] +% +Thus, the parameter of the top-most handler in the resumption stack is +ignored and replaced by a new value $p$. The translation is updated +accordingly to account for the triple structure. This involves +updating all the parts that previously dynamically decomposed and +statically recomposed frames to now include the additional state +parameter. The key updated translation clauses are shown in +Figure~\ref{fig:param-cps}. +% +The translation of $\Do$ invokes the effect continuation +$\reify \svhops$ with a pair consisting of the operation and the value +of the handler parameter. The parameter is also pushed onto the +reversed resumption stack. This is necessary to account for the case +where the effect continuation $\reify \svhops$ does not handle +operation $\ell$. +% An alternative option is to push the parameter back +% on the resumption stack during effect forwarding. However that means +% the resumption stack will be nonuniform as the top element sometimes +% will be a pair. +% + +The translation of the return and operation clauses yields functions +that take a pair as input in addition to the current continuation. The +forwarding case is adjusted in much the same way as the translation +for $\Do$. The current continuation $k$ is destructed in order to +identify the next effect continuation $\vhops$ and its parameter +$q$. Then $\vhops$ is invoked with the updated resumption stack and +the value of its parameter $q$. + +The amended CPS translation for parameterised handlers is not a zero +cost translation for shallow and ordinary deep handlers as they will +have to thread a ``dummy'' parameter value through. In contrast, the +abstract machine implementation of parameterised handlers does not +impose an overhead on shallow and deep handlers. + \section{Related work} \label{sec:cps-related-work}