diff --git a/macros.tex b/macros.tex index 3697132..7d127d1 100644 --- a/macros.tex +++ b/macros.tex @@ -306,8 +306,9 @@ % Canonical variables for handler components \newcommand{\vhret}{h^{\mret}} \newcommand{\vhops}{h^{\mops}} -\newcommand{\svhret}{\chi^{\mret}} -\newcommand{\svhops}{\chi^{\mops}} +\newcommand{\sv}{\chi} +\newcommand{\svhret}{\sv^{\mret}} +\newcommand{\svhops}{\sv^{\mops}} % \newcommand{\dk}{\dRecord{fs,\dRecord{\vhret,\vhops}}} \newcommand{\dk}{k} diff --git a/thesis.tex b/thesis.tex index 396e82d..89f2878 100644 --- a/thesis.tex +++ b/thesis.tex @@ -9100,9 +9100,9 @@ matching notation. The static meta language is generated by the following productions. % \begin{syntax} - \slab{Static patterns} &\sP \in \SPatCat &::=& \sks \mid \sk \scons \sP\\ - \slab{Static values} & \sV, \sW \in \SValCat &::=& \reflect V \mid \sV \scons \sW \mid \slam \sP. \sM\\ - \slab{Static computations} & \sM \in \SCompCat &::=& \sV \mid \sV \sapp \sW \mid \sV \dapp V \dapp W + \slab{Static\text{ }patterns} &\sP \in \SPatCat &::=& \sks \mid \sk \scons \sP\\ + \slab{Static\text{ }values} & \sV, \sW \in \SValCat &::=& \reflect V \mid \sV \scons \sW \mid \slam \sP. \sM\\ + \slab{Static\text{ }computations} & \sM \in \SCompCat &::=& \sV \mid \sV \sapp \sW \mid \sV \dapp V \dapp W \end{syntax} % The patterns comprise only static list deconstructing. We let $\sP$ @@ -10027,11 +10027,11 @@ first-class objects, but rather as a special kinds of functions. \begin{equations} \cps{\Return\,V} &\defas& \slam \shk.\kapp\;(\reify \shk)\;\cps{V} \\ \cps{\Let~x \revto M~\In~N} &\defas& - \bl\slam \sRecord{\shf, \sRecord{\svhret, \svhops}} \scons \shk. + \bl\slam \sRecord{\shf, \sv} \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{\svhret, \svhops}} \scons \shk)\el + \dcons \reify\shf), \sv} \scons \shk)\el \ea \el\\ \cps{\Do\;\ell\;V} &\defas& @@ -10083,7 +10083,10 @@ The CPS translation is given in Figure~\ref{fig:cps-higher-order-uncurried-simul}. In essence, it is the same as the CPS translation for deep effect handlers as described in Section~\ref{sec:higher-order-uncurried-deep-handlers-cps}, though -it is adjusted to account for generalised continuation representation. +it is adjusted to account for generalised continuation +representation. For notational convenience, we write $\chi$ to denote +a statically known effect continuation frame +$\sRecord{\svhret,\svhops}$. % The translation of $\Return$ invokes the continuation $\shk$ using the continuation application primitive $\kapp$. @@ -10092,8 +10095,9 @@ The translations of deep and shallow handlers differ only in their use of the resumption construction primitive. A major aesthetic improvement due to the generalised continuation -representation is that continuation construction and deconstruction is -now uniform: only a single continuation frame is inspected at a time. +representation is that continuation construction and deconstruction +are now uniform: only a single continuation frame is inspected at a +time. \subsubsection{Correctness} \label{sec:cps-gen-cont-correctness} @@ -10110,7 +10114,9 @@ element is always known statically, i.e., it is of the form $\sRecord{\sV_{fs}, \sRecord{\sV_{\mret},\sV_{\mops}}} \scons \sW$. Moreover, the static values $\sV_{fs}$, $\sV_{\mret}$, and $\sV_{\mops}$ are all reflected dynamic terms (i.e., of the form -$\reflect V$). This fact is used implicitly in the proofs. +$\reflect V$). This fact is used implicitly in the proofs. For brevity +we write $\sV_f$ to denote a statically known continuation frame +$\sRecord{\sV_{fs}, \sRecord{\sV_{\mret},\sV_{\mops}}}$. % \begin{lemma}[Substitution]\label{lem:subst-gen-cont} @@ -10124,8 +10130,10 @@ $\reflect V$). This fact is used implicitly in the proofs. and with substitution in computation terms \[ \ba{@{}l@{~}l} - &(\cps{M} \sapp (\sRecord{\sV_{fs},\sRecord{\sV_{\mret},\sV_{\mops}}} \scons \sW))[\cps{V}/x]\\ - = &\cps{M[V/x]} \sapp (\sRecord{\sV_{fs},\sRecord{\sV_{\mret},\sV_{\mops}}} \scons\sW)[\cps{V}/x], + % &(\cps{M} \sapp (\sRecord{\sV_{fs},\sRecord{\sV_{\mret},\sV_{\mops}}} \scons \sW))[\cps{V}/x]\\ + % = &\cps{M[V/x]} \sapp (\sRecord{\sV_{fs},\sRecord{\sV_{\mret},\sV_{\mops}}} \scons\sW)[\cps{V}/x], + &(\cps{M} \sapp (\sV_f \scons \sW))[\cps{V}/x]\\ + = &\cps{M[V/x]} \sapp (\sV_f \scons \sW)[\cps{V}/x], \ea \] % @@ -10150,10 +10158,10 @@ the same translations as for the corresponding constructs in $\SCalc$. \cps{\Let\; x \revto \EC \;\In\; N} &=& \begin{array}[t]{@{}l} - \slam \sRecord{\shf, \sRecord{\svhret, \svhops}} \scons \shk.\\ + \slam \sRecord{\shf, \sv} \scons \shk.\\ \quad \cps{\EC} \sapp (\bl\sRecord{\reflect((\dlam x\,\dhk.\bl\Let\;\dRecord{fs,\dRecord{\vhret,\vhops}}\dcons \dhk'=\dhk\;\In\\ \cps{N} \sapp (\sRecord{\reflect fs, \sRecord{\reflect \vhret, \reflect \vhops}} \scons \reflect \dhk')) \dcons \reify\shf),\el\\ - \sRecord{\svhret,\svhops}} \scons \shk)\el + \sv} \scons \shk)\el \end{array} \\ \cps{\Handle^\depth\; \EC \;\With\; H} @@ -10169,9 +10177,12 @@ context. \begin{lemma}[Evaluation context decomposition] \label{lem:decomposition-gen-cont} \[ - \cps{\EC[M]} \sapp (\sRecord{\sV_{fs}, \sRecord{\sV_{\mret},\sV_{\mops}}} \scons \sW) + % \cps{\EC[M]} \sapp (\sRecord{\sV_{fs}, \sRecord{\sV_{\mret},\sV_{\mops}}} \scons \sW) + % = + % \cps{M} \sapp (\cps{\EC} \sapp (\sRecord{\sV_{fs}, \sRecord{\sV_{\mret},\sV_{\mops}}} \scons \sW)) + \cps{\EC[M]} \sapp (\sV_f \scons \sW) = - \cps{M} \sapp (\cps{\EC} \sapp (\sRecord{\sV_{fs}, \sRecord{\sV_{\mret},\sV_{\mops}}} \scons \sW)) + \cps{M} \sapp (\cps{\EC} \sapp (\sV_f \scons \sW)) \] \end{lemma} % @@ -10191,11 +10202,14 @@ continuation is known. % \begin{lemma}[Reflect after reify] \label{lem:reflect-after-reify-gen-cont} - +% \[ - \cps{M} \sapp (\sRecord{\sV_{fs}, \sRecord{\sV_{\mret},\sV_{\mops}}} \scons \reflect \reify \sW) + % \cps{M} \sapp (\sRecord{\sV_{fs}, \sRecord{\sV_{\mret},\sV_{\mops}}} \scons \reflect \reify \sW) + % = + % \cps{M} \sapp (\sRecord{\sV_{fs}, \sRecord{\sV_{\mret},\sV_{\mops}}} \scons \sW). + \cps{M} \sapp (\sV_f \scons \reflect \reify \sW) = - \cps{M} \sapp (\sRecord{\sV_{fs}, \sRecord{\sV_{\mret},\sV_{\mops}}} \scons \sW). + \cps{M} \sapp (\sV_f \scons \sW). \] \end{lemma} @@ -10228,27 +10242,49 @@ dynamic language, as described above. \begin{lemma}[Handling]\label{lem:handle-op-gen-cont} Suppose $\ell \notin BL(\EC)$ and $\hell = \{\ell\,p\,r \mapsto N_\ell\}$. If $H$ is deep then % + % \[ + % \bl + % \cps{\Do\;\ell\;V} \sapp (\cps{\EC} \sapp (\sRecord{\snil, \cps{H}} \scons \sRecord{\sV_{fs},\sRecord{\sV_{\mret},\sV_{\mops}}} \scons \sW)) \reducesto^+ \\ + % \quad (\cps{N_\ell} \sapp \sRecord{\sV_{fs},\sRecord{\sV_{\mret},\sV_{\mops}}} \scons \sW)\\ + % \qquad \quad [\cps{V}/p, + % \dlam x\,\dhk.\bl + % \Let\;\dRecord{fs, \dRecord{\vhret, \vhops}} \dcons \dhk' = \dhk\;\In\;\\ + % \cps{\Return\;x} \sapp (\cps{\EC} \sapp (\sRecord{\snil, \cps{H}} \scons \sRecord{\reflect \dlk, \sRecord{\reflect \vhret, \reflect \vhops}} \scons \reflect\dhk'))/r]. \\ + % \el\\ + % \el + % \] \[ \bl - \cps{\Do\;\ell\;V} \sapp (\cps{\EC} \sapp (\sRecord{\snil, \cps{H}} \scons \sRecord{\sV_{fs},\sRecord{\sV_{\mret},\sV_{\mops}}} \scons \sW)) \reducesto^+ \\ - \quad (\cps{N_\ell} \sapp \sRecord{\sV_{fs},\sRecord{\sV_{\mret},\sV_{\mops}}} \scons \sW)\\ - \qquad \quad [\cps{V}/p, + \cps{\Do\;\ell\;V} \sapp (\cps{\EC} \sapp (\sRecord{\snil, \cps{H}} \scons \sV_f \scons \sW)) \reducesto^+ \\ + \quad (\cps{N_\ell} \sapp (\sV_f \scons \sW)) + [\cps{V}/p, \dlam x\,\dhk.\bl - \Let\;\dRecord{fs, \dRecord{\vhret, \vhops}} \dcons \dhk' = \dhk\;\In\;\\ - \cps{\Return\;x} \sapp (\cps{\EC} \sapp (\sRecord{\snil, \cps{H}} \scons \sRecord{\reflect \dlk, \sRecord{\reflect \vhret, \reflect \vhops}} \scons \reflect\dhk'))/r]. \\ + \Let\;\dRecord{fs, \dRecord{\vhret, \vhops}} \dcons \dhk' = \dhk\;\In\; + \cps{\Return\;x}\\ + \sapp (\cps{\EC} \sapp (\sRecord{\snil, \cps{H}} \scons \sRecord{\reflect \dlk, \sRecord{\reflect \vhret, \reflect \vhops}} \scons \reflect\dhk'))/r]. \\ \el\\ \el \] % Otherwise if $H$ is shallow then % - \[ + % \[ + % \bl + % \cps{\Do\;\ell\;V} \sapp (\cps{\EC} \sapp (\sRecord{\snil, \cps{H}^\dagger} \scons \sRecord{\sV_{fs},\sRecord{\sV_{\mret},\sV_{\mops}}} \scons \sW)) \reducesto^+ \\ + % \quad (\cps{N_\ell} \sapp \sRecord{\sV_{fs},\sRecord{\sV_{\mret},\sV_{\mops}}} \scons \sW)\\ + % \qquad [\cps{V}/p, \dlam x\,\dhk. \bl + % \Let\;\dRecord{\dlk, \dRecord{\vhret, \vhops}} \dcons \dhk' = \dhk \;\In \\ + % \cps{\Return\;x} \sapp (\cps{\EC} \sapp (\sRecord{\reflect \dlk, \sRecord{\reflect \vhret, \reflect \vhops}} \scons \reflect\dhk'))/r]. \\ + % \el \\ + % \el + % \] + \[ \bl - \cps{\Do\;\ell\;V} \sapp (\cps{\EC} \sapp (\sRecord{\snil, \cps{H}^\dagger} \scons \sRecord{\sV_{fs},\sRecord{\sV_{\mret},\sV_{\mops}}} \scons \sW)) \reducesto^+ \\ - \quad (\cps{N_\ell} \sapp \sRecord{\sV_{fs},\sRecord{\sV_{\mret},\sV_{\mops}}} \scons \sW)\\ - \qquad [\cps{V}/p, \dlam x\,\dhk. \bl - \Let\;\dRecord{\dlk, \dRecord{\vhret, \vhops}} \dcons \dhk' = \dhk \;\In \\ - \cps{\Return\;x} \sapp (\cps{\EC} \sapp (\sRecord{\reflect \dlk, \sRecord{\reflect \vhret, \reflect \vhops}} \scons \reflect\dhk'))/r]. \\ + \cps{\Do\;\ell\;V} \sapp (\cps{\EC} \sapp (\sRecord{\snil, \cps{H}^\dagger} \scons \sV_f \scons \sW)) \reducesto^+ \\ + \quad (\cps{N_\ell} \sapp (\sV_f \scons \sW)) + [\cps{V}/p, \dlam x\,\dhk. \bl + \Let\;\dRecord{\dlk, \dRecord{\vhret, \vhops}} \dcons \dhk' = \dhk \;\In\;\cps{\Return\;x}\\ + \sapp (\cps{\EC} \sapp (\sRecord{\reflect \dlk, \sRecord{\reflect \vhret, \reflect \vhops}} \scons \reflect\dhk'))/r]. \\ \el \\ \el \] @@ -10257,8 +10293,9 @@ Suppose $\ell \notin BL(\EC)$ and $\hell = \{\ell\,p\,r \mapsto N_\ell\}$. If $H \medskip -Now the main result for the translation: a simulation result in the -style of \citet{Plotkin75}. +With the aid of the above lemmas we can state and prove the main +result for the translation: a simulation result in the style of +\citet{Plotkin75}. % \begin{theorem}[Simulation] \label{thm:ho-simulation-gen-cont} @@ -10319,15 +10356,15 @@ $M \reducesto^\ast V$ if and only if $\pcps{M} \reducesto^\ast \pcps{V}$. \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{-} &:& \CompCat \to \SValCat^\ast \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, @@ -10420,20 +10457,20 @@ $\vhops$ such that the next activation of the handler gets the parameter value $q'$ rather than $q$. The CPS translation is updated accordingly to account for the triple -effect continuation structure. This involves updating all the parts -that previously dynamically decomposed and statically recomposed -effect continuation frames to now include the additional state -parameter. The cases that need to be updated are shown in +effect continuation structure. This involves updating the cases that +scrutinise the effect continuation structure as it now includes the +additional state value. The cases that need to be updated are shown in Figure~\ref{fig:param-cps}. We write $\xi$ to denote static handler parameters. % -The translation of $\Let$ unpacks and repacks the effect continuation -to maintain the continuation length invariant. The translation of -$\Do$ invokes the effect continuation $\reify \svhops$ with a triple -consisting of the value of the handler parameter, the operation, and -the operation payload. 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$. +% The translation of $\Let$ unpacks and repacks the effect continuation +% to maintain the continuation length invariant. +The translation of $\Do$ invokes the effect continuation +$\reify \svhops$ with a triple consisting of the value of the handler +parameter, the operation, and the operation payload. 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 @@ -10454,6 +10491,10 @@ by both the pure continuation and effect continuation.% 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. +We can avoid the use of such values entirely if the target language +had proper sums to tag effect continuation frames +accordingly. Obviously, this entails performing a case analysis every +time an effect continuation frame is deconstructed. \section{Related work} \label{sec:cps-related-work}