diff --git a/macros.tex b/macros.tex index c7f760e..c59018c 100644 --- a/macros.tex +++ b/macros.tex @@ -212,7 +212,6 @@ \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}} @@ -237,12 +236,23 @@ \newcommand{\dhf}{q} % handler frames \newcommand{\dhk}{k} % handler continuations \newcommand{\dhkr}{rk} % reverse handler continuations +\newcommand{\dLet}{\dynamic{\Let}} +\newcommand{\dIn}{\dynamic{\In}} % static \newcommand{\slf}{\phi} % let frames \newcommand{\slk}{\sigma} % let continuations \newcommand{\shf}{\theta} % handler frames \newcommand{\shk}{\kappa} % handler continuations +\newcommand{\sLet}{\static{\Let}} +\newcommand{\sIn}{\static{\In}} +\newcommand{\sk}{\kappa} +\newcommand{\sks}{\mathit{\kappa s}} +\newcommand{\sh}{\eta} +\newcommand{\sx}{\varepsilon} \newcommand{\sP}{\mathcal{P}} \newcommand{\VS}{VS} +\newcommand{\Vmap}{\keyw{vmap}} +\newcommand{\Vmapsnd}{\keyw{vmapsnd}} +\newcommand{\Fun}{\keyw{fun}} \ No newline at end of file diff --git a/thesis.tex b/thesis.tex index e6639b2..71f0595 100644 --- a/thesis.tex +++ b/thesis.tex @@ -2193,8 +2193,10 @@ have been $\eta$-reduced. The translation of operations and handlers is as follows. % \begin{equations} +\cps{-} &:& \CompCat \to \UCompCat\\ \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} \smallskip\\ +\cps{\Handle \; M \; \With \; H} &\defas& \cps{M}~\cps{\hret}~\cps{\hops} \medskip\\ +\cps{-} &:& \HandlerCat \to \UCompCat\\ \cps{\{ \Return \; x \mapsto N \}} &\defas& \lambda x . \lambda h . \cps{N} \\ \cps{\{ \ell~p~r \mapsto N_\ell \}_{\ell \in \mathcal{L}}} &\defas& @@ -2230,7 +2232,8 @@ 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) \\ +\pcps{-} &:& \CompCat \to \UCompCat\\ +\pcps{M} &\defas& \cps{M}~(\lambda x.\lambda h.x)~(\lambda \Record{z,\_}.\Absurd~z) \\ \end{equations} % Conceptually, this translation encloses the translated program in a @@ -2391,12 +2394,14 @@ translation is adjusted as follows to account for the new representation of continuations. % \begin{equations} +\cps{-} &:& \CompCat \to \UCompCat\\ \cps{\Return~V} &\defas& \lambda (k \cons ks).k\,\cps{V}\,ks \\ \cps{\Let~x \revto M~\In~N} &\defas& \lambda (k \cons ks).\cps{M}((\lambda x.\lambda ks'.\cps{N}(k \cons ks')) \cons ks) \smallskip \\ \cps{\Do\;\ell\;V} &\defas& \lambda (k \cons h \cons ks).h\,\Record{\ell,\Record{\cps{V}, \lambda x.\lambda ks'.k\,x\,(h \cons ks')}}\,ks \smallskip \\ -\cps{\Handle \; M \; \With \; H} &\defas& \lambda ks . \cps{M} (\cps{\hret} \cons \cps{\hops} \cons ks) \smallskip\\ +\cps{\Handle \; M \; \With \; H} &\defas& \lambda ks . \cps{M} (\cps{\hret} \cons \cps{\hops} \cons ks) \medskip\\ +\cps{-} &:& \HandlerCat \to \UCompCat\\ \cps{\{\Return \; x \mapsto N\}} &\defas& \lambda x.\lambda ks.\Let\; (h \cons ks') = ks \;\In\; \cps{N}\,ks' \\ \cps{\{\ell \; p \; r \mapsto N_\ell\}_{\ell \in \mathcal{L}}} @@ -2409,7 +2414,8 @@ representation of continuations. \hforward((y,p,r),ks) &\defas& \bl \Let\; (k' \cons h' \cons ks') = ks \;\In\; \\ h'\,\Record{y, \Record{p, \lambda x.\lambda ks''.\,r\,x\,(k' \cons h' \cons ks'')}}\,ks'\\ - \el \smallskip\\ + \el \medskip\\ +\pcps{-} &:& \CompCat \to \UCompCat\\ \pcps{M} &\defas& \cps{M}~((\lambda x.\lambda ks.x) \cons (\lambda \Record{z,\Record{p,r}}. \lambda ks.\,\Absurd~z) \cons \nil) \end{equations} % @@ -2479,9 +2485,10 @@ Rather than representing resumptions as functions, we move to an explicit representation of resumptions as \emph{reversed} stacks of pure and effect continuations. By choosing to reverse the order of pure and effect continuations, we can construct resumptions -efficiently using regular cons-lists. We convert these reversed stacks -to actual functions on demand using a special -$\Let\;r=\Res\,V\;\In\;N$ computation term that reduces as follows. +efficiently using regular cons-lists. We augment the syntax and +semantics of $\UCalc$ with a computation term +$\Let\;r=\Res\,V\;\In\;N$ which allow us to convert these reversed +stacks to actual functions on demand. % \begin{reductions} \usemlab{Res} @@ -2502,9 +2509,12 @@ modified to account for the change in representation of resumptions. % \begin{equations} +\cps{-} &:& \CompCat \to \UCompCat\\ \cps{\Do\;\ell\;V} &\defas& \lambda k \cons h \cons ks.\,h\, \Record{\ell,\Record{\cps{V}, h \cons k \cons \nil}}\, ks - \\ + \medskip\\ +% +\cps{-} &:& \HandlerCat \to \UCompCat\\ \cps{\{(\ell \; p \; r \mapsto N_\ell)_{\ell \in \mathcal{L}}\}} &\defas& \bl \lambda \Record{z,\Record{p,rs}}.\lambda ks.\Case \;z\; \{ @@ -2525,6 +2535,162 @@ resumption stack with the current continuation pair. % Since we have only changed the representation of resumptions, the % translation of top-level programs remains the same. +\subsection{Higher-order translation for deep effect handlers} +\label{sec:higher-order-uncurried-deep-handlers-cps} +% +\begin{figure} +% +\textbf{Static patterns and static lists} +% +\begin{syntax} +\slab{Static patterns} &\sP& ::= & \sk \scons \sP \mid \sks \\ +\slab{Static lists} &\VS& ::= & V \scons \VS \mid \reflect V \\ +\end{syntax} +% +\textbf{Reification} +% +\begin{equations} +\reify (V \scons \VS) &\defas& V \dcons \reify \VS \\ +\reify \reflect V &\defas& V \\ +\end{equations} +% +\textbf{Values} +% +\begin{displaymath} +\begin{eqs} +\cps{-} &:& \ValCat \to \UValCat\\ +\cps{x} &\defas& x \\ +\cps{\lambda x.M} &\defas& \dlam x\,ks.\cps{M} \sapp \reflect ks \\ +\cps{\Lambda \alpha.M} &\defas& \dlam z\,ks.\cps{M} \sapp \reflect ks \\ +\cps{\Record{}} &\defas& \Record{} \\ +\cps{\Record{\ell = V; W}} &\defas& \Record{\ell = \cps{V}; \cps{W}} \\ +\cps{\ell~V} &\defas& \ell~\cps{V} \\ +\end{eqs} +\end{displaymath} +% +\textbf{Computations} +% +\begin{equations} +\cps{-} &:& (\CompCat \times (\UValCat \to \UCompCat)^\ast) \to \UCompCat\\ +\cps{V\,W} &\defas& \slam \sks.\cps{V} \dapp \cps{W} \dapp \reify \sks \\ +\cps{V\,T} &\defas& \slam \sks.\cps{V} \dapp \Record{} \dapp \reify \sks \\ +\cps{\Let\; \Record{\ell=x;y} = V \; \In \; N} &\defas& \slam \sks.\Let\; \Record{\ell=x;y} = \cps{V} \; \In \; \cps{N} \sapp \sks \\ +\cps{\Case~V~\{\ell~x \mapsto M; y \mapsto N\}} &\defas& + \slam \sks.\Case~\cps{V}~\{\ell~x \mapsto \cps{M} \sapp \sks; y \mapsto \cps{N} \sapp \sks\} \\ +\cps{\Absurd~V} &\defas& \slam \sks.\Absurd~\cps{V} \\ +\cps{\Return~V} &\defas& \slam \sk \scons \sks.\sk \dapp \cps{V} \dapp \reify \sks \\ +\cps{\Let~x \revto M~\In~N} &\defas& \slam \sk \scons \sks.\cps{M} \sapp ((\dlam x\,ks.\cps{N} \sapp (\sk \scons \reflect ks)) \scons \sks) \\ +\cps{\Do\;\ell\;V} &\defas& \slam \sk \scons \sh \scons \sks.\sh \dapp + (\ell~\Record{\cps{V}, \sh \dcons \sk \dcons \dnil}) \dapp \reify \sks \\ +\cps{\Handle \; M \; \With \; H} &\defas& \slam \sks . \cps{M} \sapp (\cps{\hret} \scons \cps{\hops} \scons \sks),~\text{where} +\smallskip \\ +% +\end{equations} +% +\textbf{Handler definitions} +% +\begin{equations} +\cps{-} &:& \HandlerCat \to \UCompCat\\ +\cps{\{\Return \; x \mapsto N\}} &\defas& \dlam x\, ks.\dLet\; (h \dcons ks') = ks \;\dIn\; \cps{N} \sapp \reflect ks' +\\ +\cps{\{(\ell \; p \; r \mapsto N_\ell)_{\ell \in \mathcal{L}}\}} +&\defas& +\bl +\dlam z \, ks.\Case \;z\; \{ + \bl + (\ell~\Record{p, s} \mapsto \dLet\;r=\Fun\,s \;\dIn\; \cps{N_{\ell}} \sapp \reflect ks)_{\ell \in \mathcal{L}};\, + y \mapsto \hforward \} \\ + \el \\ +\el \\ +\hforward &\defas& \bl + \dLet\; (k' \dcons h' \dcons ks') = ks \;\dIn\; \\ + \Vmap\,(\dlam\Record{p, s}\,(k \dcons ks).k\,\Record{p, h' \dcons k' \dcons s}\,ks)\,y\,(h' \dcons ks') \\ + \el +\end{equations} + +\textbf{Top level program} +% +\begin{equations} +\pcps{M} &=& \cps{M} \sapp ((\dlam x\,ks.x) \scons (\dlam z\,ks.\Absurd~z) \scons \snil) \\ +\end{equations} +\vspace{-1em} + +\caption{Higher-order uncurried CPS translation of $\HCalc$} +\label{fig:cps-higher-order-uncurried} +\end{figure} +% +We now adapt our uncurried CPS translation to a higher-order one-pass +CPS translation~\cite{DanvyF90} that partially evaluates +administrative redexes at translation time. +% +Following Danvy and Nielsen~\cite{DanvyN03}, we adopt a two-level +lambda calculus notation to distinguish between \emph{static} lambda +abstraction and application in the meta language and \emph{dynamic} +lambda abstraction and application in the target language. +% +The idea is that redexes marked as static are reduced as part of the +translation (at compile time), whereas those marked as dynamic are +reduced at runtime. +% +The CPS translation is given in +Figure~\ref{fig:cps-higher-order-uncurried}. + +An overline denotes a static syntax constructor and an underline +denotes a dynamic syntax constructor. In order to facilitate this +notation we write application explicitly as an infix ``at'' symbol +($@$). We assume the meta language is pure and hence respects the +usual $\beta$ and $\eta$ equivalences. We extend the overline and +underline notation to distinguish between static and dynamic let +bindings. + +The reify operator $\reify$ maps static lists to dynamic ones and the +reflect constructor $\reflect$ allows dynamic lists to be treated as +static. +% +We use list pattern matching in the meta language. +% +\begin{equations} +(\slam (\sk \scons \sP).\sM) \sapp (V \scons \VS) + &=& \sLet\; \sk = V \;\sIn\; (\slam \sP.\sM) \sapp \VS \\ +(\slam (\sk \scons \sP).\sM) \sapp \reflect V + &=& \dLet\; (k \dcons ks) = V \;\dIn\; + \sLet\; \sk = k \;\sIn\; (\slam \sP.\sM) \sapp \reflect ks \\ +\end{equations} +Here we let $\sM$ range over meta language expressions. + +Now the target calculus is refined so that all lambda abstractions and +applications take two arguments, the $\usemlab{Lift}$ rule is removed, +and the $\usemlab{App}$ rule is replaced by the following reduction +rule. +% +\begin{reductions} +\usemlab{AppTwo} & (\dlam x\,ks . \, M) \dapp V \dapp W &\reducesto& M[V/x, W/ks] \\ +\end{reductions} +% +We add an extra dummy argument to the translation of type lambda +abstractions and applications in order to ensure that all dynamic +functions take exactly two arguments. +% +The single argument lambdas and applications from the first-order +uncurried translation are still present, but now they are all static. + +In order to reason about the behaviour of the \semlab{Handle-op} rule, +which is defined in terms of an evaluation context, we extend the CPS +translation to evaluation contexts. +% +\begin{displaymath} +\ba{@{}r@{~}c@{~}r@{~}l@{}} +\cps{[~]} &=& \slam \sks. &\sks \\ +\cps{\Let\; x \revto \EC \;\In\; N} &=& \slam \sk \scons \sks.&\cps{\EC} \sapp ((\dlam x\,ks.\cps{N} \sapp (k \scons \reflect ks)) \scons \sks) \\ +\cps{\Handle\; \EC \;\With\; H} &=& \slam \sks. &\cps{\EC} \sapp (\cps{\hret} \scons \cps{\hops} \scons \sks) \\ +\ea +\end{displaymath} +The following lemma is the characteristic property of the CPS +translation on evaluation contexts. +% +This allows us to focus on the computation contained within +an evaluation context. + \chapter{Abstract machine semantics} \part{Expressiveness}