mirror of
https://github.com/dhil/phd-dissertation
synced 2026-04-28 23:16:32 +01:00
Compare commits
8 Commits
69a2c881b7
...
0e02128d03
| Author | SHA1 | Date | |
|---|---|---|---|
| 0e02128d03 | |||
| aa2b963d0e | |||
| 2f494aae67 | |||
| a36b1cf0d4 | |||
| 53b54056f8 | |||
| f80becc368 | |||
| 6c6d8e2aba | |||
| bc7d89ec5f |
59
thesis.tex
59
thesis.tex
@@ -299,7 +299,7 @@
|
|||||||
%% Acknowledgements
|
%% Acknowledgements
|
||||||
\begin{acknowledgements}
|
\begin{acknowledgements}
|
||||||
Firstly, I want to thank Sam Lindley for his guidance, advice, and
|
Firstly, I want to thank Sam Lindley for his guidance, advice, and
|
||||||
encouragement throughout my studies. He has been enthusiastic
|
encouragement throughout my studies. He has been an enthusiastic
|
||||||
supervisor, and he has always been generous with his time. I am
|
supervisor, and he has always been generous with his time. I am
|
||||||
fortunate to have been supervised by him.
|
fortunate to have been supervised by him.
|
||||||
%
|
%
|
||||||
@@ -309,12 +309,11 @@
|
|||||||
%
|
%
|
||||||
Thirdly, I want to thank my academic brother Simon Fowler, who has
|
Thirdly, I want to thank my academic brother Simon Fowler, who has
|
||||||
always been a good friend and a pillar of inspiration. Regardless of
|
always been a good friend and a pillar of inspiration. Regardless of
|
||||||
academic triumphs and failures, we have always been able to laugh at
|
academic triumphs and failures, we have always had fun.
|
||||||
it all and have our own fun.
|
|
||||||
|
|
||||||
I also want to thank KC Sivaramakrishnan for taking a genuine
|
I am extremely grateful to KC Sivaramakrishnan, who took a genuine
|
||||||
interest in my research early on and for inviting me to come spend
|
interest in my research early on and invited me to come spend some
|
||||||
some time at OCaml Labs in Cambridge. My initial visit to Cambridge
|
time at OCaml Labs in Cambridge. My initial visit to Cambridge
|
||||||
sparked the beginning of a long-standing and productive
|
sparked the beginning of a long-standing and productive
|
||||||
collaboration. Also, thanks to Gemma Gordon, who I had the pleasure
|
collaboration. Also, thanks to Gemma Gordon, who I had the pleasure
|
||||||
of sharing an office with during one of my stints at OCaml Labs.
|
of sharing an office with during one of my stints at OCaml Labs.
|
||||||
@@ -324,25 +323,25 @@
|
|||||||
work is clearly reflected in this dissertation.
|
work is clearly reflected in this dissertation.
|
||||||
%
|
%
|
||||||
I also want to thank my other collaborators: Andreas Rossberg, Anil
|
I also want to thank my other collaborators: Andreas Rossberg, Anil
|
||||||
Madhavapeddy, Leo White, and Stephen Dolan, Jeremy Yallop.
|
Madhavapeddy, Leo White, Stephen Dolan, and Jeremy Yallop.
|
||||||
|
|
||||||
I have had the absolute pleasure of working in LFCS at the same time
|
I have had the pleasure of working in LFCS at the same time as James
|
||||||
as James McKinna. James has always taken a genuine interest in my
|
McKinna. James has always taken a genuine interest in my work and
|
||||||
work and challenged me with intellectually stimulating questions. I
|
challenged me with intellectually stimulating questions. I
|
||||||
have appreciate our many conversations even though I spent days,
|
appreciate our many conversations even though I spent days, weeks,
|
||||||
weeks, sometimes months, and in some instances years to come up with
|
sometimes months, and in some instances years to come up with
|
||||||
adequate answers. I also want to thank other former and present
|
adequate answers. I also want to thank other former and present
|
||||||
members of LFCS and other institutes within Informatics: Brian
|
members of Informatics: Brian Campbell, Christophe Dubach, James
|
||||||
Campbell, Christophe Dubach, James Cheney, J. Garrett Morris, Gordon
|
Cheney, J. Garrett Morris, Gordon Plotkin, Michel Steuwer, Philip
|
||||||
Plotkin, and Michel Steuwer.
|
Wadler, and Stephen Gilmore.
|
||||||
|
|
||||||
My time as a student in Informatics Forum was an enjoyable
|
My time as a student in Informatics Forum has been enjoyable in
|
||||||
experience in large part thanks to my student peers and friends:
|
large part thanks to my friends: Amna Shahab, Chris Vasiladiotis,
|
||||||
Amna Shahab, Chris Vasiladiotis, Craig McLaughlin, Dan Mills, Danel
|
Craig McLaughlin, Dan Mills, Danel Ahman, Frank Emrich, Emanuel
|
||||||
Ahman, Frank Emrich, Emanuel Martinov, Floyd Chitalu, Larisa
|
Martinov, Floyd Chitalu, Larisa Stoltzfus, Jakub Zalewski, Maria
|
||||||
Stoltzfus, Jakub Zalewski, Maria Gorinova, Marcin Szymczak, Rajkarn
|
Gorinova, Marcin Szymczak, Paul Piho, Philip Ginsbach, Radu Ciobanu,
|
||||||
Singh, Rudi Horn, Philip Ginsbach, Paul Piho, Stan Manilov, and
|
Rajkarn Singh, Rudi Horn, Shayan Najd, Stan Manilov, and Vanya
|
||||||
Vanya Yaneva-Cormack.
|
Yaneva-Cormack.
|
||||||
|
|
||||||
Thanks to Ohad Kammar for being a good friend, taking a genuine
|
Thanks to Ohad Kammar for being a good friend, taking a genuine
|
||||||
interest in my work, making it fun to attend virtual conferences,
|
interest in my work, making it fun to attend virtual conferences,
|
||||||
@@ -2326,7 +2325,10 @@ synonymous.
|
|||||||
|
|
||||||
For a function $f : A \to B$ (or partial function $f : A \pto B$) we
|
For a function $f : A \to B$ (or partial function $f : A \pto B$) we
|
||||||
write $f(a) = b$ to mean $(a, b) \in f$, and say that $f$ applied to
|
write $f(a) = b$ to mean $(a, b) \in f$, and say that $f$ applied to
|
||||||
$a$ returns $b$. The notation $f(a)$ means the application of $f$ to
|
$a$ returns $b$. We write $f(P) \defas M$ for the definition of a
|
||||||
|
function with pattern $P$ and expression $M$, and sometimes we will
|
||||||
|
use the anonymous notation $P \mapsto M$ to mean $f(P) \defas M$ for
|
||||||
|
some fresh $f$. The notation $f(a)$ means the application of $f$ to
|
||||||
$a$, and we say that $f(a)$ is defined whenever $f(a) = b$ for some
|
$a$, and we say that $f(a)$ is defined whenever $f(a) = b$ for some
|
||||||
$b$.
|
$b$.
|
||||||
%
|
%
|
||||||
@@ -11339,6 +11341,12 @@ and eliminates extraneous terms at translation
|
|||||||
time~\cite{DanvyN03}. Extraneous terms come in various disguises as we
|
time~\cite{DanvyN03}. Extraneous terms come in various disguises as we
|
||||||
shall see later in this chapter.
|
shall see later in this chapter.
|
||||||
|
|
||||||
|
The complete exposure of the control flow makes CPS a good fit for
|
||||||
|
implementing control operators such as effect handlers. It is an
|
||||||
|
established intermediate representation used by compilers, providing
|
||||||
|
it with merits as a practical compilation
|
||||||
|
target~\cite{Appel92,Kennedy07}.
|
||||||
|
|
||||||
The purpose of this chapter is to use the CPS formalism to develop a
|
The purpose of this chapter is to use the CPS formalism to develop a
|
||||||
universal implementation strategy for deep, shallow, and parameterised
|
universal implementation strategy for deep, shallow, and parameterised
|
||||||
effect handlers. Section~\ref{sec:target-cps} defines a suitable
|
effect handlers. Section~\ref{sec:target-cps} defines a suitable
|
||||||
@@ -19476,8 +19484,9 @@ design space of deep and parameterised notions of multi handlers have
|
|||||||
yet to be explored as well as their applications domains. Thus an
|
yet to be explored as well as their applications domains. Thus an
|
||||||
interesting future direction of research would be to extend $\HCalc$
|
interesting future direction of research would be to extend $\HCalc$
|
||||||
with multi handlers and explore their practical programming
|
with multi handlers and explore their practical programming
|
||||||
applicability. The effect system pose an interesting design challenge
|
applicability. Retrofitting the effect system of $\HCalc$ to provide a
|
||||||
for multi handlers as any problematic quirks that occur with unary
|
good programmer experience for programming with multi handlers pose an
|
||||||
|
interesting design challenge as any quirks that occur with unary
|
||||||
handlers only get amplified in the setting of multi handlers.
|
handlers only get amplified in the setting of multi handlers.
|
||||||
|
|
||||||
\paragraph{Handling linear resources} The implementation of effect
|
\paragraph{Handling linear resources} The implementation of effect
|
||||||
|
|||||||
Reference in New Issue
Block a user