Draft introdoctury bit

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},
+  author    = {Daniel Hillerström},
-    title      =     {Handlers for Algebraic Effects in {Links}},
+  title     = {Handlers for Algebraic Effects in {Links}},
-    school     =     {School of Informatics, The University of Edinburgh},
+  school    = {School of Informatics, The University of Edinburgh},
-    address    =     {Scotland, {UK}},
+  address   = {Scotland, {UK}},
-    month      =     aug,
+  month     = aug,
-    year       =     2015
+  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},
+  author    = {Daniel Hillerström},
-    title      =     {Compilation of Effect Handlers and their Applications in Concurrency},
+  title     = {Compilation of Effect Handlers and their Applications in Concurrency},
-    school     =     {School of Informatics, The University of Edinburgh},
+  school    = {School of Informatics, The University of Edinburgh},
-    address    =     {Scotland, {UK}},
+  address   = {Scotland, {UK}},
-    optmonth      =     aug,
+  optmonth  =     aug,
-    year       =     2016,
+  year      = 2016,
-    type       = {{MSc(R)} thesis}
+  type      = {{MSc(R)} thesis}
 }
 
 # OCaml handlers
@@ -34,16 +34,17 @@
 }
 
 @misc{DolanWSYM15,
-  title = {Effective Concurrency through Algebraic Effects},
+  title     = {Effective Concurrency through Algebraic Effects},
-  author = {Stephen Dolan and Leo White and {KC} Sivaramakrishnan and Jeremy Yallop and Anil Madhavapeddy},
+  author    = {Stephen Dolan and Leo White and {KC} Sivaramakrishnan
-  year = 2015,
+               and Jeremy Yallop and Anil Madhavapeddy},
+  year      = 2015,
   howpublished = {{OCaml} Workshop}
 }
 
 @misc{DolanWM14,
-  title = {Multicore {OCaml}},
+  title     = {Multicore {OCaml}},
-  author = {Stephen Dolan and Leo White and Anil Madhavapeddy},
+  author    = {Stephen Dolan and Leo White and Anil Madhavapeddy},
-  year  = {2014},
+  year      = {2014},
   howpublished = {{OCaml} Workshop}
 }
 
@@ -1226,9 +1227,6 @@
   OPTbibsource = {dblp computer science bibliography, http://dblp.org}
 }
 
-
-
-
 @article{Hughes00,
   author    = {John Hughes},
   title     = {Generalising monads to arrows},
@@ -3555,3 +3553,14 @@
   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}
+}

thesis.tex

@@ -371,30 +371,73 @@
 \chapter{Introduction}
 \label{ch:introduction}
 %
-Functional programmers tend to view programs as impenetrable opaque
+% Programmers tend to view programs as impenetrable opaque boxes, whose
-boxes, whose outputs are determined entirely by their
+% outputs are determined entirely by their
-inputs~\cite{Hughes89,Howard80}. This is a compelling view which
+% inputs~\cite{Hughes89,Howard80}. This is a compelling view which
-admits a canonical mathematical model of
+% admits a canonical mathematical model of
-computation~\cite{Church32,Church41}.
+% computation~\cite{Church32,Church41}.
-%
+% %
-Alas, this view does not capture the reality of practical programs,
+% Alas, this view does not capture the reality of practical programs,
-which perform operations to interact with their ambient environment to
+% which perform operations to interact with their ambient environment to
-for example signal graceful or erroneous termination, manipulate the
+% for example signal graceful or erroneous termination, manipulate the
-file system, fork a new thread, and so forth, all of which may have an
+% file system, fork a new thread, and so forth, all of which may have an
-observable effect on the program state. Interactions with the
+% observable effect on the program state. Interactions with the
-environment are mediated by some local authority (e.g. operating
+% environment are mediated by some local authority (e.g. operating
-system), which confers the meaning of operations~\cite{CartwrightF94}.
+% system), which confers the meaning of operations~\cite{CartwrightF94}.
-%
+% %
-This suggests a view of programs as translucent boxes, which convey
+% This suggests a view of programs as translucent boxes, which convey
-their internal use of operations used to compute their outputs.
+% their internal use of operations used to compute their outputs.
 
-This view underpins the \emph{effectful programming paradigm} in which
+% This view underpins the \emph{effectful programming paradigm} in which
-computational effects constitute an integral part of programs. In
+% computational effects constitute an integral part of programs. In
-effectful programming a computational effect is understood as a
+% effectful programming a computational effect is understood as a
-collection of operations, e.g. exceptions are an effect with a single
+% collection of operations, e.g. exceptions are an effect with a single
-operation \emph{raise}, mutable state is an effect with two operations
+% operation \emph{raise}, mutable state is an effect with two operations
-\emph{get} and \emph{put}, concurrency is an effect with two
+% \emph{get} and \emph{put}, concurrency is an effect with two
-operations \emph{fork} and \emph{yield}, etc~\cite{Moggi91,PlotkinP01}.
+% 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.
+%
+An effect handler is an environment that implements an effect
+interface.
+%
+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 facility 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
@@ -417,20 +460,20 @@ operations \emph{fork} and \emph{yield}, etc~\cite{Moggi91,PlotkinP01}.
 % Practical programming is inherently effectfulPractical programming involves programming with \emph{computational
 %   effects}, or simply effects.
 
-Functional programming offers two distinct, but related, approaches to
+% Functional programming offers two distinct, but related, approaches to
-effectful programming, which \citet{Filinski96} succinctly
+% effectful programming, which \citet{Filinski96} succinctly
-characterises as \emph{effects as data} and \emph{effects as
+% characterises as \emph{effects as data} and \emph{effects as
-  behaviour}. The former uses monads to encapsulate
+%   behaviour}. The former uses monads to encapsulate
-effects~\cite{Moggi91,Wadler92} which is compelling because it
+% effects~\cite{Moggi91,Wadler92} which is compelling because it
-recovers some of benefits of the opaque box view for effectful
+% recovers some of benefits of the opaque box view for effectful
-programs, though, at the expense of a change of programming
+% programs, though, at the expense of a change of programming
-style~\cite{JonesW93}. The latter retains the usual direct style of
+% style~\cite{JonesW93}. The latter retains the usual direct style of
-programming by way of \emph{first-class control}, which is a powerful
+% programming by way of \emph{first-class control}, which is a powerful
-facility that can simulate any computational
+% facility that can simulate any computational
-effect~\cite{Filinski94,Filinski96}.
+% effect~\cite{Filinski94,Filinski96}.
 
-\citeauthor{PlotkinP09}'s \emph{effect handlers} are a recent
+% \citeauthor{PlotkinP09}'s \emph{effect handlers} are a recent
-innovation\dots
+% innovation\dots
 
 % First-class control enables the programmer to reify and manipulate the
 % control state as a first-class data object known as a
@@ -443,8 +486,6 @@ innovation\dots
 % ability can significantly improve the computational expressiveness and
 % efficiency of programming languages~\cite{LongleyN15,HillerstromLL20}.
 
-effect handlers, a recent innovation,
-
 %\citet{Sabry98}
 % Virtually every useful program performs some computational effects
 % such as exceptions, state, concurrency, nondeterminism, interactive