|
|
|
@ -248,6 +248,50 @@ |
|
|
|
%% This creates the title page |
|
|
|
\maketitle |
|
|
|
|
|
|
|
%% Lay summary |
|
|
|
\begin{laysummary} |
|
|
|
% This dissertation is about \emph{taking back control} from the |
|
|
|
% operating system and putting it back into the hands of |
|
|
|
% programmers. For too long programmers have been governed by |
|
|
|
% unelected primitives |
|
|
|
Computer programs interact with the real world, e.g. to send and |
|
|
|
retrieve e-mails, stream videos, transferal of data from or onto |
|
|
|
some pluggable data storage medium, and so forth. This interaction |
|
|
|
is governed by the operating system, which is responsible for |
|
|
|
running programs and providing them with the vocabulary to interact |
|
|
|
with the world. |
|
|
|
% |
|
|
|
Programs use words from this vocabulary with a preconceived idea of |
|
|
|
their meaning, however, importantly words are just mere syntax. The |
|
|
|
semantics of each word is determined by the operating system |
|
|
|
(typically such that it aligns with the intent of the program). |
|
|
|
|
|
|
|
This separation of syntax and semantics makes it possible for |
|
|
|
programs and operating systems to evolve independently, because any |
|
|
|
program can be run by any operating system whose vocabulary conforms |
|
|
|
to the expectations of the program. It has proven to be a remarkably |
|
|
|
successful model for building and maintaining computer programs. |
|
|
|
|
|
|
|
\emph{Effect handlers} localise are tiny programmable operating systems |
|
|
|
|
|
|
|
In this dissertation I develop the foundations for programming with |
|
|
|
effect handlers. Specifically, I present a practical design for |
|
|
|
programming with effect handlers as well as applications, I develop |
|
|
|
two universal implementation strategies for effect handlers, and I |
|
|
|
give a precise mathematical characterisation of the inherent |
|
|
|
computational efficiency of effect handlers. |
|
|
|
|
|
|
|
% The meaning of words This separation of |
|
|
|
|
|
|
|
% modular reconfiguration of programs |
|
|
|
|
|
|
|
% Computer programs interact with the real world by way of \emph{system calls}\dots this interaction |
|
|
|
% is facilitated by the operating system, which is responsible for |
|
|
|
% % |
|
|
|
% Effect handlers provide a modular means for structuring the internal |
|
|
|
% code of computer programs. |
|
|
|
\end{laysummary} |
|
|
|
|
|
|
|
%% Acknowledgements |
|
|
|
\begin{acknowledgements} |
|
|
|
Firstly, I want to thank Sam Lindley for his guidance, advice, and |
|
|
|
|