Update acknowledgements

thesis.bib

@@ -331,7 +331,7 @@
 }
 
 @article{LuksicP20,
-  author    = {Ziga Luksic and
+  author    = {{\v{Z}}iga Luk{\v{s}}i{\v{c}} and
                Matija Pretnar},
   title     = {Local algebraic effect theories},
   journal   = {J. Funct. Program.},
@@ -802,6 +802,17 @@
   year      = {1992}
 }
 
+@inproceedings{KingW92,
+  author    = {David J. King and
+               Philip Wadler},
+  title     = {Combining Monads},
+  booktitle = {Functional Programming},
+  series    = {Workshops in Computing},
+  pages     = {134--143},
+  publisher = {Springer},
+  year      = {1992}
+}
+
 @inproceedings{JonesW93,
   author    = {Simon L. Peyton Jones and
                Philip Wadler},
@@ -3404,6 +3415,14 @@
   year      = {1986}
 }
 
+@phdthesis{Lucassen87,
+  author    = {John M. Lucassen},
+  title     = {Types and Effects --- Towards the Integration of
+               Functional and Imperative Programming},
+  school    = {{MIT}, {USA}},
+  year      = 1987
+}
+
 @inproceedings{LucassenG88,
   author    = {John M. Lucassen and
                David K. Gifford},
@@ -3476,3 +3495,19 @@
   publisher = {Springer},
   year      = {2017}
 }
+
+# Žiga Lukšič's PhD thesis on local effect theories
+@phdthesis{Ziga20,
+  author    = {{\v{Z}}iga Luk{\v{s}}i{\v{c}}},
+  title     = {Applications of algebraic effect theories},
+  school    = {University of Ljubljana, Slovenia},
+  year      = {2020}
+}
+
+# Jeremy Yallop's phd thesis
+@phdthesis{Yallop10,
+  author    = {Jeremy Yallop},
+  title     = {Abstraction for web programming},
+  school    = {The University of Edinburgh, {UK}},
+  year      = {2010}
+}

thesis.tex

@@ -158,18 +158,18 @@
   idioms as shareable libraries.
   %
   Effect handlers provide a particularly structured approach to
-  programming with first-class control by separating control reifying
+  programming with first-class control by naming control reifying
-  operations from their handling.
+  operations and separating from their handling.
 
-  This thesis is composed of three strands in which I develop
+  This thesis is composed of three strands of work in which I develop
   operational foundations for programming and implementing effect
   handlers as well as exploring the expressive power of effect
   handlers.
 
   The first strand develops a fine-grain call-by-value core calculus
-  of a statically typed programming language a \emph{structural}
+  of a statically typed programming language with a \emph{structural}
-  notion of effects, as opposed to the \emph{nominal} notion of
+  notion of effect types, as opposed to the \emph{nominal} notion of
-  effects that dominants the literature.
+  effect types that dominates the literature.
   %
   With the structural approach, effects need not be declared before
   use. The usual safety properties of statically typed programming are
@@ -196,37 +196,43 @@
   techniques that admit a unified basis for implementing deep,
   shallow, and parameterised effect handlers in the same environment.
   %
-  The CPS translation is obtained through a series refinements by
+  The CPS translation is obtained through a series of refinements of a
-  starting from a basic first-order CPS translation for a fine-grain
+  basic first-order CPS translation for a fine-grain call-by-value
-  call-by-value language into an untyped language. The initial
+  language into an untyped language.
-  refinement adds support for deep handlers by representing stacks of
-  continuations and handlers as a curried sequence of arguments.
   %
-  The resulting translation is not \emph{properly tail-recursive},
+  Each refinement moves toward a more intensional representation of
-  meaning some function application terms do not appear in tail
+  continuations eventually arriving at the notion of \emph{generalised
-  position. To rectify this the CPS translation is refined once more
+    continuation}, which admit simultaneous support for deep, shallow,
-  to obtain an uncurried representation of stacks of continuations and
+  and parameterised handlers.
-  handlers. Each refinement moves toward a more intensional
+  %
-  representation of continuations eventually arriving at the notion of
+  The initial refinement adds support for deep handlers by
-  \emph{generalised continuation}, which admit simultaneous support
+  representing stacks of continuations and handlers as a curried
-  for deep, shallow, and parameterised handlers. Finally, the
+  sequence of arguments.
-  translation is made higher-order in order to contract administrative
+  %
-  redexes at translation time.
+  The image of the resulting translation is not \emph{properly
+    tail-recursive}, meaning some function application terms do not
+  appear in tail position. To rectify this the CPS translation is
+  refined once more to obtain an uncurried representation of stacks of
+  continuations and handlers. Finally, the translation is made
+  higher-order in order to contract administrative redexes at
+  translation time.
   %
   The generalised continuation representation is used to construct an
-  abstract machine that supports the three kinds of handlers.
+  abstract machine that provide simultaneous support for deep,
+  shallow, and parameterised effect handlers.  kinds of effect
+  handlers.
 
   The third strand explores the expressiveness of effect
   handlers. First, I show that deep, shallow, and parameterised
   notions of handlers are interdefinable by way of \emph{typed
     macro-expressiveness}, which provides a syntactic notion of
-  expressiveness that merely affirms existence of encodings between
+  expressiveness that affirms the existence of encodings between
   handlers, but it provides no information about the computational
   content of the encodings. Second, using the semantic notion of
   \emph{type-respecting expressiveness} I show that for a class of
-  programs a programming language with first-class (e.g. effect
+  programs a programming language with first-class control
-  handlers) admits asymptotically faster implementations than possible
+  (e.g. effect handlers) admits asymptotically faster implementations
-  in a language without first-class.
+  than possible in a language without first-class control.
 %
 }
 
@@ -245,6 +251,42 @@
   encouragement throughout my studies. He has been enthusiastic
   supervisor, and he has always been generous with his time. I am
   fortunate to have been supervised by him.
+  %
+  Secondly, I want to extend my gratitude to John Longley, who has
+  been an admirable second supervisor and who has stimulated my
+  mathematical curiosity.
+  %
+  Thirdly, I want to thank my academic brother Simon Fowler. You have
+  always been a good friend and a pillar of inspiration. Regardless of
+  academic triumphs and failures, we have always been able to laugh at
+  it all and have our own fun.
+
+  I also want to thank KC Sivaramakrishnan for taking a genuine
+  interest in my research early on and for inviting me to come spend
+  some time at OCaml Labs in Cambridge, where I met Anil Madhavapeddy,
+  Stephen Dolan, and Leo White. I have learned so much from each of
+  them and I have been fortunate to enjoy productive and long-standing
+  collaboration with them. Also, thanks to Gemma Gordon, who I had the
+  pleasure of sharing an office with during one of my stints at OCaml
+  Labs.
+
+  I am very grateful for the fruitful and long-standing collaboration
+  with Robert Atkey that I have been fortunate to enjoy. Robert has
+  been a continuous source of inspiration.
+  %
+  Thanks to James McKinna for always asking intellectually
+  interesting, and at times challenging, questions. I have appreciate
+  our many conversations even though I spent days, weeks, sometimes
+  months, and in extreme cases years to think about answers to your
+  questions. Also thanks to Brian Campbell and J. Garrett Morris for
+  putting up with all the supervision meetings that I had with Sam in
+  their shared office 5.28.
+
+  Speaking of offices, I also want to thank my peers from my own
+  office 5.21 for stimulating my general interest in computer science
+  and mathematics beyond programming languages. Also, thanks to my CDT
+  cohort, I want to particularly emphasise my gratitude to Amna
+  Shahab, who has been a truly valuable friend.
 
   Throughout my studies I have received funding from the
   \href{https://www.ed.ac.uk/informatics}{School of Informatics} at
@@ -256,29 +298,11 @@
 
   List of people to thank
   \begin{itemize}
-    \item Sam Lindley
-    \item John Longley
-    \item Christophe Dubach
-    \item KC Sivaramakrishnan
-    \item Stephen Dolan
-    \item Anil Madhavapeddy
-    \item Gemma Gordon
-    \item Leo White
     \item Andreas Rossberg
-    \item Robert Atkey
     \item Jeremy Yallop
-    \item Simon Fowler
-    \item Craig McLaughlin
-    \item Garrett Morris
-    \item James McKinna
-    \item Brian Campbell
     \item Paul Piho
-    \item Amna Shahab
     \item Gordon Plotkin
     \item Ohad Kammar
-    \item School of Informatics (funding)
-    \item Google (Kevin Millikin, Dmitry Stefantsov)
-    \item Microsoft Research (Daan Leijen)
   \end{itemize}
 \end{acknowledgements}
 
@@ -1327,12 +1351,42 @@ The free monad brings us close to the essence of programming with
 effect handlers.
 
 \subsection{Back to direct-style}
-\dhil{The problem with monads is that they do not
+Monads do not freely compose, because monads must satisfy a
-  compose. Cite~\citet{Espinosa95}, \citet{VazouL16} \citet{McBrideP08}}
+distributive property in order to combine~\cite{KingW92}. Alas, not
+every monad has a distributive property.
 %
-Another problem is that monads break the basic doctrine of modular
+The lack of composition is to an extent remedied by monad
-abstraction, which we should program against an abstract interface,
+transformers, which provide a programmatic abstraction for stacking
-not an implementation. A monad is a concrete implementation.
+one monad on top of another~\cite{Espinosa95}. The problem with monad
+transformers is that they enforce an ordering on effects that affects
+the program semantics (c.f. my MSc dissertation for a concrete example
+of this~\cite{Hillerstrom15}).
+
+However, a more fundamental problem with monads is that they break the
+basic doctrine of modular abstraction, which says we should program
+against an abstract interface, not an implementation. Effectful
+programming using monads fixates on the concrete structure first, and
+adds effect operations second. As a result monadic effect operations
+are intimately tied to the concrete structure of their monad.
+
+Before moving onto direct-style alternatives, it is worth mentioning
+\citeauthor{McBrideP08}'s idioms (known as applicative functors in
+Haskell) as an alternative to monadic
+programming~\cite{McBrideP08}. Idioms provide an applicative style for
+programming with effects. Even though idioms are computationally
+weaker than monads, they are still capable of encapsulating a wide
+range of computational effects whose realisation do not require the
+full monad structure (consult \citet{Yallop10} for a technical
+analysis of idioms and monads). Another thing worth pointing out is
+that it is possible to have a direct-style interface for effectful
+programming in the source language, which the compiler can translate
+into monadic binds and returns automatically. For a concrete example
+of this see the work of \citet{VazouL16}.
+
+Let us wrap up this crash course in effectful programming by looking
+at two approaches for programming in direct-style with effects that
+make structured use of delimited control, before finishing with a
+brief discussion of effect tracking.
 
 \subsubsection{Monadic reflection on state}
 %
@@ -1579,23 +1633,37 @@ combined. Throughout the dissertation we will see multiple examples of
 handlers in action (e.g. Chapter~\ref{ch:unary-handlers}).
 
 \subsubsection{Effect tracking}
-\dhil{Cite \citet{GiffordL86}, \citet{LucassenG88}, \citet{TalpinJ92},
+% \dhil{Cite \citet{GiffordL86}, \citet{LucassenG88}, \citet{TalpinJ92},
-\citet{TofteT97}, \citet{NielsonN99}, \citet{WadlerT03}.}
+% \citet{TofteT97}, \citet{WadlerT03}.}
-
 A benefit of using monads for effectful programming is that we get
 effect tracking `for free' (some might object to this statement and
 claim we paid for it by having to program in monadic style). Effect
 tracking is a useful tool for making programming with effects less
-prone to error in much the same way a static type system is useful
+prone to error in much the same way a static type system is useful for
-detecting a wide range of potential runtime errors at compile
+detecting a wide range of potential runtime errors at compile time.
-time.
 
-The principal idea of an effect system is to annotate computation
+Effect systems provide suitable typing discipline for statically
-types with the collection of effects that their inhabitants are
+tracking the observable effects of programs~\cite{NielsonN99}. The
-allowed to perform, e.g. the type $A \to B \eff E$ denotes a function
+notion of effect system was developed around the same time as monads
-that accepts a value of type $A$ as input and ultimately returns a
+rose to prominence, though, its development was independent of
-value of type $B$. As it computes the $B$ value it is allowed to use
+monads. Nevertheless, \citet{WadlerT03} have shown that effect systems
-the operations given by the effect signature $E$.
+and monads are formally related, providing effect systems with some
+formal validity. Subsequently, \citet{Kammar14} has contributed to the
+formal understanding of effect systems through development of a
+general algebraic theory of effect systems. \citet{LucassenG88}
+developed the original effect system as a means for lightweight static
+analyses of functional programs with imperative features. For
+instance, \citet{Lucassen87} made crucial use of an effect system to
+statically distinguish between safe and unsafe terms for parallel
+execution.
+
+The principal idea of a \citeauthor{LucassenG88} style effect system is to
+annotate computation types with the collection of effects that their
+inhabitants are allowed to perform, e.g. the type $A \to B \eff E$ is
+inhabited by functions that accept a value of type $A$ as input and
+ultimately return a value of type $B$. As an inhabitant computes the
+$B$ value it is allowed to perform the effect operations mentioned by
+the effect signature $E$.
 
 This typing discipline fits nicely with the effect handlers-style of
 programming. The $\Do$ construct provides a mechanism for injecting an
@@ -1603,8 +1671,8 @@ operation into the effect signature, whilst the $\Handle$ construct
 provides a way to eliminate an effect operation from the signature.
 %
 If we instantiate $A = \UnitType$, $B = \Bool$, and $E = \Sigma$, then
-we obtain a type-and-effect signature for the control effects version
+we obtain a type-and-effect signature for the handler version of
-of $\incrEven$.
+$\incrEven$.
 %
 \[
   \incrEven : \UnitType \to \Bool \eff \{\Get:\UnitType \opto \Int;\Put:\Int \opto \UnitType\}
@@ -1614,32 +1682,50 @@ Now, the signature of $\incrEven$ communicates precisely what it
 expects from the ambient context. It is clear that we must run this
 function under a handler that interprets at least $\Get$ and $\Put$.
 
-\dhil{Mention the importance of polymorphism in effect tracking}
+Some form of polymorphism is necessary to make an effect system
+extensible and useful in practice. Otherwise effect annotations end up
+pervading the entire program in a similar fashion as monads do. In
+Chapter~\ref{ch:base-language} we will develop an extensible effect
+system based on row polymorphism.
 
 \section{Scope}
-Since the inception of effect handlers numerous variations and
+Summarised in one sentence this dissertation is about practical
-extensions of them have been proposed.  In this dissertation I am
+programming language designs for programming with effect handlers,
-concerned only with \citeauthor{PlotkinP09}'s deep handlers, their
+their foundational implementation techniques, and implications for the
-shallow variation, and parameterised handlers which are a slight
+expressive power of their host language.
-variation of deep handlers.
 
-\subsection{Some pointers to elsewhere}
+Numerous variations and extensions of effect handlers have been
+proposed since their inceptions.  In this dissertation I restrict my
+attention to \citeauthor{PlotkinP09}'s deep handlers, their shallow
+variation, and parameterised handlers which are a slight variation of
+deep handlers. In particular I work with free algebraic theories,
+which is to say my designs do not incorporate equational theories for
+effects. Furthermore, I frame my study in terms of simply-typed and
+polymorphic $\lambda$-calculi for which I give computational
+interpretations in terms of contextual operational semantics and
+realise using two foundational operational techniques: continuation
+passing style and abstract machine semantics. When it comes to
+expressivity studies there are multiple complementary notions of
+expressiveness available in the literature; in this dissertation I
+work with typed macro-expressiveness and type-respecting
+expressiveness notions.
+
+\subsection{Scope extrusion}
 The literature on effect handlers is rich, and my dissertation is but
 one of many on topics related to effect handlers. In this section I
 provide a few pointers to related work involving effect handlers that
 I will not otherwise discuss in this dissertation.
 
-Readers interested in the mathematical theory and original development
+Readers interested in the mathematical foundations and original
-of effect handlers should consult \citeauthor{Pretnar10}'s PhD
+development of effect handlers should consult \citeauthor{Pretnar10}'s
-dissertation~\cite{Pretnar10}.
+PhD dissertation~\cite{Pretnar10}.
 
-Lexical effect handlers are a variation on \citeauthor{PlotkinP09}'s
+Most programming language treatments of algebraic effects and their
-deep handlers, which provide a form of lexical scoping for effect
+handlers sideline equational theories, despite equational theories
-operations, thus statically binding them to their handlers.
+being an important part of the original treatment of effect
-%
+handlers. \citeauthor{Ziga20}'s PhD dissertation brings equations back
-\citeauthor{Geron19}'s PhD dissertation develops the mathematical
+onto the pitch as \citet{Ziga20} develops a core calculus with a novel
-theory of scoped effect operations, whilst \citet{WuSH14} and
+local notion of equational theories for algebraic effects.
-\citet{BiernackiPPS20} studies them from a programming perspective.
 
 To get a grasp of the reasoning principles for effect handlers,
 interested readers should consult \citeauthor{McLaughlin20}'s PhD
@@ -1652,21 +1738,34 @@ techniques for deep handlers due to \citet{BiernackiPPS18}.
 \citeauthor{Ahman17}'s PhD dissertation is relevant for readers
 interested in the integration of computational effects into dependent
 type theories~\cite{Ahman17}. \citeauthor{Ahman17} develops an
-intensional \citet{MartinLof84} style effectful dependent type theory
+intensional \citet{MartinLof84} style dependent type theory equipped
-equipped with a novel computational dependent type.
+with a novel computational dependent type, which makes it possible to
+treat type-dependency in the sequential composition of effectful
+computations uniformly.
 
-Effect handlers were conceived in the realm of category theory to give
+Lexical effect handlers are a variation on \citeauthor{PlotkinP09}'s
-an algebraic treatment of exception handling~\cite{PlotkinP09}. They
+deep handlers, which provide a form of lexical scoping for effect
-were adopted early by functional programmers, who either added
+operations, thus statically binding them to their handlers.
-language-level support for effect handlers~
+%
+\citeauthor{Geron19}'s PhD dissertation develops the mathematical
+theory of scoped effect operations, whilst \citet{WuSH14} and
+\citet{BiernackiPPS20} study them from a programming perspective.
+
+% Effect handlers were conceived in the realm of category theory to give
+% an algebraic treatment of exception handling~\cite{PlotkinP09}. They
+% were adopted early by functional programmers, who either added
+% language-level support for effect handlers~
+Functional programmers were early adopters of effect handlers. They
+either added language-level support for handlers~
 \cite{Hillerstrom15,DolanWSYM15,BiernackiPPS18,Leijen17,BauerP15,BrachthauserSO20a,LindleyMM17,Chiusano20}
 or embedded them in
 libraries~\cite{KiselyovSS13,KiselyovI15,KiselyovS16,KammarLO13,BrachthauserS17,Brady13,XieL20}. Thus
 functional perspectives on effect handlers are plentiful in the
-literature. Only a few has studied effect handlers outside the realm
+literature. There are only a a few takes on effect handlers outside
-of functional programming: \citet{Brachthauser20} offers an
+functional programming: \citeauthor{Brachthauser20}'s PhD dissertation
-object-oriented perspective on effect handlers; \citet{Saleh19}
+contains an object-oriented perspective on effect handlers in
-provides a logic programming perspective via an effect handlers
+Java~\cite{Brachthauser20}; \citeauthor{Saleh19}'s PhD dissertation
+offers a logic programming perspective via an effect handlers
 extension to Prolog; and \citet{Leijen17b} has an imperative take on
 effect handlers in C.