Theorem 8.9

thesis.bib

@@ -592,16 +592,6 @@
   year      = {2017}
 }
 
-@inproceedings{Leijen05,
-  author    = {Daan Leijen},
-  title     = {Extensible records with scoped labels},
-  booktitle = {Trends in Functional Programming},
-  series    = {Trends in Functional Programming},
-  volume    = {6},
-  pages     = {179--194},
-  publisher = {Intellect},
-  year      = {2005}
-}
 
 # Helium
 @article{BiernackiPPS18,
@@ -1205,6 +1195,50 @@
   year      = {2006}
 }
 
+# Row polymorphism
+@inproceedings{Wand87,
+  author    = {Mitchell Wand},
+  title     = {Complete Type Inference for Simple Objects},
+  booktitle = {{LICS}},
+  pages     = {37--44},
+  publisher = {{IEEE} Computer Society},
+  year      = {1987}
+}
+
+@inbook{Remy94,
+  author    = {Didier R\'{e}my},
+  title     = {Type Inference for Records in Natural Extension of ML},
+  year      = 1994,
+  OPTisbn = {026207155X},
+  publisher = {MIT Press},
+  address = {Cambridge, MA, USA},
+  booktitle = {Theoretical Aspects of Object-Oriented Programming: Types, Semantics, and Language Design},
+  pages     = {67--95},
+  numpages  = {29}
+}
+
+@inproceedings{Leijen05,
+  author    = {Daan Leijen},
+  title     = {Extensible records with scoped labels},
+  booktitle = {Trends in Functional Programming},
+  series    = {Trends in Functional Programming},
+  volume    = {6},
+  pages     = {179--194},
+  publisher = {Intellect},
+  year      = {2005}
+}
+
+@article{MorrisM19,
+  author    = {J. Garrett Morris and
+               James McKinna},
+  title     = {Abstracting extensible data types: or, rows by any other name},
+  journal   = {Proc. {ACM} Program. Lang.},
+  volume    = {3},
+  number    = {{POPL}},
+  pages     = {12:1--12:28},
+  year      = {2019}
+}
+
 # fancy row typing systems that support shapes
 @inproceedings{BerthomieuS95,
   author = {Bernard Berthomieu and Camille le Moniès de Sagazan},
@@ -1221,7 +1255,6 @@
   year = {1993},
 }
 
-
 # Zipper data structure.
 @article{Huet97,
   author    = {G{\'{e}}rard P. Huet},
@@ -3497,6 +3530,26 @@
   year      = {1999}
 }
 
+@inproceedings{BentonB07,
+  author    = {Nick Benton and
+               Peter Buchlovsky},
+  title     = {Semantics of an effect analysis for exceptions},
+  booktitle = {{TLDI}},
+  pages     = {15--26},
+  publisher = {{ACM}},
+  year      = {2007}
+}
+
+@article{BentonK99,
+  author    = {Nick Benton and
+               Andrew Kennedy},
+  title     = {Monads, Effects and Transformations},
+  journal   = {Electron. Notes Theor. Comput. Sci.},
+  volume    = {26},
+  pages     = {3--20},
+  year      = {1999}
+}
+
 # Intensional type theory
 @book{MartinLof84,
   author    = {Per Martin{-}L{\"{o}}f},
@@ -3628,3 +3681,28 @@
   publisher = {Springer},
   year      = {2014}
 }
+
+# TT lifting
+@inproceedings{LindleyS05,
+  author    = {Sam Lindley and
+               Ian Stark},
+  title     = {Reducibility and TT-Lifting for Computation Types},
+  booktitle = {{TLCA}},
+  series    = {Lecture Notes in Computer Science},
+  volume    = {3461},
+  pages     = {262--277},
+  publisher = {Springer},
+  year      = {2005}
+}
+
+# Three state equations
+@inproceedings{Mellies14,
+  author    = {Paul{-}Andr{\'{e}} Melli{\`{e}}s},
+  title     = {Local States in String Diagrams},
+  booktitle = {{RTA-TLCA}},
+  series    = {{LNCS}},
+  volume    = {8560},
+  pages     = {334--348},
+  publisher = {Springer},
+  year      = {2014}
+}

thesis.tex

@@ -123,6 +123,7 @@
 \newtheorem{lemma}[theorem]{Lemma}
 \newtheorem{proposition}[theorem]{Proposition}
 \newtheorem{corollary}[theorem]{Corollary}
+\newtheorem{claim}[theorem]{Claim}
 \theoremstyle{definition}
 \newtheorem{definition}[theorem]{Definition}
 % Example environment.
@@ -682,6 +683,7 @@ operations and separate the from their handling.
 \dhil{Maybe expand this a bit more to really sell it}
 
 \section{State of effectful programming}
+\label{sec:state-of-effprog}
 
 Functional programmers tend to view programs as impenetrable black
 boxes, whose outputs are determined entirely by their
@@ -1167,7 +1169,8 @@ manipulating the state cell.
 
 The literature often presents the state monad with a fourth equation,
 which states that $\getF$ is idempotent. However, this equation is
-redundant as it is derivable from the first and third equations.
+redundant as it is derivable from the first and third
+equations~\cite{Mellies14}.
 
 We can implement a monadic variation of the $\incrEven$ function that
 uses the state monad to emulate manipulations of the state cell as
@@ -1535,6 +1538,7 @@ The free monad brings us close to the essence of programming with
 effect handlers.
 
 \subsection{Back to direct-style}
+\label{sec:back-to-directstyle}
 Monads do not freely compose, because monads must satisfy a
 distributive property in order to combine~\cite{KingW92}. Alas, not
 every monad has a distributive property.
@@ -5813,10 +5817,10 @@ contexts.
 \end{proof}
 
 %
-The calculus enjoys a rather strong \emph{progress} property, which
-states that \emph{every} closed computation term reduces to a trivial
-computation term $\Return\;V$ for some value $V$. In other words, any
-realisable function in \BCalc{} is effect-free and total.
+The calculus satisfies the standard \emph{progress} property, which
+states that \emph{every} closed computation term either reduces to a
+trivial computation term $\Return\;V$ for some value $V$, or there
+exists some $N$ such that $M \reducesto N$.
 %
 \begin{definition}[Computation normal form]\label{def:base-language-comp-normal}
   A computation $M \in \CompCat$ is said to be \emph{normal} if it is
@@ -5841,29 +5845,41 @@ which states that if some computation $M$ is well typed and reduces to
 some other computation $M'$, then $M'$ is also well typed.
 %
 \begin{theorem}[Subject reduction]\label{thm:base-language-preservation}
-  Suppose $\typ{\Gamma}{M : C}$ and $M \reducesto M'$, then
-  $\typ{\Gamma}{M' : C}$.
+  Suppose $\typ{\Delta;\Gamma}{M : C}$ and $M \reducesto N$, then
+  $\typ{\Delta;\Gamma}{N : C}$.
 \end{theorem}
 %
 \begin{proof}
   By induction on the typing derivations.
 \end{proof}
 
+Even more the calculus, as specified, is \emph{strongly normalising},
+meaning that every closed computation term reduces to a trivial
+computation term. In other words, any realisable function in $\BCalc$
+is effect-free and total.
+%
+\begin{claim}[Type soundness]
+  If $\typ{}{M : C}$, then there exists $\typ{}{N : C}$ such that
+  $M \reducesto^\ast N \not\reducesto$ and $N$ is normal.
+\end{claim}
+%
+We will not prove this theorem here as the required proof gadgetry is
+rather involved~\cite{LindleyS05}, and we will soon dispense of this
+property.
+
 \section{A primitive effect: recursion}
 \label{sec:base-language-recursion}
 %
-As evident from Theorem~\ref{thm:base-language-progress} \BCalc{}
-admit no computational effects. As a consequence every realisable
-program is terminating. Thus the calculus provide a solid and minimal
-basis for studying the expressiveness of any extension, and in
-particular, which primitive effects any such extension may sneak into
-the calculus.
+As $\BCalc$ is (claimed to be) strongly normalising it provides a
+solid and minimal basis for studying the expressiveness of any
+extension, and in particular, which primitive effects any such
+extension may sneak into the calculus.
 
 However, we cannot write many (if any) interesting programs in
 \BCalc{}. The calculus is simply not expressive enough. In order to
-bring it closer to the ML-family of languages we endow the calculus
-with a fixpoint operator which introduces recursion as a primitive
-effect. We dub the resulting calculus \BCalcRec{}.
+bring the calculus closer to the ML-family of languages we endow the
+calculus with a fixpoint operator which introduces recursion as a
+primitive effect. % We dub the resulting calculus \BCalcRec{}.
 %
 
 First we augment the syntactic category of values with a new
@@ -5908,7 +5924,7 @@ progress theorem as some programs may now diverge.
 \subsection{Tracking divergence via the effect system}
 \label{sec:tracking-div}
 %
-With the $\Rec$-operator in \BCalcRec{} we can now implement the
+With the $\Rec$-operator in place we can now implement the
 factorial function.
 %
 \[
@@ -5953,16 +5969,17 @@ In this typing rule we have chosen to inject an operation named
 $\dec{Div}$ into the effect row of the computation type on the
 recursive binder $f$. The operation is primitive, because it can never
 be directly invoked, rather, it occurs as a side-effect of applying a
-$\Rec$-definition.
+$\Rec$-definition (this is also why we ascribe it type $\ZeroType$,
+though, we may use whatever type we please).
 %
 Using this typing rule we get that
 $\dec{fac} : \Int \to \Int \eff \{\dec{Div}:\ZeroType\}$. Consequently,
 every application-site of $\dec{fac}$ must now permit the $\dec{Div}$
 operation in order to type check.
-%
-\begin{example}
-  We will use the following suspended computation to demonstrate
-  effect tracking in action.
+
+% \begin{example}
+To illustrate effect tracking in action consider the following
+suspended computation.
   %
   \[
     \bl
@@ -5972,10 +5989,11 @@ operation in order to type check.
   %
   The computation calculates $3!$ when forced.
   %
-  We will now give a typing derivation for this computation to
-  illustrate how the application of $\dec{fac}$ causes its effect row
-  to be propagated outwards. Let
-  $\Gamma = \{\dec{fac} : \Int \to \Int \eff \{\dec{Div}:\ZeroType\}\}$.
+  The typing derivation for this computation illustrates how the
+  application of $\dec{fac}$ causes its effect row to be propagated
+  outwards. Let
+  $\Gamma = \{\dec{fac} : \Int \to \Int \eff
+  \{\dec{Div}:\ZeroType\}\}$.
   %
   \begin{mathpar}
     \inferrule*[Right={\tylab{Lam}}]
@@ -5990,8 +6008,8 @@ operation in order to type check.
   %
   The information that the computation applies a possibly divergent
   function internally gets reflected externally in its effect
-  signature.
-\end{example}
+  signature.\medskip
+
 %
 A possible inconvenience of the current formulation of
 $\tylab{Rec}^\ast$ is that it recursion cannot be mixed with other
@@ -6027,15 +6045,27 @@ 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}
-\dhil{A discussion of alternative row systems}
+\section{Related work}
+
+\paragraph{Row polymorphism} Row polymorphism was originally
+introduced by \citet{Wand87} as a typing discipline for extensible
+records. The style of row polymorphism used in this chapter was
+originally developed by \citet{Remy94}.
+
+\citet{MorrisM19} have developed a unifying theory of rows, which
+collects the aforementioned row systems under one umbrella. Their
+system provides a general account of record extension and projection,
+and dually, variant injection and branching.
+
+\paragraph{Effect tracking} As mentioned in
+Section~\ref{sec:back-to-directstyle} the original effect system
+was developed by \citet{LucassenG88} to provide a lightweight facility
+for static concurrency analysis.  \citet{NielsonN99} \citet{TofteT97}
+\citet{BentonK99} \citet{BentonB07}
+%
+\citet{LindleyC12} used the effect system presented in this chapter to
+support abstraction for database programming in Links.
 
-% \section{Type and effect inference}
-% \dhil{While I would like to detail the type and effect inference, it
-%   may not be worth the effort. The reason I would like to do this goes
-%   back to 2016 when Richard Eisenberg asked me about how we do effect
-%   inference in Links.}
 
 \chapter{Effect handler oriented programming}
 \label{ch:unary-handlers}
@@ -6073,17 +6103,17 @@ interpret the effect signature of the whole program.
 % trees. Dually, \emph{shallow} handlers are defined as case-splits over
 % computation trees.
 %
-The purpose of the chapter is to augment the base calculi \BCalc{} and
-\BCalcRec{} with effect handlers, and demonstrate their practical
-versatility by way of a programming case study. The primary focus is
-on so-called \emph{deep} and \emph{shallow} variants of handlers. In
+The purpose of the chapter is to augment the base calculi \BCalc{}
+with effect handlers, and demonstrate their practical versatility by
+way of a programming case study. The primary focus is on so-called
+\emph{deep} and \emph{shallow} variants of handlers. In
 Section~\ref{sec:unary-deep-handlers} we endow \BCalc{} with deep
 handlers, which we put to use in
 Section~\ref{sec:deep-handlers-in-action} where we implement a
 \UNIX{}-style operating system. In
-Section~\ref{sec:unary-shallow-handlers} we extend \BCalcRec{} with
-shallow handlers, and subsequently we use them to extend the
-functionality of the operating system example. Finally, in
+Section~\ref{sec:unary-shallow-handlers} we extend \BCalc{} with shallow
+handlers, and subsequently we use them to extend the functionality of
+the operating system example. Finally, in
 Section~\ref{sec:unary-parameterised-handlers} we will look at
 \emph{parameterised} handlers, which are a refinement of ordinary deep
 handlers.
@@ -6122,7 +6152,7 @@ without the recursion operator and extend it with deep handlers to
 yield the calculus \HCalc{}. We elect to do so because deep handlers
 do not require the power of an explicit fixpoint operator to be a
 practical programming abstraction. Building \HCalc{} on top of
-\BCalcRec{} require no change in semantics.
+\BCalc{} with the recursion operator requires no change in semantics.
 %
 Deep handlers~\cite{PlotkinP09,Pretnar10} are defined by folds
 (specifically \emph{catamorphisms}~\cite{MeijerFP91}) over computation
@@ -9067,9 +9097,9 @@ in terms of two mutually recursive functions (specifically
 implement with deep
 handlers~\cite{KammarLO13,HillerstromL18,HillerstromLA20}.
 
-In this section we take $\BCalcRec$ as our starting point and extend
-it with shallow handlers, resulting in the calculus $\SCalc$.  The
-calculus borrows some syntax and semantics from \HCalc{}, whose
+In this section we take the full $\BCalc$ as our starting point and
+extend it with shallow handlers, resulting in the calculus $\SCalc$.
+The calculus borrows some syntax and semantics from \HCalc{}, whose
 presentation will not be duplicated in this section.
 % Often deep handlers are attractive because they are semantically
 % well-behaved and provide appropriate structure for efficient
@@ -10500,7 +10530,7 @@ labels ($\ell$).
 Computations ($M$) comprise values ($V$), applications ($M~V$), pair
 elimination ($\Let\; \Record{x, y} = V \;\In\; N$), label elimination
 ($\Case\; V \;\{\ell \mapsto M; x \mapsto N\}$), and explicit marking
-of unreachable code ($\Absurd$). A key difference from $\BCalcRec$ is
+of unreachable code ($\Absurd$). A key difference from $\BCalc$ is
 that the function position of an application is allowed to be a
 computation (i.e., the application form is $M~W$ rather than
 $V~W$). Later, when we refine the initial CPS translation we will be
@@ -14530,76 +14560,217 @@ $N'$ such that $N' \approxa \sdtrans{N}$ and $M' \reducesto^+ N'$.
 \end{theorem}
 %
 \begin{proof}
-  By case analysis on $\reducesto$ and induction on $\approxa$ using
-  Lemma~\ref{lem:sdtrans-subst} and Lemma~\ref{lem:sdtrans-admin}.
+  % By case analysis on $\reducesto$ and induction on $\approxa$ using
+  % Lemma~\ref{lem:sdtrans-subst} and Lemma~\ref{lem:sdtrans-admin}.
   %
-  \noindent\textbf{Case} $\ShallowHandle\;\EC[\Do\;\ell~V]\;\With\;H \reducesto
-  N_\ell[V/p,\lambda y.\EC[\Return\;y]/r]$ where
-  $\ell \notin \BL(\EC)$ and
-  $H^\ell = \{\OpCase{\ell}{p}{r} \mapsto N_\ell\}$. \smallskip\\
-  There are three subcases to consider.
-  \begin{enumerate}
-  \item Base step:
-    $M' = \sdtrans{\ShallowHandle\;\EC[\Do\;\ell~V]\;\With\;H}$. We
-    can compute $N'$ by direct calculation starting from $M'$ yielding
-    %
-    \begin{derivation}
+  By induction on $M' \approxa \sdtrans{M}$ and side induction on
+  $M \reducesto N$ using Lemma~\ref{lem:sdtrans-subst} and Lemma~\ref{lem:sdtrans-admin}.
+  %
+  The interesting case is reflexivity of $\approxa$ where
+  $M \reducesto N$ is an application of $\semlab{Op^\dagger}$, which
+  we will show.
+
+  In the reflexivity case we have $M' \approxa \sdtrans{M}$, where
+  $M = \ShallowHandle\;\EC[\Do\;\ell~V]\;\With\;H$ and
+  $N = N_\ell[V/p,\lambda y.\EC[\Return\;y]/r]$ such that
+  $M \reducesto N$ where $\ell \notin \BL(\EC)$ and
+  $H^\ell = \{\OpCase{\ell}{p}{r} \mapsto N_\ell\}$.
+  %
+  Hence by reflexivity of $\approxa$ we have
+  $M' = \sdtrans{\ShallowHandle\;\EC[\Do\;\ell~V]\;\With\;H}$. Now we
+  can compute $N'$ by direct calculation starting from $M'$ yielding
+  \begin{derivation}
     & \sdtrans{\ShallowHandle\;\EC[\Do\;\ell~V]\;\With\;H}\\
-    =\reducesto^+& \reason{\semlab{Op} ($\ell \notin \BL(\sdtrans{\EC})$), $2\times$\semlab{Let},\semlab{Split},\semlab{App}, Lemma~\ref{lem:sdtrans-subst}}\\
+    =& \reason{definition of $\sdtrans{-}$}\\
+    &\bl
+      \Let\;z \revto \Handle\;\sdtrans{\EC}[\Do\;\ell~\sdtrans{V}]\;\With\;\sdtrans{H}\;\In\\
+      \Let\;\Record{f;g} = z\;\In\;g\,\Unit
+     \el\\
+     \reducesto^+& \reason{\semlab{Op} using assumption $\ell \notin \BL(\sdtrans{\EC})$, \semlab{Let}, \semlab{Let}}\\
+   &\bl
+   \Let\;\Record{f;g} = \Record{
+     \bl
+     \lambda\Unit.\Let\;x \revto \Do\;\ell~\sdtrans{V}\;\In\;r~x;\\
+     \lambda\Unit.\sdtrans{N_\ell}}[\lambda x.
+             \bl
+             \Let\;z \revto (\lambda y.\Handle\;\sdtrans{\EC}[\Return\;y]\;\With\;\sdtrans{H})~x\;\In\\
+             \Let\;\Record{f;g} = z\;\In\;f\,\Unit/r,\sdtrans{V}/p]\;\In\; g\,\Unit
+             \el
+     \el\\
+     \el\\
+  \reducesto^+ &\reason{\semlab{Split}, \semlab{App}}\\
+  &\sdtrans{N_\ell}[\lambda x.
+             \bl
+             \Let\;z \revto (\lambda y.\Handle\;\sdtrans{\EC}[\Return\;y]\;\With\;\sdtrans{H})~x\;\In\\
+             \Let\;\Record{f;g} = z\;\In\;f\,\Unit/r,\sdtrans{V}/p]
+             \el\\
+  =& \reason{by Lemma~\ref{lem:sdtrans-subst}}\\
    &\sdtrans{N_\ell[\lambda x.
              \bl
              \Let\;z \revto (\lambda y.\Handle\;\EC[\Return\;y]\;\With\;H)~x\;\In\\
              \Let\;\Record{f;g} = z\;\In\;f\,\Unit/r,V/p]}
-           \el\\
+             \el
   \end{derivation}
   %
   Take the final term to be $N'$. If the resumption
   $r \notin \FV(N_\ell)$ then the two terms $N'$ and
   $\sdtrans{N_\ell[V/p,\lambda y.\EC[\Return\;y]/r]}$ are the
   identical, and thus the result follows immediate by reflexivity of
-  the $\approxa$-relation. Otherwise $N'$ approximates
-  $N_\ell[V/p,\lambda y.\EC[\Return\;y]/r]$ at least up to a use of
-  $r$. We need to show that the approximation remains faithful during
-  any application of $r$. Specifically, we proceed to show that for
-  any value $W \in \ValCat$
+  the $\approxa$-relation. Otherwise the proof reduces to showing that
+  the larger resumption term simulates the smaller resumption term,
+  i.e (note we lift the $\approxa$-relation to value terms).
   %
   \[
     (\bl
      \lambda x.\Let\;z \revto (\lambda y.\Handle\;\sdtrans{\EC}[\Return\;y]\;\With\;\sdtrans{H})~x\;\In\\
-    \Let\;\Record{f;g} = z \;\In\;f\,\Unit)~W \approxa (\lambda y.\sdtrans{\EC}[\Return\;y])~W.
+    \Let\;\Record{f;g} = z \;\In\;f\,\Unit) \approxa (\lambda y.\sdtrans{\EC}[\Return\;y]).
     \el
   \]
   %
-  The right hand side reduces to $\sdtrans{\EC}[\Return\;W]$. Two
-  applications of \semlab{App} on the left hand side yield the term
+  We use the congruence rules to apply a single $\semlab{App}$ on the
+  left hand side to obtain
   %
   \[
-    \Let\;z \revto \Handle\;\sdtrans{\EC}[\Return\;W]\;\With\;\sdtrans{H}\;\In\;\Let\;\Record{f;g} = z \;\In\;f\,\Unit.
+    (\bl
+     \lambda x.\Let\;z \revto \Handle\;\sdtrans{\EC}[\Return\;x]\;\With\;\sdtrans{H}\;\In\\
+    \Let\;\Record{f;g} = z \;\In\;f\,\Unit) \approxa (\lambda y.\sdtrans{\EC}[\Return\;y]).
+    \el
   \]
   %
-  Define
+  Now the trick is to define the following context
   %
-  $\EC' \defas \Let\;z \revto \Handle\; [\,]\;\With\;\sdtrans{H}\;\In\;\Let\;\Record{f;g} = z \;\In\;f\,\Unit$
+  \[
+    \EC' \defas \Let\;z \revto \Handle\; [\,]\;\With\;\sdtrans{H}\;\In\;\Let\;\Record{f;g} = z \;\In\;f\,\Unit.
+  \]
   %
-  such that $\EC'$ is an administrative evaluation context by
-  Lemma~\ref{lem:sdtrans-admin}. Then it follows by
+  The context $\EC'$ is an administrative evaluation context by
+  Lemma~\ref{lem:sdtrans-admin}. Now it follows by
   Defintion~\ref{def:approx-admin} that
-  $\EC'[\sdtrans{\EC}[\Return\;W]] \approxa
-  \sdtrans{\EC}[\Return\;W]$.
+  $(\lambda x.\EC'[\sdtrans{\EC}[\Return\;x]]) \approxa
+  (\lambda y.\sdtrans{\EC}[\Return\;y])$.
+  %
+  % \noindent\textbf{Case} $\ShallowHandle\;\EC[\Do\;\ell~V]\;\With\;H \reducesto
+  % N_\ell[V/p,\lambda y.\EC[\Return\;y]/r]$ where
+  % $\ell \notin \BL(\EC)$ and
+  % $H^\ell = \{\OpCase{\ell}{p}{r} \mapsto N_\ell\}$. \smallskip\\
+  % There are three subcases to consider.
+  % \begin{enumerate}
+  % \item Base step:
+  %   $M' = \sdtrans{\ShallowHandle\;\EC[\Do\;\ell~V]\;\With\;H}$. We
+  %   can compute $N'$ by direct calculation starting from $M'$ yielding
+  %   %
+  % %   \begin{derivation}
+  % %   & \sdtrans{\ShallowHandle\;\EC[\Do\;\ell~V]\;\With\;H}\\
+  % %   =\reducesto^+& \reason{\semlab{Op} ($\ell \notin \BL(\sdtrans{\EC})$), $2\times$\semlab{Let},\semlab{Split},\semlab{App}, Lemma~\ref{lem:sdtrans-subst}}\\
+  % %  &\sdtrans{N_\ell[\lambda x.
+  % %            \bl
+  % %            \Let\;z \revto (\lambda y.\Handle\;\EC[\Return\;y]\;\With\;H)~x\;\In\\
+  % %            \Let\;\Record{f;g} = z\;\In\;f\,\Unit/r,V/p]}
+  % %          \el\\
+  % %        \end{derivation}
+  %     \begin{derivation}
+  %   & \sdtrans{\ShallowHandle\;\EC[\Do\;\ell~V]\;\With\;H}\\
+  %   =& \reason{definition of $\sdtrans{-}$}\\
+  %   &\bl
+  %     \Let\;z \revto \Handle\;\sdtrans{\EC}[\Do\;\ell~\sdtrans{V}]\;\With\;\sdtrans{H}\;\In\\
+  %     \Let\;\Record{f;g} = z\;\In\;g\,\Unit
+  %    \el\\
+  %    \reducesto^+& \reason{\semlab{Op} using assumption $\ell \notin \BL(\sdtrans{\EC})$, \semlab{Let}, \semlab{Let}}\\
+  %  % &\bl
+  %  %    \Let\;z \revto
+  %  %     (\bl
+  %  %       \Let\;r \revto \lambda x.\Let\;z \revto r~x\;\In\;\Let\;\Record{f;g} = z\;\In\;f\,\Unit\;\In\\
+  %  %       \Return\;\Record{
+  %  %         \bl
+  %  %         \lambda\Unit.\Let\;x \revto \Do\;\ell~p\;\In\;r~x;\\
+  %  %         \lambda\Unit.\sdtrans{N_\ell}})[
+  %  %           \bl
+  %  %             \sdtrans{V}/p,\\
+  %  %             \lambda y.\Handle\;\sdtrans{\EC}[\Return\;y]\;\With\;\sdtrans{H}/r]
+  %  %           \el
+  %  %       \el
+  %  %       \el\\
+  %  %   \In\;\Let\;\Record{f;g} = z\;\In\;g\,\Unit
+  %  %   \el\\
+  %  % \reducesto^+& \reason{\semlab{Let}, \semlab{Let}}\\
+  %  &\bl
+  %  \Let\;\Record{f;g} = \Record{
+  %    \bl
+  %    \lambda\Unit.\Let\;x \revto \Do\;\ell~\sdtrans{V}\;\In\;r~x;\\
+  %    \lambda\Unit.\sdtrans{N_\ell}}[\lambda x.
+  %            \bl
+  %            \Let\;z \revto (\lambda y.\Handle\;\sdtrans{\EC}[\Return\;y]\;\With\;\sdtrans{H})~x\;\In\\
+  %            \Let\;\Record{f;g} = z\;\In\;f\,\Unit/r,\sdtrans{V}/p]\;\In\; g\,\Unit
+  %            \el
+  %    \el\\
+  %    \el\\
+  % \reducesto^+ &\reason{\semlab{Split}, \semlab{App}}\\
+  % &\sdtrans{N_\ell}[\lambda x.
+  %            \bl
+  %            \Let\;z \revto (\lambda y.\Handle\;\sdtrans{\EC}[\Return\;y]\;\With\;\sdtrans{H})~x\;\In\\
+  %            \Let\;\Record{f;g} = z\;\In\;f\,\Unit/r,\sdtrans{V}/p]
+  %            \el\\
+  % =& \reason{by Lemma~\ref{lem:sdtrans-subst}}\\
+  %  &\sdtrans{N_\ell[\lambda x.
+  %            \bl
+  %            \Let\;z \revto (\lambda y.\Handle\;\EC[\Return\;y]\;\With\;H)~x\;\In\\
+  %            \Let\;\Record{f;g} = z\;\In\;f\,\Unit/r,V/p]}
+  %            \el
+  % \end{derivation}
+  % %
+  % Take the final term to be $N'$. If the resumption
+  % $r \notin \FV(N_\ell)$ then the two terms $N'$ and
+  % $\sdtrans{N_\ell[V/p,\lambda y.\EC[\Return\;y]/r]}$ are the
+  % identical, and thus the result follows immediate by reflexivity of
+  % the $\approxa$-relation. Otherwise $N'$ approximates
+  % $N_\ell[V/p,\lambda y.\EC[\Return\;y]/r]$ at least up to a use of
+  % $r$. We need to show that the approximation remains faithful during
+  % any application of $r$. Specifically, we proceed to show that for
+  % any value $W \in \ValCat$
+  % %
+  % \[
+  %   (\bl
+  %    \lambda x.\Let\;z \revto (\lambda y.\Handle\;\sdtrans{\EC}[\Return\;y]\;\With\;\sdtrans{H})~x\;\In\\
+  %   \Let\;\Record{f;g} = z \;\In\;f\,\Unit)~W \approxa (\lambda y.\sdtrans{\EC}[\Return\;y])~W.
+  %   \el
+  % \]
+  % %
+  % The right hand side reduces to $\sdtrans{\EC}[\Return\;W]$. Two
+  % applications of \semlab{App} on the left hand side yield the term
+  % %
+  % \[
+  %   \Let\;z \revto \Handle\;\sdtrans{\EC}[\Return\;W]\;\With\;\sdtrans{H}\;\In\;\Let\;\Record{f;g} = z \;\In\;f\,\Unit.
+  % \]
+  % %
+  % Define
+  % %
+  % $\EC' \defas \Let\;z \revto \Handle\; [\,]\;\With\;\sdtrans{H}\;\In\;\Let\;\Record{f;g} = z \;\In\;f\,\Unit$
+  % %
+  % such that $\EC'$ is an administrative evaluation context by
+  % Lemma~\ref{lem:sdtrans-admin}. Then it follows by
+  % Defintion~\ref{def:approx-admin} that
+  % $\EC'[\sdtrans{\EC}[\Return\;W]] \approxa
+  % \sdtrans{\EC}[\Return\;W]$.
 
-  \item Inductive step: Assume $M' \reducesto M''$ and
-    $M'' \approxa \sdtrans{\ShallowHandle\;\EC[\Do\;\ell~V]\;\With\;H}$. Using a similar argument to above we get that
-    \[
-      \sdtrans{\ShallowHandle\;\EC[\Do\;\ell~V]\;\With\;H}
-      \reducesto^+ \sdtrans{N_\ell[V/p,\lambda y.\EC[\Return\;y]/r]}.
-    \]
-    Take $N' = M''$ then by the first induction hypothesis
-    $M' \reducesto N'$ and by the second induction hypothesis
-    $N' \approxa \sdtrans{N_\ell[V/p,\lambda y.\EC[\Return\;y]/r]}$ as
-    desired.
-  \item Inductive step: Assume $admin(\EC')$ and
-    $M' \approxa \sdtrans{\ShallowHandle\;\EC[\Do\;\ell~V]\;\With\;H}$.
-  \end{enumerate}
+  % \item Inductive step: Assume $M' \reducesto M''$ and
+  %   $M'' \approxa \sdtrans{\ShallowHandle\;\EC[\Do\;\ell~V]\;\With\;H}$. Using a similar argument to above we get that
+  %   \[
+  %     \sdtrans{\ShallowHandle\;\EC[\Do\;\ell~V]\;\With\;H}
+  %     \reducesto^+ \sdtrans{N_\ell[V/p,\lambda y.\EC[\Return\;y]/r]}.
+  %   \]
+  %   Take $N' = M''$ then by the first induction hypothesis
+  %   $M' \reducesto N'$ and by the second induction hypothesis
+  %   $N' \approxa \sdtrans{N_\ell[V/p,\lambda y.\EC[\Return\;y]/r]}$ as
+  %   desired.
+  % \item Inductive step: Assume $admin(\EC')$ and
+  %   $M' \approxa \sdtrans{\ShallowHandle\;\EC[\Do\;\ell~V]\;\With\;H}$.
+  %   %
+  %   By the induction the hypothesis $M' \reducesto N''$.  Take
+  %   $N' = \EC'[N'']$. The result follows by an application of the
+  %   admin rule.
+  % \item Compatibility step: We check every syntax constructor,
+  %   however, since the relation is compositional\dots
+  % \end{enumerate}
 \end{proof}
 % \begin{proof}
 %   By case analysis on $\reducesto$ using Lemma~\ref{lem:sdtrans-subst}
@@ -16844,25 +17015,25 @@ predicates. We now prove that no implementation in $\BPCF$ can match
 this: in fact, we establish a lower bound of $\Omega(n2^n)$ for the
 runtime of any counting program on \emph{any} $n$-standard predicate.
 This mathematically rigorous characterisation of the efficiency gap
-between languages with and without first-class control constructs is
-the central contribution of the paper.
+between languages with and without effect handlers is the objective of
+this chapter.
 
-One might ask at this point whether the claimed lower bound could not
-be obviated by means of some known continuation passing style (CPS) or
-monadic transform of effect handlers
-\cite{HillerstromLAS17,Leijen17}. This can indeed be done, but only by
-dint of changing the type of our predicates $P$ which would defeat the
-purpose of our enquiry.  We want to investigate the relative power of
-various languages for manipulating predicates that are given to us in
-a certain way which we do not have the luxury of choosing.
+% One might ask at this point whether the claimed lower bound could not
+% be obviated by means of some known continuation passing style (CPS) or
+% monadic transform of effect handlers
+% \cite{HillerstromLAS17,Leijen17}. This can indeed be done, but only by
+% dint of changing the type of our predicates $P$ which would defeat the
+% purpose of our enquiry.  We want to investigate the relative power of
+% various languages for manipulating predicates that are given to us in
+% a certain way which we do not have the luxury of choosing.
 
-To get a feel for the issues that our proof must address, let us
-consider how one might construct a counting program in
-$\BPCF$.  The \naive approach, of course, would be simply to apply the
-given predicate $P$ to all $2^n$ possible $n$-points in turn, keeping
-a count of those on which $P$ yields true.  It is a routine exercise to
-implement this approach in $\BPCF$, yielding (parametrically in $n$)
-a program
+To get a feel for the issues that the proof must address, let us
+consider how one might construct a counting program in $\BPCF$.  The
+\naive approach, of course, would be simply to apply the given
+predicate $P$ to all $2^n$ possible $n$-points in turn, keeping a
+count of those on which $P$ yields true.  It is a routine exercise to
+implement this approach in $\BPCF$, yielding (parametrically in $n$) a
+program
 %
 {
 \[