WIP

macros.tex

@@ -382,6 +382,20 @@
 % configurations
 \newcommand{\conf}{\mathcal{C}}
 
+% effect sugar
+\newcommand{\xcomp}[1]{\sembr{#1}}
+\newcommand{\xval}[1]{\sembr{#1}}
+\newcommand{\xpre}[1]{\sembr{#1}}
+\newcommand{\xrow}[1]{\sembr{#1}}
+\newcommand{\xeff}[1]{\sembr{#1}}
+\newcommand{\pcomp}[1]{\sembr{#1}}
+\newcommand{\pval}[1]{\sembr{#1}}
+\newcommand{\ppre}[1]{\sembr{#1}}
+\newcommand{\prow}[1]{\sembr{#1}}
+\newcommand{\peff}[1]{\sembr{#1}}
+\newcommand{\eamb}{\ensuremath{E_{\mathsf{amb}}}}
+\newcommand{\trval}[1]{\mathcal{T}\sembr{#1}}
+
 % UNIX example
 \newcommand{\UNIX}{UNIX}
 \newcommand{\OSname}[0]{Tiny UNIX}

thesis.bib

@@ -3574,4 +3574,16 @@
   publisher = {Springer Netherlands},
   pages     = {25--63},
   OPTisbn   = {978-94-017-1291-0}
-}
+}
+
+# Sixth order function example
+@article{Okasaki98,
+  author    = {Chris Okasaki},
+  title     = {Functional Pearl: Even Higher-Order Functions for Parsing},
+  journal   = {J. Funct. Program.},
+  volume    = {8},
+  number    = {2},
+  pages     = {195--199},
+  year      = {1998}
+}
+

thesis.tex

@@ -610,17 +610,18 @@ efficiency.
 \section{Why first-class control matters}
 From the perspective of programmers first-class control is a valuable
 programming feature because it enables them to implement their own
-control idioms as if they were native to the programming
+control idioms as if they were native to the programming language (in
-language. More important, with first-class control programmer-defined
+fact this is the very definition of first-class control). More
-control idioms are local phenomena which can be encapsulated in a
+important, with first-class control programmer-defined control idioms
-library such that the rest of the program does not need to be made
+are local phenomena which can be encapsulated in a library such that
-aware of their existence. Conversely, without first-class control some
+the rest of the program does not need to be made aware of their
-control idioms can only be implemented using global program
+existence. Conversely, without first-class control some control idioms
-restructuring techniques such as continuation passing style.
+can only be implemented using global program restructuring techniques
+such as continuation passing style.
 
 From the perspective of compiler engineers first-class control is
 valuable because it unifies several control-related constructs under
-one single construct. First-class control can be beneficial for
+one single construct. First-class control can even be beneficial for
 implementing programming languages which have no notion of first-class
 control in source language. A runtime with support for first-class
 control can considerably simplify and ease maintainability of an
@@ -839,7 +840,7 @@ return type $R$ with state of type $S$, we transform the function
 signature as follows.
 %
 \[
-    \val{A_1 \to \cdots \to A_n \to R}_S
+    \sembr{A_1 \to \cdots \to A_n \to R}_S
   \defas A_1 \to \cdots \to A_n \to S \to R \times S
 \]
 %
@@ -6496,6 +6497,170 @@ getting stuck on an unhandled operation.
   By induction on the typing derivations.
 \end{proof}
 
+\subsection{Effect sugar}
+\label{sec:effect-sugar}
+
+Every effect row which share the same effect variable must mention the
+exact same operations to be complete. Their presence information may
+differ. In higher-order effectful programming this can lead to
+duplication of information, and thus verbose effect
+signature. Verbosity can be a real nuisance in larger codebases.
+%
+We can retrospectively fix this issue with some syntactic sugar rather
+than redesigning the entire effect system to rectify this problem.
+%
+I will describe an ad-hoc elaboration scheme, which is designed to
+emulate Frank's effect polymorphic system~\cite{LindleyMM17} for
+first-order and second-order functions, but might not work so well for
+third-order and above. The reason for focusing on first-order and
+second-order functions is that many familiar and useful functions are
+either first-order or second-order, and in the following sections we
+will mostly be working with first-order and second-order functions
+(although, it should be noted that there exist useful functions at
+higher order, e.g. in Chapter~\ref{ch:handlers-efficiency} we shall
+use third-order functions; for an example of a sixth order function
+see \citet{Okasaki98}).
+
+First, let us consider some small instances of the kind of incomplete
+effect rows we would like to be able to write. Consider the type of
+$\map$ function for lists.
+%
+\[
+  \map : \Record{\alpha \to \beta;\List~\alpha} \to \List~\beta
+\]
+%
+For this type to be correct in $\HCalc$ (and $\BCalc$ for that matter)
+we must annotate the arrows with their effect signatures, e.g.
+%
+\[
+  \map : \Record{\alpha \to \beta \eff \{\varepsilon\};\List~\alpha}
+         \to \List~\beta \eff \{\varepsilon\}
+\]
+%
+The effect annotations do not convey any additional information,
+because the function is entirely parametric in all effects, thus the
+ink spent on the effect annotations is really wasted in this instance.
+%
+To fix this we simply need to instantiate each computation type with
+the same effect variable $\varepsilon$.
+
+A slight variation of this example is an effectful second-order
+function that is parametric in its argument's effects.
+%
+\[
+  (A \to B_1 \eff \{\varepsilon\}) \to B_2 \eff \{\ell : A' \opto B';\varepsilon\} \simeq (A \to B_1 \eff \{\ell : A' \opto B';\varepsilon\}) \to B_2 \eff \{\ell : A' \opto B';\varepsilon\}
+\]
+%
+For the effect row of the functional parameter to be correct it must
+mention the $\ell$ operation.
+%
+The idea here is to push the effect signature inwards. The following
+infix function $\vartriangleleft$ copies operations and their presence
+information from its right argument to its left argument.
+%
+\begin{equations}
+  \vartriangleleft &:& \EffectCat \times \EffectCat \to \EffectCat\\
+  E \vartriangleleft \{\cdot\} &\defas& E\\
+  E \vartriangleleft \{\varepsilon\} &\defas& E\\
+  E \vartriangleleft \{\ell : P;R\} &\defas&
+  \begin{cases}
+    \{\ell : P\} \uplus (E \vartriangleleft \{R\}) & \text{if } \ell \notin E\\
+    \{R\} \vartriangleleft E & \text{otherwise}
+  \end{cases}\\
+\end{equations}
+%
+This function essentially computes the union of the two effect rows.
+
+Another example is an observably pure function whose input is
+effectful, meaning the function must be handling the effects of its
+argument internally (or not apply its argument at all). To capture the
+intuition that operations have been handled, we would like to not
+mention the handled operations in the function's effect signature,
+however, the underlying row polymorphism formalism requires us to
+explicitly mention handled operations as being polymorphic in their
+presence, e.g.
+%
+\[
+  (A \to B_1 \eff \{\ell : A' \opto B';\varepsilon\}) \to B_2 \eff \{\varepsilon\} \simeq (A \to B_1 \eff \{\ell : A' \opto B';\varepsilon\}) \to B_2 \eff \{\ell : \theta;\varepsilon\}
+\]
+%
+The idea is to extract the effect signature of the domain $A$ and then
+copy every operation from this signature into the function's signature
+as polymorphic in its presence if it is not mentioned by the
+function's signature. The following function implements the copy
+aspect of this idea.
+%
+\begin{equations}
+  \vartriangleright &:& \EffectCat \times \EffectCat \to \EffectCat\\
+  \{\cdot\} \vartriangleright E &\defas& E\\
+  \{\varepsilon\} \vartriangleright E &\defas& E\\
+  \{\ell : A \opto B;R\} \vartriangleright E &\defas&
+  \begin{cases}
+    \{\ell : \theta\} \uplus (\{R\} \vartriangleright E) & \text{if } \ell \notin E\\
+    \{R\} \vartriangleright E & \text{otherwise}
+  \end{cases}\\
+  \{\ell : P;R\} \vartriangleright E &\defas&
+  \begin{cases}
+    \{\ell : P\} \uplus (\{R\} \vartriangleright E) & \text{if } \ell \notin E\\
+    \{R\} \vartriangleright E & \text{otherwise}
+  \end{cases}
+\end{equations}
+%
+The only subtlety occur in the interesting case which is when an
+operation is present in the left signature, but not in the right
+signature. In this case we instantiate the operation with a fresh
+presence variable in the output signature.
+%
+\begin{equations}
+  \xval{-} &:& \ValTypeCat \to \EffectCat\\
+  \xval{\alpha} &\defas& \{\cdot\}\\
+  \xval{\Record{R}} &\defas& \xval{[R]} \defas \xval{R}\\
+  \xval{A \to C} &\defas& \xval{A} \vartriangleright \xcomp{C} \\
+  \xval{\forall \alpha^K.C} &\defas& \xcomp{C} \smallskip\\
+  \xcomp{-} &:& \CompTypeCat \to \EffectCat\\
+  \xcomp{A \eff E} &\defas& \xval{A} \vartriangleright E \smallskip\\
+  \xrow{-}  &:& \RowCat \to \Effect\\
+  \xrow{\cdot} &\defas& \xval{\rho} \defas \{\cdot\}\\
+  \xrow{\ell : P;R} &\defas& \xval{P} \vartriangleright \xval{R} \smallskip\\
+  \xpre{-}    &:& \PresenceCat \to \EffectCat\\
+  \xpre{\Pre{A}} &\defas& \xval{A}\\
+  \xpre{\Abs}    &\defas& \xpre{\theta} \defas \{\cdot\}
+\end{equations}
+%
+\begin{equations}
+  \pval{-} &:& \ValTypeCat \times \EffectCat \to \ValTypeCat\\
+  \pval{\alpha}_{\eamb} &\defas& \alpha\\
+  \pval{\Record{R}}_{\eamb} &\defas& \Record{\prow{R}_{\eamb}}\\
+  \pval{[R]}_{\eamb} &\defas& [\prow{R}_{\eamb}]\\
+  \pval{A \to C}_{\eamb} &\defas& \pval{A}_{\eamb} \to \pcomp{C}_{\eamb} \\
+  \pval{\forall \alpha^K.C}_{\eamb} &\defas& \forall\alpha^K.\pcomp{C} \smallskip\\
+  \pcomp{-} &:& \CompTypeCat \times \EffectCat \to \CompTypeCat\\
+  \pcomp{A \eff E}_{\eamb} &\defas& \pval{A}_{\eamb} \eff E \vartriangleleft \eamb \smallskip\\
+  \prow{-}  &:& \RowCat \times \EffectCat \to \RowCat\\
+  \prow{\cdot}_{\eamb} &\defas& \{\cdot\}\\
+  \prow{\rho}_{\eamb} &\defas& \{\rho\}\\
+  \prow{\ell : P;R}_{\eamb} &\defas& \ppre{P};\prow{R} \smallskip\\
+  \ppre{-}    &:& \PresenceCat \times \EffectCat \to \EffectCat\\
+  \ppre{\Pre{A}}_{\eamb} &\defas& \pval{A}_{\eamb}\\
+  \ppre{\Abs}_{\eamb}    &\defas& \Abs\\
+  \ppre{\theta} &\defas& \theta
+\end{equations}
+%
+\begin{equations}
+  \trval{-} &:& \ValTypeCat \to \ValTypeCat\\
+  \trval{A \to B \eff E} &\defas& \pval{A}_{E'} \to \pval{B}_{E'} \eff E' \vartriangleright E\\
+  \multicolumn{3}{l}{\quad\where~E' = \xval{A} \vartriangleright \xval{B}}
+\end{equations}
+% \begin{equations}
+%   \trval{-} &:& \ValTypeCat \to \ValTypeCat\\
+%   \trval{A \to B \eff E} &\defas& A' \to B' \eff E'\\
+%   \multicolumn{3}{l}{\quad\where~(A', E_A) \defas \trval{A}_{E}\;\keyw{and}\;(B', \_) = \trval{B}_{\{\varepsilon\}}\;\keyw{and}\; E' = E_A \vartriangleright E} \medskip\\
+%   \trval{-} &:& \ValTypeCat \times \EffectCat \to \ValTypeCat \times \EffectCat\\
+%   \trval{\UnitType}_{E_{amb}} &\defas& (\UnitType, \{\cdot\})\\
+%   \trval{A \to B \eff E}_{E_{amb}} &\defas& (A' \to B' \eff E', E_A \vartriangleright E)\\
+%   \multicolumn{3}{l}{\quad\where~E' = (E_A \vartriangleright E) \vartriangleleft E_{amb}\;\keyw{and}\;(A', E_A) = \trval{A}_{E'}\;\keyw{and}\;(B', \_) = \trval{B}_{\{\varepsilon\}}}
+% \end{equations}
+
 \section{Composing \UNIX{} with effect handlers}
 \label{sec:deep-handlers-in-action}
 
@@ -8250,7 +8415,7 @@ an unique entry.
                \bl
                   \If\;inode.lno > 1\;\Then\\
                    \quad\bl
-                      \Let\;inode' \revto \Record{inode\;\With\;lno = inode.lno - 1}\\
+                      \Let\;inode' \revto \Record{\bl inode\;\With\\lno = inode.lno - 1}\el\\
                       \In\;\Record{\modify\,\Record{ino;inode';fs.ilist};fs.dreg}
                     \el\\
                   \Else\;
@@ -8428,7 +8593,8 @@ We can now plug it all together.
                \Record{3;
                  \ba[t]{@{}l@{}l}
                    \texttt{"}&\texttt{UNIX is basically a simple operating system, }\\
-                             &\texttt{but you have to be a genius to understand the simplicity.\nl{"}}},
+                             &\texttt{but you have to be a genius }\\
+                             &\texttt{to understand the simplicity.\nl{"}}},
                  \ea\\
                \Record{2;
                  \ba[t]{@{}l@{}l}
@@ -9080,25 +9246,25 @@ analysis utility need not operate on the low level of characters.
     \paste : \UnitType \to \UnitType \eff \{\Await : \UnitType \opto \Char;\Yield : \String \opto \UnitType\}\\
     \paste\,\Unit \defas
       \bl
-        paste'\,\Record{\Do\;\Await~\Unit;\strlit{}}\\
+        pst\,\Record{\Do\;\Await~\Unit;\strlit{}}\\
         \where
           \ba[t]{@{~}l@{~}c@{~}l}
-             paste'\,\Record{\charlit{\textnil};str} &\defas& \Do\;\Yield~str;\Do\;\Yield~\strlit{\textnil}\\
+             pst\,\Record{\charlit{\textnil};str} &\defas& \Do\;\Yield~str;\Do\;\Yield~\strlit{\textnil}\\
-             paste'\,\Record{\charlit{\nl};str} &\defas& \Do\;\Yield~str;\Do\;\Yield~\strlit{\nl};paste'\,\Record{\Do\;\Await~\Unit;\strlit{}}\\
+             pst\,\Record{\charlit{\nl};str} &\defas& \Do\;\Yield~str;\Do\;\Yield~\strlit{\nl};pst\,\Record{\Do\;\Await~\Unit;\strlit{}}\\
-             paste'\,\Record{\charlit{~};str} &\defas& \Do\;\Yield~str;paste'\,\Record{\Do\;\Await~\Unit;\strlit{}}\\
+             pst\,\Record{\charlit{~};str} &\defas& \Do\;\Yield~str;pst\,\Record{\Do\;\Await~\Unit;\strlit{}}\\
-             paste'\,\Record{c;str} &\defas& paste'\,\Record{\Do\;\Await~\Unit;str \concat [c]}
+             pst\,\Record{c;str} &\defas& pst\,\Record{\Do\;\Await~\Unit;str \concat [c]}
 
           \ea
       \el
   \el
 \]
 %
-The heavy-lifting is delegated to the recursive function $paste'$
+The heavy-lifting is delegated to the recursive function $pst$
 which accepts two parameters: 1) the next character in the input
 stream, and 2) a string buffer for building the output string. The
 function is initially applied to the first character from the stream
 (returned by the invocation of $\Await$) and the empty string
-buffer. The function $paste'$ is defined by pattern matching on the
+buffer. The function $pst$ is defined by pattern matching on the
 character parameter. The first three definitions handle the special
 cases when the received character is nil, newline, and space,
 respectively. If the character is nil, then the function yields the