dhil/phd-dissertation
1
0
Fork 0
mirror of https://github.com/dhil/phd-dissertation synced 2026-03-13 02:58:26 +00:00
Code Issues Releases Wiki Activity

Abstract

Browse Source
This commit is contained in:
Daniel Hillerström
2021-02-11 21:15:29 +00:00
parent b8fd8ea43d
commit 7917c2ca0b
1 changed files with 18 additions and 9 deletions
Download Patch File Download Diff File Expand all files Collapse all files

27
thesis.tex
View File

@@ -168,13 +168,13 @@
This thesis is composed of three strands in which I develop This thesis is composed of three strands in which I develop
operational foundations for programming and implementing effect operational foundations for programming and implementing effect
handlers as well as investigating the expressive power of effect handlers as well as exploring the expressive power of effect
handlers. handlers.
The first strand develops a fine-grain call-by-value core calculus 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 a \emph{structural}
notion of effects, as opposed to the dominant \emph{nominal} notion notion of effects, as opposed to the \emph{nominal} notion of
of effects in the literature. effects that dominants the literature.
% %
With the structural approach, effects need not be declared before With the structural approach, effects need not be declared before
use. The usual safety properties of statically typed programming are use. The usual safety properties of statically typed programming are
@@ -192,9 +192,9 @@
trees. trees.
% %
To demonstrate the usefulness of effects and handlers as a practical To demonstrate the usefulness of effects and handlers as a practical
programming abstraction I implement a small \UNIX{}-style operating programming abstraction I implement the essence of a small
system complete with multi-user environment, time-sharing, and file \UNIX{}-style operating system complete with multi-user environment,
I/O. time-sharing, and file I/O.
The second strand studies \emph{continuation passing style} (CPS) The second strand studies \emph{continuation passing style} (CPS)
and \emph{abstract machine semantics}, which are foundational and \emph{abstract machine semantics}, which are foundational
@@ -212,7 +212,7 @@
position. To rectify this the CPS translation is refined once more position. To rectify this the CPS translation is refined once more
to obtain an uncurried representation of stacks of continuations and to obtain an uncurried representation of stacks of continuations and
handlers. Each refinement moves toward a more intensional handlers. Each refinement moves toward a more intensional
representation of continuations eventually leading to the notion of representation of continuations eventually arriving at the notion of
\emph{generalised continuation}, which admit simultaneous support \emph{generalised continuation}, which admit simultaneous support
for deep, shallow, and parameterised handlers. Finally, the for deep, shallow, and parameterised handlers. Finally, the
translation is made higher-order in order to contract administrative translation is made higher-order in order to contract administrative
@@ -221,8 +221,17 @@
The generalised continuation representation is used to construct an The generalised continuation representation is used to construct an
abstract machine that supports the three kinds of handlers. abstract machine that supports the three kinds of handlers.
The third strand investigates the expressive power of effect The third strand explores the expressiveness of effect
handlers. 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
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
handlers) admits asymptotically faster implementations than possible
in a language without first-class.
% %
} }