Performing effectful operations.

macros.tex

@@ -4,7 +4,9 @@
 \newcommand{\Links}{Links\xspace}
 \newcommand{\CoreLinks}{\ensuremath{\mathsf{CoreLinks}}\xspace}
 \newcommand{\BCalc}{\ensuremath{\lambda_{\mathsf{b}}}\xspace}
-\newcommand{\BCalcRec}{\ensuremath{\lambda_{\mathsf{b}}^{\mathsf{rec}}}\xspace}
+\newcommand{\BCalcRec}{\ensuremath{\lambda_{\mathsf{b}+\mathsf{rec}}}\xspace}
+\newcommand{\HCalc}{\ensuremath{\lambda_{\mathsf{h}}}\xspace}
+\newcommand{\EffCalc}{\ensuremath{\lambda_{\mathsf{eff}}}\xspace}
 
 %%
 %% Calculi terms and types type-setting.

thesis.bib

@@ -768,4 +768,15 @@
   booktitle = {Annals of Mathematics},
   pages     = {346--366},
   volume    = {33}
+}
+
+# Termination analysis.
+@article{Walther94,
+  author    = {Christoph Walther},
+  title     = {On Proving the Termination of Algorithms by Machine},
+  journal   = {Artif. Intell.},
+  volume    = {71},
+  number    = {1},
+  pages     = {101--157},
+  year      = {1994}
 }

thesis.tex

@@ -63,6 +63,10 @@
 \newtheorem{proposition}[theorem]{Proposition}
 \newtheorem{corollary}[theorem]{Corollary}
 \newtheorem{definition}[theorem]{Definition}
+% Example environment.
+\makeatletter
+\def\@endtheorem{\hfill$\blacksquare$\endtrivlist\@endpefalse} % inserts a black square at the end.
+\makeatother
 \theoremstyle{definition}
 \newtheorem{example}{Example}[chapter]
 
@@ -1192,7 +1196,11 @@ customary factorial function.
        \ba[t]{@{}l}
          \Let\;is\_zero \revto n = 0\;\In\\
          \If\;is\_zero\;\Then\; \Return\;1\\
-         \Else\;\Let\; n' \revto n - 1 \;\In\;f~n'
+         \Else\;\ba[t]{@{~}l}
+                   \Let\; n' \revto n - 1 \;\In\\
+                   \Let\; m \revto f~n' \;\In\\
+                   n * m
+                 \ea
        \ea
   \el
 \]
@@ -1205,16 +1213,16 @@ effect signature does not alert us about the potential divergence. In
 fact, in this particular instance the effect row on the computation
 type is empty, which might deceive the doctrinaire to think that this
 function is `pure'. Whether this function is pure or impure depend on
-the precise notion of purity -- which we have yet to choose. We shall
+the precise notion of purity -- which we have yet to choose. In
-soon make clear the notion of purity that we have mind, however,
+Section~\ref{sec:notions-of-purity} we shall make clear the notion of
-before doing so let us briefly illustrate how we might utilise the
+purity that we have mind, however, first let us briefly illustrate how
-effect system to track divergence.
+we might utilise the effect system to track divergence.
 
 The key to track divergence is to modify the \tylab{Rec} to inject
 some primitive operation into the effect row.
 %
 \begin{mathpar}
-  \inferrule*[Lab=\tylab{Rec}]
+  \inferrule*[Lab=$\tylab{Rec}^\ast$]
     {\typ{\Delta;\Gamma,f : A \to B\eff\{\dec{Div}:\Zero\}, x : A}{M : B\eff\{\dec{Div}:\Zero\}}}
     {\typ{\Delta;\Gamma}{(\Rec \; f^{A \to B\eff\{\dec{Div}:\Zero\}} \, x .M) : A \to B\eff\{\dec{Div}:\Zero\}}}
 \end{mathpar}
@@ -1231,22 +1239,21 @@ every application-site of $\dec{fac}$ must now permit the $\dec{Div}$
 operation in order to type check.
 %
 \begin{example}
-  Consider the following ill-typed suspended computation which is
+  We will use the following suspended computation to demonstrate
-  intended to compute the $3!$ when forced.
+  effect tracking in action.
   %
   \[
     \bl
-      \dec{fac_3} : \Unit \to \Int \eff \emptyset\\
+      \lambda\Unit. \dec{fac}~3
-      \dec{fac_3} \defas \lambda\Unit. \dec{fac}~3
     \el
   \]
   %
-  We will now show that this suspended computation fails to type check
+  The computation calculates $3!$ when forced.
-  with the above type signature. Let
+  %
-  $\Gamma = \{\dec{fac} : \Int \to \Int \eff
+  We will now give a typing derivation for this computation to
-  \{\dec{Div}:\Zero\}\}$. The following typing derivation shows that
+  illustrate how the application of $\dec{fac}$ causes its effect row
-  the application of $\dec{fac}$ causes its effect row to be
+  to be propagated outwards. Let
-  propagated outwards.
+  $\Gamma = \{\dec{fac} : \Int \to \Int \eff \{\dec{Div}:\Zero\}\}$.
   %
   \begin{mathpar}
     \inferrule*[Right={\tylab{Lam}}]
@@ -1254,17 +1261,49 @@ operation in order to type check.
         {\typ{\emptyset;\Gamma,\Unit:\Record{}}{\dec{fac} : \Int \to \Int \eff \{\dec{Div}:\Zero\}}\\
          \typ{\emptyset;\Gamma,\Unit:\Record{}}{3 : \Int}
         }
-        {\typ{\emptyset;\Gamma,\Unit:\Record{}}{\dec{fac}~3 : \Int \eff \{\dec{Div}:\Zero\}}}
+        {\typc{\emptyset;\Gamma,\Unit:\Record{}}{\dec{fac}~3 : \Int}{\{\dec{Div}:\Zero\}}}
       }
       {\typ{\emptyset;\Gamma}{\lambda\Unit.\dec{fac}~3} : \Unit \to \Int \eff \{\dec{Div}:\Zero\}}
   \end{mathpar}
   %
-  It follows from the typing derivation that the effect row on
+  The information that the computation applies a possibly divergent
-  $\dec{fac_3}$ cannot be empty. In other words, the information that
+  function internally gets reflected externally in its effect
-  $\dec{fac_3}$ applies a possibly divergent function internally must
+  signature.
-  be reflected externally in its effect signature.
 \end{example}
+%
+A possible inconvenience of the current formulation of
+$\tylab{Rec}^\ast$ is that it recursion cannot be mixed with other
+computational effects. The reason being that the effect row on
+$A \to B\eff \{\dec{Div}:\Zero\}$ is closed. Thus in a practical
+general-purpose programming language implementation it is likely be
+more convenient to leave the tail of the effect row open as to allow
+recursion to be used in larger effect contexts. The rule formulation
+is also rather coarse as it renders every $\Rec$-definition as
+possibly divergent -- even definitions that are obviously
+non-divergent such as the $\Rec$-variation of the identity function:
+$\Rec\;f\,x.x$. A practical implementation could utilise a static
+termination checker~\cite{Walther94} to obtain more fine-grained
+tracking of divergence.
+% By fairly lightweight means we can obtain a finer analysis of
+% $\Rec$-definitions by simply having an additional typing rule for
+% the application of $\Rec$.
+% %
+% \begin{mathpar}
+%   \inferrule*[lab=$\tylab{AppRec}^\ast$]
+%   { E' = \{\dec{Div}:\Zero\} \uplus E\\
+%     \typ{\Delta}{E'}\\\\
+%     \typ{\Delta;\Gamma}{\Rec\;f^{A \to B \eff E}\,x.M : A \to B \eff E}\\
+%     \typ{\Delta;\Gamma}{W : A}
+%   }
+%   {\typ{\Delta;\Gamma}{(\Rec\;f^{A \to B \eff E}\,x.M)\,W : B \eff E'}}
+% \end{mathpar}
+% %
 
+\subsection{Notions of purity}
+\label{sec:notions-of-purity}
+The term `pure' is heavily overloaded in the programming literature.
+%
+\dhil{In this thesis we use the Haskell notion of purity.}
 
 \section{Row polymorphism}
 \label{sec:row-polymorphism}
@@ -1278,11 +1317,340 @@ operation in order to type check.
 
 \chapter{Unary handlers}
 \label{ch:unary-handlers}
+%
+In this chapter we study various flavours of unary effect
+handlers. First we endow \BCalc{} with a syntax for performing
+effectful operations, yielding the calculus \EffCalc{}. On its own the
+calculus is not very interesting, however, as the sole addition of the
+ability to perform effectful operations does not provide any practical
+note-worthy expressiveness. However, as we augment the calculus with
+different forms of effect handlers, we begin be able to implement
+interesting that are either difficult or impossible to realise in
+\BCalc{} in direct-style. Concretely, we shall study four variations
+of effect handlers, each as a separate extension to \EffCalc{}: deep,
+default, parameterised, and shallow handlers.
+
+\section{Performing effectful operations}
+\label{sec:eff-calculus-perform}
+
+An effectful operation is a purely syntactic construction, which has
+no predefined dynamic semantics. The introduction form for effectful
+operations is a computation term.
+%
+\begin{syntax}
+  &M,N \in \CompCat &::=& \cdots \mid~ \tikzmarkin{do1} (\Do \; \ell~V)^E \tikzmarkend{do1}
+\end{syntax}
+%
+Informally, the intended behaviour of the new computation term
+$(\Do\; \ell~V)^E$ is that it performs some operation $\ell$ with
+value argument $V$. Thus the $\Do$-construct is similar to the typical
+exception-signalling $\keyw{throw}$ or $\keyw{raise}$ constructs found
+in programming languages with support for exceptions. The term is
+annotated with an effect row $E$, providing a handle to obtain the
+current effect context. We make use of this effect row during typing:
+%
+\begin{mathpar}
+  \inferrule*[Lab=\tylab{Do}]
+    { E = \{\ell : A \to B; R\} \\
+      \typ{\Delta}{E} \\
+      \typ{\Delta;\Gamma}{V : A}
+    }
+    {\typc{\Delta;\Gamma}{(\Do \; \ell \; V)^E : B}{E}}
+\end{mathpar}
+%
+An operation invocation is only well-typed if the effect row $E$ is
+well-kinded and contains the said operation with a present type; in
+other words, the current effect context permits the operation. The
+argument type $A$ must be the same as the domain of the operation.
+%
+We slightly abuse notation by using the function space arrow, $\to$,
+to also denote the operation space. Although, the function and
+operation spaces are separate entities, we may think of the operation
+space as a subspace of the function space in which every effect row is
+empty, i.e. every operation has a type on the form
+$A \to B \eff \emptyset$. As we shall see in
+Section~\ref{sec:unary-deep-handlers}, the reason that the effect row
+is always empty is that any effects an operation might have are
+ultimately conferred by a handler.
+
+% to be effect row the
+% operation $\ell$ appears in the effect signature $\Sigma$, and the
+% argument type $A$ matches the type of the provided argument $V$. The
+% result type $B$ determines the type of the invocation. In richer type
+% systems with effect tracking such as that of \citet{HillerstromL16} or
+% \citet{Leijen17} signatures are an integral part of the type
+% structure.
+
 
 \section{Deep handlers}
-\subsection{Syntax and static semantics}
+\label{sec:unary-deep-handlers}
-\subsection{Effect inference}
+We now endow $\BCalc$ with effects and yielding the calculus $\HCalc$.
-\subsection{Dynamic semantics}
+Specifically, we add two new computation term forms that introduce and
+eliminate effects.
+%
+The syntax of value terms will be unchanged.
+%
+First we define notation for handler types.
+%
+\begin{syntax}
+\slab{Handler types}     &F     &::=& C \Rightarrow D\\
+\end{syntax}
+%
+We assume the existence of a countably infinite set of operation
+symbols $\mathcal{L}$.
+%
+An effect signature $\Sigma$ is a map from operation symbols to their
+types, thus we assume that each operation symbol in a signature is
+distinct. An operation type $A \to B$ denotes an operation that takes
+an argument of type $A$ and returns a result of type $B$.
+%
+We write $dom(\Sigma) \subseteq \mathcal{L}$ for the set of operation
+symbols in a signature $\Sigma$.
+%
+%
+%% SL: probably overly fussy
+%%
+%%  satisfies the criterion that its
+%% domain consists of distinct operation symbols; we define this
+%% criterion inductively on the structure of a signature as follows.
+%% %
+%% \begin{mathpar}
+%%   \inferrule*[Lab=\siglab{empty}]
+%%     { }
+%%     {\vdash {\cdot~\mathsf{sig}}}
+%%
+%%   \inferrule*[Lab=\siglab{member}]
+%%     {\vdash \Sigma~\mathsf{sig}\\
+%%      \ell \not\in dom(\Sigma)}
+%%     {\vdash \{\ell : A \to B \} \cup \Sigma~\mathsf{sig}}
+%% \end{mathpar}
+%% %
+%
+An effect handler type $C \Rightarrow D$ classifies effect handlers
+that transform computations of type $C$ into computations of type $D$.
+%
+Following \citet{Pretnar15}, we shall assume a global signature for
+every program.
+%
+%% \jrl{The following is a bit unclear at this point.}
+%% In our setup, the sole purpose of signatures is to be informative, as
+%% we shall see shortly, signatures provide the necessary information to
+%% type operation invocations and effect handlers.
+%% %
+%% Following \citet{Pretnar15}, we will make one simplifying assumption
+%% regarding signatures, namely, we shall assume a global signature for
+%% every program that encompasses all the used operations. Note that such
+%% a signature can easily be built by recursively inspecting the syntax
+%% of the program in question.
+%% %
+%
+We now have the basic machinery to present the two new computation
+forms.
+
+\subsection{Handling of effectful operations}
+%% \jrl{Worth mentioning that values are the same as in $\BCalc$}
+%% \sam{We now mention that above}
+We now present the elimination form for effectful operations.
+%
+\begin{syntax}
+\slab{Computations} &M,N \in \CompCat &::=& \cdots \mid~ \tikzmarkin{deephandlers1} \Handle \; M \; \With \; H\tikzmarkend{deephandlers1}\\[1ex]
+\slab{Handlers}     &H                &::=& \{ \Val \; x \mapsto M \}\\
+                    &                 &\mid&  \{ \ell \; p \; r \mapsto N \} \uplus H\\
+\end{syntax}
+%
+%% \jrl{Maybe easier to understand once typing have been given?}
+%
+%% SL: Possibly, but let's stick with this structure for now.
+%
+The handle construct $(\Handle \; M \; \With \; H)$ is the counterpart
+to $\Do$. It runs computation $M$ using handler $H$. A handler $H$
+consists of a value clause $\{\Val \; x \mapsto M\}$ and a possibly
+empty set of operation clauses $\{\ell \; p \; r \mapsto
+N_\ell\}_{\ell \in \mathcal{L}}$.
+%
+The value clause $\{\Val \; x \mapsto M\}$ defines how to interpret a
+final return value of the handled computation. The variable $x$ is
+bound to the final return value in the body $M$.
+%
+Each operation clause $\{\ell \; p \; r \mapsto N_\ell\}_{\ell \in
+  \mathcal{L}}$ defines how to interpret an invocation of a particular
+operation $\ell$. The variables $p$ and $r$ are bound in the body
+$N_\ell$: $p$ binds the argument carried by the operation and
+resumption $r$ binds the resumption of the invocation site of $\ell$.
+
+An appealing feature of effect handlers is \emph{operation
+  forwarding}, which intuitively means that if some handler $H$ has no
+matching operation clause for some operation $\ell$, then $H$ silently
+forwards $\ell$ to its nearest enclosing handler.
+%
+In programming practice, forwarding is crucial for modularity as it
+provides a basis for composing a collection of fine-grained,
+specialised effect handlers to interpret a larger effect
+signature~\citep{KammarLO13,HillerstromL16}.
+%
+The handlers in our calculus do not support forwarding directly;
+rather, we follow \citet{PlotkinP13} and adopt the convention that a
+handler with omitted operation clauses (with respect to global
+signature $\Sigma$) is syntactic sugar for one in which all missing
+clauses perform forwarding explicitly:
+%
+\[
+   \{\ell \; p \; r \mapsto \Let\; x \revto \Do \; \ell \, p \;\In\; r \, x\}
+\]
+%
+By omitting forwarding, we obtain a slightly simpler metatheory
+without altering the expressive power of the
+system.
+% SL: I don't think this is a relevant citation
+%
+%~\citep{ForsterKLP17}.
+%
+(Of course, if we were to add a type-and-effect system then this
+approach would lose important information.)
+
+%% It is worth noting that this approach only works because our type
+%% system is oblivious to effects. With a type-and-effect system this
+%% convention would change the effect types of every handler.
+
+Given a handler $H$, we often wish to refer to the clause for a
+particular operation or the value clause; for these purposes we define
+two convenient projections on handlers in the metalanguage.
+\[
+  \ba{@{~}r@{~}c@{~}l@{~}l}
+    \hell &\defas& \{\ell\; p\,r \mapsto M \}, &\quad \text{where } \{\ell\; p\,r \mapsto M \} \in H\\
+    \hret &\defas& \{\Val\, x \mapsto M \}, &\quad \text{where } \{\Val\, x \mapsto M \} \in H\\
+  \ea
+\]
+%
+The $\hell$ projection yields the singleton set consisting of the
+operation clause in $H$ that handles the operation $\ell$, whilst
+$\hret$ yields the singleton set containing the value clause of $H$.
+
+\subsubsection{Static semantics}
+
+The typing of effect handlers is slightly more involved than the
+typing of the $\Do$-construct.
+%
+\begin{mathpar}
+  \inferrule*[Lab=\tylab{Handle}]
+    {\typ{\Gamma}{M : C} \\
+     \Gamma \vdash H : C \Rightarrow D}
+    {\typ{\Gamma}{\Handle \; M \; \With \; H : D}}
+
+%\mprset{flushleft}
+\inferrule*[Lab=\tylab{Handler}]
+    {  \hret = \{\Val \; x \mapsto M\} \\
+      [\hell = \{\ell \; p_\ell \; r_\ell \mapsto N_\ell\}]_{\ell \in dom(\Sigma)} \\
+      [\typ{\Gamma, p_\ell : A_\ell, r_\ell : B_\ell \to D}{N_\ell : D}]_{(\ell : A_\ell \to B_\ell) \in \Sigma} \\
+       \typ{\Gamma, x : C}{M : D} \\
+    }
+    {{\Gamma} \vdash {H : C \Rightarrow D}}
+\end{mathpar}
+%
+The $\tylab{Handle}$ rule is straightforward.
+%
+Most of the work happens in the \tylab{Handler} rule.
+%
+It ensures that the bodies of the value clause and the operation
+clauses all have the output type $D$. The type of $x$ in the value
+clause must match the input type $C$. The type of the parameter
+$p_\ell$ ($A_\ell$) and resumption $r_\ell$ ($B_\ell \to D$) in the
+operation clause $\hell$ is determined by the signature for
+$\ell$. The return type of $r_\ell$ is $D$, as the body of the
+resumption will itself be handled by $H$.
+%
+
+% \paragraph{Deep Versus Shallow}
+
+% An alternative would be to set the return type of $r_\ell$ to be
+% $C$. Then the programmer would have to explicitly reinvoke the effect
+% handler as desired. Our current rule gives rise to \emph{deep
+%   handlers} whereas the alternative rule gives rise to \emph{shallow
+%   handlers}~\citep{KammarLO13, HillerstromL18}.
+
+%% The body of the value clause must be of type $D$ provided that the
+%% binder $x$ has type $C$ -- the return type of the computation $M$. The
+%% operation clause bodies, $N_\ell$, must also have the same type
+%% $D$. Furthermore, the bodies are typed with respect to operation
+%% argument and the resumption, whose types are constructed using the
+%% signature $\Sigma$. Each invocation of $r_\ell$ in $N_\ell$ must
+%% provide an argument of the expected return type $B_\ell$ of $\ell$,
+%% whilst $r_\ell$ itself must return a value of the same type $D$ as the
+%% handler.
+
+%% Readers familiar with the effect handlers' literature will recognise
+%% these rules as the typing rules for so-called \emph{deep
+%%   handlers}~\citep{BauerP15} as opposed to \emph{shallow
+%%   handlers}~\citep{HillerstromL18}. We shall not delve into their technical
+%% distinction in this paper.
+
+
+
+\subsubsection{Dynamic semantics}
+
+We add two new reduction rules to the operational semantics: one for
+handling return values and the other for handling operations.
+%{\small{
+\begin{reductions}
+\semlab{Ret} &
+  \Handle \; (\Return \; V) \; \With \; H &\reducesto& N[V/x],  \hfill\text{where } \hret = \{ \Val \; x \mapsto N \} \\
+\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 \}
+}
+\end{reductions}%}}%
+%
+The rule \semlab{Ret} invokes the return clause of a handler.
+%
+The rule \semlab{Op} handles an operation via the corresponding
+operation clause.
+%
+Rather than augmenting the notion of evaluation contexts from the base
+language, we introduce a new context for handlers.
+% \begin{syntax}
+% \slab{Handler contexts} &  \HC &::=& [\,] \mid \Handle \; \HC \; \With \; H \mid \Let\;x \revto \HC\; \In\; N
+% \end{syntax}
+% \begin{reductions}
+%   \semlab{Lift-H} & \HC[M] &\reducesto& \HC[N], \qquad\hfill\text{if } M \reducesto N
+% \end{reductions}
+%
+The separation between pure evaluation contexts $\EC$ and handler
+contexts $??$ guarantees the reduction rules remain deterministic, as
+otherwise $(\semlab{Op})$ can pick an arbitrary handler in scope. But
+with this separation, the rule must pick the innermost handler.
+% SL: deleted unique decomposition lemma as it wasn't formulated
+% correctly and not mentioned directly
+%
+%% The unique decomposition lemma remains true for the extended
+%% evaluation contexts, although, there are more cases to consider in the
+%% proof.
+
+The metatheoretic properties of $\BCalc$ transfer to $\HCalc$ with
+little extra effort, alas we have to amend the definition of
+computation normal forms as there are now two ways in which a
+computation term can terminate: successfully returning a value or
+getting stuck on an unhandled operation.
+%
+\begin{definition}[Computation normal forms]
+  We say that a computation term $N$ is normal with respect to
+  $\ell \in \Sigma$, if $N$ is either of the form $\Return\;V$, or
+  $\EC[\Do\;\ell\,W]$.
+\end{definition}
+%
+
+%
+\begin{theorem}[Subject Reduction]
+If $\typ{\Gamma}{M : C}$ and $M \reducesto M'$, then
+$\typ{\Gamma}{M' : C}$.
+\end{theorem}
+%
+
+\begin{theorem}[Type Soundness]
+  If $\typ{}{M : C}$, then either there exists $\typ{}{N : C}$ such
+  that $M \reducesto^+ N$ and $N$ is normal, or $M$ diverges.
+\end{theorem}
 
 \section{Default handlers}