dhil/phd-dissertation
1
0
Fork 0
mirror of https://github.com/dhil/phd-dissertation synced 2026-03-13 11:08:25 +00:00
Code Issues Releases Wiki Activity

CPS intro

Browse Source
This commit is contained in:
Daniel Hillerström
2021-03-02 23:36:33 +00:00
parent bd3e2c8b9f
commit a29a6dc9c5
1 changed files with 58 additions and 38 deletions
Download Patch File Download Diff File Expand all files Collapse all files

96
thesis.tex
View File

@@ -4326,7 +4326,7 @@ The term `pure' is heavily overloaded in the programming literature.
% back to 2016 when Richard Eisenberg asked me about how we do effect % back to 2016 when Richard Eisenberg asked me about how we do effect
% inference in Links.} % inference in Links.}
\chapter{Programming with control via effect handlers} \chapter{Effect handler oriented programming}
\label{ch:unary-handlers} \label{ch:unary-handlers}
% %
Programming with effect handlers is a dichotomy of \emph{performing} Programming with effect handlers is a dichotomy of \emph{performing}
@@ -8289,7 +8289,7 @@ called the \emph{continuation}, which represents the next computation
in evaluation position. CPS is canonical in the sense that it is in evaluation position. CPS is canonical in the sense that it is
definable in pure $\lambda$-calculus without any further definable in pure $\lambda$-calculus without any further
primitives. As an informal illustration of CPS consider again the primitives. As an informal illustration of CPS consider again the
rudimentary factorial function from Section~\ref{sec:tracking-div}. ever-green factorial function from Section~\ref{sec:tracking-div}.
% %
\[ \[
\bl \bl
@@ -8335,52 +8335,72 @@ $\dec{fac}_{\dec{cps}}$.
Firstly note that their type signatures differ. The CPS version has an Firstly note that their type signatures differ. The CPS version has an
additional formal parameter of type $\Int \to \alpha$ which is the additional formal parameter of type $\Int \to \alpha$ which is the
continuation. By convention the continuation parameter is named $k$ in continuation. By convention the continuation parameter is named $k$ in
the implementation. The continuation captures the remainder of the implementation. As usual, the continuation represents the
computation that ultimately produces a result of type $\alpha$, or put remainder of computation. In this specific instance $k$ represents the
undelimited current continuation of an application of
$\dec{fac}_{\dec{cps}}$, i.e. the computation to occur after
evaluation of $\dec{fac}_{\dec{cps}}$. Given a value of type $\Int$,
the continuation produces a result of type $\alpha$, or put
differently: it determines what to do with the result returned by an differently: it determines what to do with the result returned by an
invocation of $\dec{fac}_{\dec{cps}}$. Semantically the continuation corresponds invocation of $\dec{fac}_{\dec{cps}}$.
to the surrounding evaluation
context.
% %
Secondly note that every $\Let$-binding in $\dec{fac}$ has become a Secondly note that every $\Let$-binding in $\dec{fac}$ has become a
function application in $\dec{fac}_{\dec{cps}}$. The functions function application in $\dec{fac}_{\dec{cps}}$. The functions
$=_{\dec{cps}}$, $-_{\dec{cps}}$, and $*_{\dec{cps}}$ denote the CPS $=_{\dec{cps}}$, $-_{\dec{cps}}$, and $*_{\dec{cps}}$ denote the CPS
versions of equality testing, subtraction, and multiplication versions of equality testing, subtraction, and multiplication
respectively. Moreover, the explicit $\Return~1$ in the true branch respectively. Moreover, the explicit $\Return~1$ in the $\Then$-branch
has been turned into an application of continuation $k$, and the has been turned into an application of the continuation $k$, and the
implicit return $n*m$ in the $\Else$-branch has been turned into an implicit return $n*m$ in the $\Else$-branch has been turned into an
explicit application of the continuation. application of $*_{\dec{cps}}$, that receives the current continuation
$k$ of $\dec{fac}_{\dec{cps}}$, which effectively delegates the
responsibility of `returning' from $\dec{fac}_{\dec{cps}}$ to
$*_{\dec{cps}}$.
% %
Thirdly note every function application occurs in tail position. This Thirdly note that every function application occurs in tail position
is a characteristic property of CPS that makes CPS feasible as a (recall Definition~\ref{def:tail-comp}). This is a characteristic
practical implementation strategy since programs in CPS notation do property of CPS transforms that make them feasible as a practical
not consume stack space. implementation strategy, since programs in CPS notation require only a
constant amount of stack space to run, namely, a single activation
frame~\cite{Appel92}.
% %
\dhil{The focus of the introduction should arguably not be to explain CPS.} %\dhil{The focus of the introduction should arguably not be to explain CPS.}
\dhil{Justify CPS as an implementation technique} %\dhil{Justify CPS as an implementation technique}
\dhil{Give a side-by-side reduction example of $\dec{fac}$ and $\dec{fac}_{\dec{cps}}$.} %\dhil{Give a side-by-side reduction example of $\dec{fac}$ and $\dec{fac}_{\dec{cps}}$.}
\dhil{Define desirable properties of a CPS translation: properly tail-recursive, no static administrative redexes} \dhil{Define desirable properties of a CPS translation: properly tail-recursive, no static administrative redexes}
% %
\begin{definition}[Properly tail-recursive~\cite{Danvy06}] % \begin{definition}[Properly tail-recursive~\cite{Danvy06}]
% % %
A CPS translation $\cps{-}$ is properly tail-recursive if the % A CPS translation $\cps{-}$ is properly tail-recursive if the
continuation of every CPS transformed tail call $\cps{V\,W}$ within % continuation of every CPS transformed tail call $\cps{V\,W}$ within
$\cps{\lambda x.M}$ is $k$, where % $\cps{\lambda x.M}$ is $k$, where
\begin{equations} % \begin{equations}
\cps{\lambda x.M} &=& \lambda x.\lambda k.\cps{M}\\ % \cps{\lambda x.M} &=& \lambda x.\lambda k.\cps{M}\\
\cps{V\,W} &=& \cps{V}\,\cps{W}\,k. % \cps{V\,W} &=& \cps{V}\,\cps{W}\,k.
\end{equations} % \end{equations}
\end{definition} % \end{definition}
\[ % \[
\ba{@{~}l@{~}l} % \ba{@{~}l@{~}l}
\pcps{(\lambda x.(\lambda y.\Return\;y)\,x)\,\Unit} &= (\lambda x.(\lambda y.\lambda k.k\,y)\,x)\,\Unit\,(\lambda x.x)\\ % \pcps{(\lambda x.(\lambda y.\Return\;y)\,x)\,\Unit} &= (\lambda x.(\lambda y.\lambda k.k\,y)\,x)\,\Unit\,(\lambda x.x)\\
&\reducesto ((\lambda y.\lambda k.k\,y)\,\Unit)\,(\lambda x.x)\\ % &\reducesto ((\lambda y.\lambda k.k\,y)\,\Unit)\,(\lambda x.x)\\
&\reducesto (\lambda k.k\,\Unit)\,(\lambda x.x)\\ % &\reducesto (\lambda k.k\,\Unit)\,(\lambda x.x)\\
&\reducesto (\lambda x.x)\,\Unit\\ % &\reducesto (\lambda x.x)\,\Unit\\
&\reducesto \Unit % &\reducesto \Unit
\ea % \ea
\] % \]
\paragraph{Relation to prior work} This chapter is based on the
following work.
%
\begin{enumerate}[i]
\item \bibentry{HillerstromLAS17}\label{en:ch-cps-HLAS17}
\item \bibentry{HillerstromL18} \label{en:ch-cps-HL18}
\item \bibentry{HillerstromLA20} \label{en:ch-cps-HLA20}
\end{enumerate}
%
Section~\ref{sec:higher-order-uncurried-deep-handlers-cps} is
based on item \ref{en:ch-cps-HLAS17}, however, I have adapted it to
follow the notation and style of item \ref{en:ch-cps-HLA20}.
\section{Initial target calculus} \section{Initial target calculus}
\label{sec:target-cps} \label{sec:target-cps}
@@ -8472,7 +8492,7 @@ term) to cope with the case of pattern matching failure.
of treating them as primitive rather than syntactic sugar (target of treating them as primitive rather than syntactic sugar (target
languages such as JavaScript has similar primitives).} languages such as JavaScript has similar primitives).}
\section{CPS transform for fine-grain call-by-value} \section{Transforming fine-grain call-by-value}
\label{sec:cps-cbv} \label{sec:cps-cbv}
We start by giving a CPS translation of $\BCalc$ in We start by giving a CPS translation of $\BCalc$ in
@@ -8528,7 +8548,7 @@ translate to value terms in the target.
\label{fig:cps-cbv} \label{fig:cps-cbv}
\end{figure} \end{figure}
\section{CPS transforming deep effect handlers} \section{Transforming deep effect handlers}
\label{sec:fo-cps} \label{sec:fo-cps}
The translation of a computation term by the basic CPS translation in The translation of a computation term by the basic CPS translation in