From 6f445247504e940597c02abf4533cd00d0e98717 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Daniel=20Hillerstr=C3=B6m?= Date: Tue, 25 May 2021 13:28:10 +0100 Subject: [PATCH] WIP --- thesis.tex | 233 ++++++++++++++++++++++++++--------------------------- 1 file changed, 113 insertions(+), 120 deletions(-) diff --git a/thesis.tex b/thesis.tex index c93df25..5547cf1 100644 --- a/thesis.tex +++ b/thesis.tex @@ -14839,7 +14839,7 @@ the captured context and continuation invocation context to coincide. % Felleisen's macro-expressiveness, Longley's type-respecting % expressiveness, Kammar's typability-preserving expressiveness. -\chapter{Asymptotic speedup with first-class control} +\chapter{Asymptotic speedup with effect handlers} \label{ch:handlers-efficiency} \def\LLL{{\mathcal L}} \def\N{{\mathbb N}} @@ -15068,12 +15068,12 @@ The rest of the paper is structured as follows. \item Section~\ref{sec:handlers-primer} provides an introduction to effect handlers as a programming abstraction. \item Section~\ref{sec:calculi} presents a PCF-like language - $\BCalc$ and its extension $\HCalc$ with effect handlers. + $\BPCF$ and its extension $\HPCF$ with effect handlers. \item Section~\ref{sec:abstract-machine-semantics} defines abstract - machines for $\BCalc$ and $\HCalc$, yielding a runtime cost model. + machines for $\BPCF$ and $\HPCF$, yielding a runtime cost model. \item Section~\ref{sec:generic-search} introduces generic count and some associated machinery, and presents an implementation in - $\HCalc$ with runtime $\BigO(2^n)$. + $\HPCF$ with runtime $\BigO(2^n)$. \item Section~\ref{sec:pure-counting} establishes that any generic count implementation in $\BCalc$ must have runtime $\Omega(n2^n)$. \item Section~\ref{sec:robustness} shows that our results scale to @@ -15081,11 +15081,11 @@ The rest of the paper is structured as follows. the adaptation from generic count to generic search, and an extension of the base language with state. \item Section~\ref{sec:experiments} evaluates implementations of - generic search based on $\BCalc$ and $\HCalc$ in Standard ML. + generic search based on $\BPCF$ and $\HPCF$ in Standard ML. \item Section \ref{sec:conclusions} concludes. \end{itemize} % -The languages $\BCalc$ and $\HCalc$ are rather minimal versions of +The languages $\BPCF$ and $\HPCF$ are rather minimal versions of previously studied systems --- we only include the machinery needed for illustrating the generic search efficiency phenomenon. % @@ -15097,11 +15097,11 @@ version of the paper~\citep{HillerstromLL20}. %% \section{Calculi} \label{sec:calculi} -In this section, we present our base language $\BCalc$ and its -extension with effect handlers $\HCalc$. +In this section, we present our base language $\BPCF$ and its +extension with effect handlers $\HPCF$. \subsection{Base Calculus} -The base calculus $\BCalc$ is a fine-grain +The base calculus $\BPCF$ is a fine-grain call-by-value~\cite{LevyPT03} variation of PCF~\cite{Plotkin77}. % Fine-grain call-by-value is similar to A-normal @@ -15109,11 +15109,10 @@ form~\cite{FlanaganSDF93} in that every intermediate computation is named, but unlike A-normal form is closed under reduction. The syntax of $\BCalc$ is as follows. -{\small -\noindent +{\noindent \begin{syntax} \slab{Types} &A,B,C,D\in\TypeCat &::= & \Nat \mid \One \mid A \to B \mid A \times B \mid A + B \\ - \slab{Type Environments} &\Gamma\in\CtxCat &::= & \cdot \mid \Gamma, x:A \\ + \slab{Type\textrm{ }Environments} &\Gamma\in\CtxCat &::= & \cdot \mid \Gamma, x:A \\ \slab{Values} &V,W\in\ValCat &::= & x \mid k \mid c \mid \lambda x^A .\, M \mid \Rec \; f^{A \to B}\, x.M \\ & &\mid& \Unit \mid \Record{V, W} \mid (\Inl\, V)^B \mid (\Inr\, W)^A\\ % & & & @@ -15168,9 +15167,7 @@ A trivial computation $(\Return\;V)$ returns value $V$. The sequencing expression $(\Let \; x \revto M \; \In \; N)$ evaluates $M$ and binds the result value to $x$ in $N$. - \begin{figure*} -\small \raggedright\textbf{Values} \begin{mathpar} % Variable @@ -15257,7 +15254,7 @@ the result value to $x$ in $N$. } {\typ{\Gamma}{\Let \; x \revto M\; \In \; N : C}} \end{mathpar} -\caption{Typing Rules for $\BCalc$} +\caption{Typing rules for $\BPCF$.} \label{fig:typing} \end{figure*} @@ -15272,7 +15269,7 @@ either a value term ($V$) or a computation term ($M$). % The constants have the following types. % -{\small +{ \begin{mathpar} \{(+), (-)\} : \Nat \times \Nat \to \Nat @@ -15280,15 +15277,14 @@ The constants have the following types. \end{mathpar}} % \begin{figure*} -\small \begin{reductions} \semlab{App} & (\lambda x^A . \, M) V &\reducesto& M[V/x] \\ -\semlab{App-Rec} & (\Rec\; f^A \,x.\, M) V &\reducesto& M[(\Rec\;f^A\,x .\,M)/f,V/x]\\ +\semlab{App\textrm{-}Rec} & (\Rec\; f^A \,x.\, M) V &\reducesto& M[(\Rec\;f^A\,x .\,M)/f,V/x]\\ \semlab{Const} & c~V &\reducesto& \Return\;(\const{c}\,(V)) \\ \semlab{Split} & \Let \; \Record{x,y} = \Record{V,W} \; \In \; N &\reducesto& N[V/x,W/y] \\ -\semlab{Case-inl} & +\semlab{Case\textrm{-}inl} & \Case \; (\Inl\, V)^B \; \{\Inl \; x \mapsto M;\Inr \; y \mapsto N\} &\reducesto& M[V/x] \\ -\semlab{Case-inr} & +\semlab{Case\textrm{-}inr} & \Case \; (\Inr\, V)^A \; \{\Inl \; x \mapsto M; \Inr \; y \mapsto N\} &\reducesto& N[V/y]\\ \semlab{Let} & \Let \; x \revto \Return \; V \; \In \; N &\reducesto& N[V/x] \\ @@ -15296,9 +15292,9 @@ The constants have the following types. \EC[M] &\reducesto& \EC[N], \hfill \text{if }M \reducesto N \\ \end{reductions} \begin{syntax} -\slab{Evaluation contexts} & \mathcal{E} &::=& [\,] \mid \Let \; x \revto \mathcal{E} \; \In \; N +\slab{Evaluation\textrm{ }contexts} & \mathcal{E} &::=& [\,] \mid \Let \; x \revto \mathcal{E} \; \In \; N \end{syntax} -\caption{Contextual Small-Step Operational Semantics} +\caption{Contextual small-step operational semantics.} \label{fig:small-step} \end{figure*} % @@ -15326,7 +15322,7 @@ call-by-value~\citep{Moggi91, FlanaganSDF93}. For example, the expression $f\,(h\,w) + g\,\Unit$ is syntactic sugar for: % -{\small +{ \[ \ba[t]{@{~}l} \Let\; x \revto h\,w \;\In\; @@ -15338,7 +15334,7 @@ for: % We define sequencing of computations in the standard way. % -{\small +{ \[ M;N \defas \Let\;x \revto M \;\In\;N, \quad \text{where $x \notin FV(N)$} \]}% @@ -15346,7 +15342,7 @@ We define sequencing of computations in the standard way. We make use of standard syntactic sugar for pattern matching. For instance, we write % -{\small +{ \[ \lambda\Unit.M \defas \lambda x^{\One}.M, \quad \text{where $x \notin FV(M)$} \]}% @@ -15354,13 +15350,13 @@ instance, we write for suspended computations, and if the binder has a type other than $\One$, we write: % -{\small +{ \[ \lambda\_^A.M \defas \lambda x^A.M, \quad \text{where $x \notin FV(M)$} \]}% % We use the standard encoding of booleans as a sum: -{\small +{ \begin{mathpar} \Bool \defas \One + \One @@ -15379,15 +15375,15 @@ We use the standard encoding of booleans as a sum: We now define $\HCalc$ as an extension of $\BCalc$. % -{\small +{ \begin{syntax} -\slab{Operation symbols} &\ell \in \mathcal{L} & & \\ +\slab{Operation\textrm{ }symbols} &\ell \in \mathcal{L} & & \\ \slab{Signatures} &\Sigma&::=& \cdot \mid \{\ell : A \to B\} \cup \Sigma\\ -\slab{Handler types} &F &::=& C \Rightarrow D\\ +\slab{Handler\textrm{ }types} &F &::=& C \Rightarrow D\\ \slab{Computations} &M, N &::=& \dots \mid \Do \; \ell \; V \mid \Handle \; M \; \With \; H \\ -\slab{Handlers} &H&::=& \{ \Val \; x \mapsto M \} - \mid \{ \ell \; p \; r \mapsto N \} \uplus H\\ +\slab{Handlers} &H&::=& \{ \Return \; x \mapsto M \} + \mid \{ \OpCase{\ell}{p}{r} \mapsto N \} \uplus H\\ \end{syntax}}% % We assume a countably infinite set $\mathcal{L}$ of operation symbols @@ -15398,7 +15394,7 @@ types, thus we assume that each operation symbol in a signature is distinct. An operation type $A \to B$ classifies operations that take an argument of type $A$ and return a result of type $B$. % -We write $dom(\Sigma) \subseteq \mathcal{L}$ for the set of operation +We write $\dom(\Sigma) \subseteq \mathcal{L}$ for the set of operation symbols in a signature $\Sigma$. % A handler type $C \Rightarrow D$ classifies effect handlers that @@ -15419,11 +15415,10 @@ with missing operation clauses (with respect to $\Sigma$) is syntactic sugar for one in which all missing clauses perform explicit forwarding: \[ - \{\ell \; p \; r \mapsto \Let\; x \revto \Do \; \ell \, p \;\In\; r \, x\} + \{\OpCase{\ell}{p}{r} \mapsto \Let\; x \revto \Do \; \ell \, p \;\In\; r \, x\}. \] \begin{figure*} -\small \raggedright \textbf{Computations} \begin{mathpar} @@ -15447,11 +15442,11 @@ forwarding: {{\Gamma} \vdash {H : C \Rightarrow D}} \end{mathpar} -\caption{Additional Typing Rules for $\HCalc$} +\caption{Additional typing rules for $\HPCF$} \label{fig:typing-handlers} \end{figure*} -The typing rules for $\HCalc$ are those of $\BCalc$ +The typing rules for $\HPCF$ are those of $\BPCF$ (Figure~\ref{fig:typing}) plus three additional rules for operations, handling, and handlers given in Figure~\ref{fig:typing-handlers}. % @@ -15473,11 +15468,11 @@ be handled by $H$. % We write $\hell$ and $\hret$ for projecting success and operation clauses. -{\small +{ \[ \ba{@{~}r@{~}c@{~}l@{~}l} - \hret &\defas& \{\Val\, x \mapsto M \}, &\quad \text{where } \{\Val\, x \mapsto M \} \in H\\ - \hell &\defas& \{\ell\, p\,r \mapsto M \}, &\quad \text{where } \{\ell\, p\;r \mapsto M \} \in H + \hret &\defas& \{\Return\, x \mapsto N \}, &\quad \text{where } \{\Return\, x \mapsto N \} \in H\\ + \hell &\defas& \{\OpCase{\ell}{p}{r} \mapsto N \}, &\quad \text{where } \{\OpCase{\ell}{p}{r} \mapsto N \} \in H \ea \]}% @@ -15485,11 +15480,11 @@ We extend the operational semantics to $\HCalc$. Specifically, we add two new reduction rules: one for handling return values and another for handling operation invocations. % -{\small +{ \begin{reductions} \semlab{Ret} & \Handle \; (\Return \; V) \; \With \; H &\reducesto& N[V/x], \qquad - \text{where } \hret = \{ \Val \; x \mapsto N \} \smallskip\\ - \semlab{Op} & \Handle \; \EC[\Do \; \ell \, V] \; \With \; H &\reducesto& N[V/p,\; (\lambda y.\Handle \; \EC[\Return \; y] \; \With \; H)/r],\\ + \text{where } \hret = \{ \Return \; x \mapsto N \} \smallskip\\ + \semlab{Op} & \Handle \; \EC[\Do \; \ell \, V] \; \With \; H &\reducesto& N[V/p,(\lambda y.\Handle \; \EC[\Return \; y] \; \With \; H)/r],\\ \multicolumn{4}{@{}r@{}}{ \hfill\text{where } \hell = \{ \ell\, p \; r \mapsto N \} } @@ -15508,15 +15503,15 @@ In order to ensure that the semantics is deterministic, we instead add a distinct form of evaluation context for effectful computation, which we call handler contexts. % -{\small +{ \begin{syntax} -\slab{Handler contexts} & \HC &::= & [\,] \mid \Handle \; \HC \; \With \; H +\slab{Handler\textrm{ }contexts} & \HC &::= & [\,] \mid \Handle \; \HC \; \With \; H \mid \Let\;x \revto \HC\; \In\; N\\ \end{syntax}}% % We replace the $\semlab{Lift}$ rule with a corresponding rule for handler contexts. -{\small +{ \[ \HC[M] ~\reducesto~ \HC[N], \qquad\hfill\text{if } M \reducesto N \]}% @@ -15544,7 +15539,7 @@ property of $\HCalc$. %% %% Abstract machine semantics %% -\subsection{The Role of Types} +\subsection{The role of types} Readers familiar with backtracking search algorithms may wonder where types come into the expressiveness picture. @@ -15566,10 +15561,10 @@ include effect types. Future work includes reconciling effect typing with our approach to expressiveness. -\section{Abstract Machine Semantics} +\section{Abstract machine semantics} \label{sec:abstract-machine-semantics} -Thus far we have introduced the base calculus $\BCalc$ and its -extension with effect handlers $\HCalc$. +Thus far we have introduced the base calculus $\BPCF$ and its +extension with effect handlers $\HPCF$. % For each calculus we have given a \emph{small-step operational semantics} which uses a substitution model for evaluation. Whilst @@ -15578,7 +15573,7 @@ realistic account of practical computation as substitution is an expensive operation. We now develop a more practical model of computation based on an \emph{abstract machine semantics}. -\subsection{Base Machine} +\subsection{Base machine} \label{sec:base-abstract-machine} \newcommand{\Conf}{\dec{Conf}} @@ -15597,7 +15592,7 @@ third component contains the continuation which instructs the machine how to proceed once evaluation of the current computation is complete. % The syntax of abstract machine states is as follows. -{\small +{ \begin{syntax} \slab{Configurations} & \conf \in \Conf &::=& \cek{M \mid \env \mid \sigma} \\ % & &\mid& \cekop{M \mid \env \mid \kappa \mid \kappa'} \\ @@ -15623,7 +15618,6 @@ pattern matching to deconstruct pure continuations. % \begin{figure*} -\small \raggedright \textbf{Transition relation} \begin{reductions} @@ -15703,7 +15697,7 @@ pattern matching to deconstruct pure continuations. \el \] -\caption{Abstract Machine Semantics for $\BCalc$} +\caption{Abstract machine semantics for $\BPCF$.} \label{fig:abstract-machine-semantics} \end{figure*} @@ -15749,19 +15743,19 @@ terms~\citep{HillerstromLA20}. \newcommand{\contapp}[2]{#1 #2} \newcommand{\contappp}[2]{#1(#2)} -\subsection{Handler Machine} +\subsection{Handler machine} \newcommand{\HClosure}{\dec{HClo}} -We now enrich the $\BCalc$ machine to a $\HCalc$ machine. +We now enrich the $\BPCF$ machine to a $\HPCF$ machine. % We extend the syntax as follows. % -{\small +{ \begin{syntax} \slab{Configurations} &\conf \in \Conf &::=& \cek{M \mid \env \mid \kappa}\\ \slab{Resumptions} &\rho \in \dec{Res} &::=& (\sigma, \chi)\\ \slab{Continuations} &\kappa \in \Cont &::=& \nil \mid \rho \cons \kappa\\ - \slab{Handler closures} &\chi \in \HClosure &::=& (\env, H) \\ - \slab{Machine values} &v, w \in \MVal &::=& \cdots \mid \rho \\ + \slab{Handler\textrm{ }closures} &\chi \in \HClosure &::=& (\env, H) \\ + \slab{Machine\textrm{ }values} &v, w \in \MVal &::=& \cdots \mid \rho \\ \end{syntax}}% % The notion of configurations changes slightly in that the continuation @@ -15777,7 +15771,7 @@ The identity continuation is a singleton list containing the identity resumption, which is an empty pure continuation paired with the identity handler closure: % -{\small +{ \[ \kappa_0 \defas [(\nil, (\emptyset, \{\Val\;x \mapsto x\}))] \]}% @@ -15810,7 +15804,6 @@ The handler machine has two possible final states: either it yields a value or it gets stuck on an unhandled operation. \begin{figure*} -\small \raggedright \textbf{Transition relation} @@ -15848,14 +15841,14 @@ value or it gets stuck on an unhandled operation. \text{ and } \hell = \{\ell\; p \; r \mapsto M\} \el\\ \end{reductions} -\caption{Abstract Machine Semantics for $\HCalc$} +\caption{Abstract machine semantics for $\HPCF$.} \label{fig:abstract-machine-semantics-handlers} \end{figure*} \paragraph{Correctness} % The handler machine faithfully simulates the operational semantics of -$\HCalc$. +$\HPCF$. % Extending the result for the base machine, we formally state and prove the correspondence in @@ -15913,11 +15906,11 @@ thus would add nothing but noise to the overall analysis. %% %% Generic search %% -\section{Predicates, Decision Trees and Generic Count} +\section{Predicates, decision trees, and generic count} \label{sec:generic-search} -We now come to the crux of the paper. In this section and the next, we -prove that $\HCalc$ supports implementations of certain operations +We now come to the crux of the chapter. In this section and the next, we +prove that $\HPCF$ supports implementations of certain operations with an asymptotic runtime bound that cannot be achieved in $\BCalc$ (Section~\ref{sec:pure-counting}). % @@ -15939,7 +15932,6 @@ $n$-queens problem~\citep{BellS09} and graph colouring can be cast as instances of generic search, and similar ideas have been explored in connection with Nash equilibria and exact real integration~\citep{Simpson98, Daniels16}. -% Taken out Nash equilibria. For simplicity, we will restrict attention to search spaces of the form $\B^n$, the set of bit vectors of length $n$. @@ -15956,9 +15948,9 @@ We will often informally write $\Nat_n$ in place of $\Nat$ to indicate that only the values $0,\dots,n-1$ are relevant, but this convention has no formal status since our setup does not support dependent types. -To summarise, in both $\BCalc$ and $\HCalc$ we will be working with the types +To summarise, in both $\BPCF$ and $\HPCF$ we will be working with the types % -{\small +{ \[ \begin{twoeqs} \Point & \defas & \Nat \to \Bool & \hspace*{2.0em} & @@ -15971,7 +15963,7 @@ To summarise, in both $\BCalc$ and $\HCalc$ we will be working with the types % and will be looking for programs % -{\small +{ \[ \Count_n : \Predicate_n \to \Nat \]}% @@ -15983,10 +15975,10 @@ Before formalising these ideas more closely, let us look at some examples, which will also illustrate the machinery of \emph{decision trees} that we will be using. -\subsection{Examples of Points, Predicates and Trees} +\subsection{Examples of points, predicates and trees} \label{sec:predicates-points} Consider first the following terms of type $\Point$: -{\small +{ \begin{mathpar} \dec{q}_0 \defas \lambda \_. \True @@ -16004,7 +15996,7 @@ and $\dec{q}_2$ represents $\langle{\True,\False}\rangle \in \B^2$. Next some predicates. First, the following terms all represent the constant true predicate $\B^2 \to \B$: -{\small +{ \begin{mathpar} \dec{T}_0 \defas \lambda q. \True @@ -16017,7 +16009,7 @@ for each $i