Introduction draft

thesis.bib

@@ -1,22 +1,22 @@
-# Daniel's master's thesis (initial implementation of handlers in Links)
+# My MSc thesis (initial implementation of handlers in Links)
 @MastersThesis{Hillerstrom15,
-    author     =     {Daniel Hillerström},
-    title      =     {Handlers for Algebraic Effects in {Links}},
-    school     =     {School of Informatics, The University of Edinburgh},
-    address    =     {Scotland, {UK}},
-    month      =     aug,
-    year       =     2015
+  author    = {Daniel Hillerström},
+  title     = {Handlers for Algebraic Effects in {Links}},
+  school    = {School of Informatics, The University of Edinburgh},
+  address   = {Scotland, {UK}},
+  month     = aug,
+  year      = 2015
 }
 
-# Daniel's master's thesis (abstract message-passing concurrency model, compilation of handlers)
+# My MSc(R) thesis (abstract message-passing concurrency model, compilation of handlers)
 @MastersThesis{Hillerstrom16,
-    author     =     {Daniel Hillerström},
-    title      =     {Compilation of Effect Handlers and their Applications in Concurrency},
-    school     =     {School of Informatics, The University of Edinburgh},
-    address    =     {Scotland, {UK}},
-    optmonth      =     aug,
-    year       =     2016,
-    type       = {{MSc(R)} thesis}
+  author    = {Daniel Hillerström},
+  title     = {Compilation of Effect Handlers and their Applications in Concurrency},
+  school    = {School of Informatics, The University of Edinburgh},
+  address   = {Scotland, {UK}},
+  optmonth  =     aug,
+  year      = 2016,
+  type      = {{MSc(R)} thesis}
 }
 
 # OCaml handlers
@@ -34,16 +34,17 @@
 }
 
 @misc{DolanWSYM15,
-  title = {Effective Concurrency through Algebraic Effects},
-  author = {Stephen Dolan and Leo White and {KC} Sivaramakrishnan and Jeremy Yallop and Anil Madhavapeddy},
-  year = 2015,
+  title     = {Effective Concurrency through Algebraic Effects},
+  author    = {Stephen Dolan and Leo White and {KC} Sivaramakrishnan
+               and Jeremy Yallop and Anil Madhavapeddy},
+  year      = 2015,
   howpublished = {{OCaml} Workshop}
 }
 
 @misc{DolanWM14,
-  title = {Multicore {OCaml}},
-  author = {Stephen Dolan and Leo White and Anil Madhavapeddy},
-  year  = {2014},
+  title     = {Multicore {OCaml}},
+  author    = {Stephen Dolan and Leo White and Anil Madhavapeddy},
+  year      = {2014},
   howpublished = {{OCaml} Workshop}
 }
 
@@ -741,6 +742,19 @@
   year      = {2012}
 }
 
+# "Proto handlers"
+@inproceedings{CartwrightF94,
+  author    = {Robert Cartwright and
+               Matthias Felleisen},
+  title     = {Extensible Denotational Language Specifications},
+  booktitle = {{TACS}},
+  series    = {Lecture Notes in Computer Science},
+  volume    = {789},
+  pages     = {244--272},
+  publisher = {Springer},
+  year      = {1994}
+}
+
 # Applicative idioms
 @article{McBrideP08,
   author    = {Conor McBride and
@@ -1213,9 +1227,6 @@
   OPTbibsource = {dblp computer science bibliography, http://dblp.org}
 }
 
-
-
-
 @article{Hughes00,
   author    = {John Hughes},
   title     = {Generalising monads to arrows},
@@ -3531,4 +3542,36 @@
   number    = {2},
   pages     = {98--107},
   year      = {1989}
+}
+
+# Curry-Howard correspondence
+@incollection{Howard80,
+  author    = {William A. Howard},
+  title     = {The Formulae-as-Types Notion of Construction},
+  booktitle = {To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus, and Formalism},
+  publisher = {Academic Press},
+  editor    = {Haskell Curry and Hindley B. and Seldin J. Roger and P. Jonathan},
+  year      = 1980
+}
+
+# Criteria for modular programming
+@article{Parnas72,
+  author    = {David Lorge Parnas},
+  title     = {On the Criteria To Be Used in Decomposing Systems into Modules},
+  journal   = {Commun. {ACM}},
+  volume    = {15},
+  number    = {12},
+  pages     = {1053--1058},
+  year      = {1972}
+}
+
+# The universal type
+@InProceedings{Longley03,
+  author    = {John Longley},
+  title     = {Universal Types and What They are Good For},
+  booktitle = {Domain Theory, Logic and Computation},
+  year      = 2003,
+  publisher = {Springer Netherlands},
+  pages     = {25--63},
+  OPTisbn   = {978-94-017-1291-0}
 }

thesis.tex

@@ -371,15 +371,74 @@
 \chapter{Introduction}
 \label{ch:introduction}
 %
-Functional programmers tend to view functions as impenetrable black
-boxes, whose outputs are determined entirely by their
-inputs~\cite{Hughes89}. This is a compelling view which admits a
-canonical mathematical model of
-computation~\cite{Church32,Church41}.
+% Programmers tend to view programs as impenetrable opaque boxes, whose
+% outputs are determined entirely by their
+% inputs~\cite{Hughes89,Howard80}. This is a compelling view which
+% admits a canonical mathematical model of
+% computation~\cite{Church32,Church41}.
+% %
+% Alas, this view does not capture the reality of practical programs,
+% which perform operations to interact with their ambient environment to
+% for example signal graceful or erroneous termination, manipulate the
+% file system, fork a new thread, and so forth, all of which may have an
+% observable effect on the program state. Interactions with the
+% environment are mediated by some local authority (e.g. operating
+% system), which confers the meaning of operations~\cite{CartwrightF94}.
+% %
+% This suggests a view of programs as translucent boxes, which convey
+% their internal use of operations used to compute their outputs.
+
+% This view underpins the \emph{effectful programming paradigm} in which
+% computational effects constitute an integral part of programs. In
+% effectful programming a computational effect is understood as a
+% collection of operations, e.g. exceptions are an effect with a single
+% operation \emph{raise}, mutable state is an effect with two operations
+% \emph{get} and \emph{put}, concurrency is an effect with two
+% operations \emph{fork} and \emph{yield}, etc~\cite{Moggi91,PlotkinP01}.
+
+\citeauthor{PlotkinP09}'s \emph{effect handlers} provide a promising
+modular basis for effectful
+programming~\cite{PlotkinP09,PlotkinP13,KammarLO13}. The basic tenet
+of programming with effect handlers is that programs are written with
+respect to an interface of effectful operations they expect to be
+offered by their environment.
 %
-Alas, this view does not capture the reality of practical programs,
-which must interact with their environment (i.e. operating system) to
-facilitate file I/O\dots
+An effect handler is an environment that implements an effect
+interface (also known as a computational effect).
+%
+Programs can run under any effect handler whose implementation
+conforms to the expected effect interface.
+%
+
+In this regard, the \emph{doing} and \emph{being} of effects are kept
+separate~\cite{JonesW93,LindleyMM17}, which is a necessary condition
+for modular abstraction~\cite{Parnas72}.
+%
+A key property of effect handlers is that they provide modular
+instantiation of effect interfaces through seamless composition,
+meaning the programmer can compose any number of complementary
+handlers to obtain a full implementation of some
+interface~\cite{HillerstromL16}.
+%
+The ability to seamless compose handlers gives to a programming
+paradigm which we shall call \emph{effect handler oriented
+  programming} in which the meaning of effectful programs may be
+decomposed into a collection of fine-grained effect handlers.
+
+The key enabler for seamless composition is \emph{first-class
+  control}, which provides a mechanism for reifying the program
+control state as a first-class data object known as a
+continuation~\cite{FriedmanHK84}.
+%
+Through structured manipulation of continuations control gets
+transferred between programs and their handlers.
+
+In this dissertation I present a practical design for programming
+languages with support for effect handler oriented programming, I
+develop two foundational implementation techniques for effect
+handlers, and I study their inherent computational expressiveness and
+efficiency.
+
 % Alas, this view does not capture the reality of practical programs, which
 % may use a variety of observable computational effects such as
 % exceptions, state, concurrency, interactive input/output, and so
@@ -401,24 +460,22 @@ facilitate file I/O\dots
 % Practical programming is inherently effectfulPractical programming involves programming with \emph{computational
 %   effects}, or simply effects.
 
-Functional programming offers two distinct, but related, approaches to
-effectful programming, which \citet{Filinski96} succinctly
-characterises as \emph{effects as data} and \emph{effects as
-  behaviour}. The former uses monads to encapsulate
-effects~\cite{Moggi91,Wadler92} which is compelling because it extends
-the black box view to effectful functions, though, at the expense of a
-change of programming style~\cite{JonesW93}. The latter retains the
-usual direct style of programming by way of \emph{first-class
-  control}, which is a powerful facility that can simulate any
-effect~\cite{Filinski94,Filinski96}. First-class control enables the
-programmer to manipulate and reify the control state as a first-class
-data object known as a continuation~\cite{FriedmanHK84}. First-class
-control has the ability pry open function boundaries, which fractures
-the black box view of computation. This ability can significantly
-improve the computational expressiveness and efficiency of programming
-languages~\cite{LongleyN15,HillerstromLL20}.
+% Functional programming offers two distinct, but related, approaches to
+% effectful programming, which \citet{Filinski96} succinctly
+% characterises as \emph{effects as data} and \emph{effects as
+%   behaviour}. The former uses monads to encapsulate
+% effects~\cite{Moggi91,Wadler92} which is compelling because it
+% recovers some of benefits of the opaque box view for effectful
+% programs, though, at the expense of a change of programming
+% style~\cite{JonesW93}. The latter retains the usual direct style of
+% programming by way of \emph{first-class control}, which is a powerful
+% facility that can simulate any computational
+% effect~\cite{Filinski94,Filinski96}.
 
-effect handlers, a recent innovation,
+% Programmers with continuations at their disposal have the ability to
+% pry open function boundaries, which shatters the opaque box view. This
+% ability can significantly improve the computational expressiveness and
+% efficiency of programming languages~\cite{LongleyN15,HillerstromLL20}.
 
 %\citet{Sabry98}
 % Virtually every useful program performs some computational effects
@@ -568,26 +625,81 @@ 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
 implementation of a programming language with various distinct
-second-class control idioms such as async/await, coroutines, etc,
-because compiler engineers need only implement and maintain a single
-control mechanism rather than having to implement and maintain
-individual runtime support for each control idiom of the source
-language.
+second-class control idioms such as async/await~\cite{SymePL11},
+coroutines~\cite{MouraI09}, etc, because compiler engineers need only
+implement and maintain a single control mechanism rather than having
+to implement and maintain individual runtime support for each control
+idiom of the source language.
 
-% From either perspective first-class control adds value to a
-% programming language regardless of whether it is featured in the
-% source language.
-
-% \subsection{Flavours of control}
-% \paragraph{Undelimited control}
-% \paragraph{Delimited control}
-% \paragraph{Composable control}
+The idea of first-class control is old. It was conceived already
+during the design of the programming language
+Algol~\cite{BackusBGKMPRSVWWW60} (one of the early high-level
+programming languages along with Fortran~\cite{BackusBBGHHNSSS57} and
+Lisp~\cite{McCarthy60}) when \citet{Landin98} sought to model
+unrestricted goto-style jumps using an extended $\lambda$-calculus.
+%
+Since then a wide variety of first-class control operators have
+appeared. We can coarsely categorise them into two groups:
+\emph{undelimited} and \emph{delimited} (in
+Chapter~\ref{ch:continuations} we will perform a finer analysis of
+first-class control). Undelimited control operators are global
+phenomena that let programmers capture the entire control state of
+their programs, whereas delimited control operators are local
+phenomena that provide programmers with fine-grain control over which
+parts of the control state to capture.
+%
+Thus there are good reasons for preferring delimited control over
+undelimited control for practical programming.
 
 \subsection{Why effect handlers matter}
-\dhil{Something about structured programming with delimited control}
+%
+The problem with traditional delimited control operators such as
+\citeauthor{DanvyF90}'s shift/reset~\cite{DanvyF90} or
+\citeauthor{Felleisen88}'s control/prompt~\cite{Felleisen88} is that
+they hard-wire an implementation for the \emph{control effect}
+interface, which provides only a single operation for reifying the
+control state. In itself this interface does not limit what effects
+are expressible as the control effect is in a particular sense `the
+universal effect' because it can simulate any other computational
+effect~\cite{Filinski96}.
+
+The problem, meanwhile, is that the universality of the control effect
+hinders modular programming as the control effect is inherently
+unstructured. In essence, programming with traditional delimited
+control to simulate effects is analogous to programming with the
+universal type~\cite{Longley03} in statically typed programming
+languages, and having to program with the universal type is usually a
+telltale that the programming abstraction is inadequate for the
+intended purpose.
+
+In contrast, effect handlers provide a structured form of delimited
+control, where programmers can give distinct names to control reifying
+operations and separate the from their handling.
+%
+\dhil{Maybe expand this a bit more to really sell it}
 
 \section{State of effectful programming}
 
+Functional programmers tend to view programs as impenetrable black
+boxes, whose outputs are determined entirely by their
+inputs~\cite{Hughes89,Howard80}. This is a compelling view which
+admits a canonical mathematical model of
+computation~\cite{Church32,Church41}. Alas, this view does not capture
+the reality of practical programs, which interact their environment.
+%
+Functional programming prominently features two distinct, but related,
+approaches to effectful programming, which \citet{Filinski96}
+succinctly characterises as \emph{effects as data} and \emph{effects
+  as behaviour}.
+%
+The former uses data abstraction to encapsulate
+effects~\cite{Moggi91,Wadler92} which is compelling because it
+recovers some of benefits of the black box view for effectful
+programs, though, at the expense of a change of programming
+style~\cite{JonesW93}. The latter retains the usual direct style of
+programming either by hard-wiring the semantics of the effects into
+the language or by more flexible means via first-class control.
+
 In this section I will provide a brief programming perspective on
 different approaches to programming with effects along with an
 informal introduction to the related concepts. We will look at each