mirror of
https://github.com/dhil/phd-dissertation
synced 2026-03-13 11:08:25 +00:00
Compare commits
2 Commits
de8158d6ec
...
ab38da7102
| Author | SHA1 | Date | |
|---|---|---|---|
| ab38da7102 | |||
| 5e7ce98c0e |
152
thesis.bib
152
thesis.bib
@@ -3,7 +3,7 @@
|
||||
author = {Daniel Hillerström},
|
||||
title = {Handlers for Algebraic Effects in {Links}},
|
||||
school = {School of Informatics, The University of Edinburgh},
|
||||
address = {Scotland},
|
||||
address = {Scotland, {UK}},
|
||||
month = aug,
|
||||
year = 2015
|
||||
}
|
||||
@@ -13,9 +13,10 @@
|
||||
author = {Daniel Hillerström},
|
||||
title = {Compilation of Effect Handlers and their Applications in Concurrency},
|
||||
school = {School of Informatics, The University of Edinburgh},
|
||||
address = {Scotland},
|
||||
address = {Scotland, {UK}},
|
||||
optmonth = aug,
|
||||
year = 2016,
|
||||
type = {{MSc(R)} Dissertation}
|
||||
}
|
||||
|
||||
# OCaml handlers
|
||||
@@ -97,7 +98,7 @@
|
||||
@phdthesis{Pretnar10,
|
||||
author = {Matija Pretnar},
|
||||
title = {Logic and handling of algebraic effects},
|
||||
school = {The University of Edinburgh, {UK}},
|
||||
school = {The University of Edinburgh, Scotland, {UK}},
|
||||
year = {2010}
|
||||
}
|
||||
|
||||
@@ -239,28 +240,28 @@
|
||||
@phdthesis{McLaughlin20,
|
||||
author = {Craig McLaughlin},
|
||||
title = {Relational Reasoning for Effects and Handlers},
|
||||
school = {The University of Edinburgh, {UK}},
|
||||
school = {The University of Edinburgh, Scotland, {UK}},
|
||||
year = {2020}
|
||||
}
|
||||
|
||||
@phdthesis{Ahman17,
|
||||
author = {Danel Ahman},
|
||||
title = {Fibred Computational Effects},
|
||||
school = {The University of Edinburgh, {UK}},
|
||||
school = {The University of Edinburgh, Scotland, {UK}},
|
||||
year = {2017}
|
||||
}
|
||||
|
||||
@phdthesis{Fowler19,
|
||||
author = {Simon Fowler},
|
||||
title = {Typed concurrent functional programming with channels, actors and sessions},
|
||||
school = {The University of Edinburgh, {UK}},
|
||||
school = {The University of Edinburgh, Scotland, {UK}},
|
||||
year = {2019}
|
||||
}
|
||||
|
||||
@phdthesis{Kammar14,
|
||||
author = {Ohad Kammar},
|
||||
title = {Algebraic theory of type-and-effect systems},
|
||||
school = {The University of Edinburgh, {UK}},
|
||||
school = {The University of Edinburgh, Scotland, {UK}},
|
||||
year = {2014}
|
||||
}
|
||||
|
||||
@@ -320,7 +321,7 @@
|
||||
author = {Leo Poulson},
|
||||
title = {Asynchronous Effect Handling},
|
||||
school = {School of Informatics, The University of Edinburgh},
|
||||
address = {Scotland},
|
||||
address = {Scotland, {UK}},
|
||||
year = 2020,
|
||||
}
|
||||
|
||||
@@ -457,6 +458,14 @@
|
||||
year = {2017}
|
||||
}
|
||||
|
||||
@MastersThesis{Convent17,
|
||||
author = {Lukas Convent},
|
||||
title = {Enhancing a Modular Effectful Programming Language},
|
||||
school = {School of Informatics, The University of Edinburgh},
|
||||
address = {Scotland, {UK}},
|
||||
year = 2017,
|
||||
}
|
||||
|
||||
# Shonky
|
||||
@misc{McBride16,
|
||||
title={Shonky},
|
||||
@@ -837,7 +846,7 @@
|
||||
howpublished = {{ML Workshop}}
|
||||
}
|
||||
|
||||
# Delimited Control
|
||||
# Dynamic binding
|
||||
@inproceedings{KiselyovSS06,
|
||||
author = {Oleg Kiselyov and
|
||||
Chung{-}chieh Shan and
|
||||
@@ -1171,6 +1180,16 @@
|
||||
year = {1994}
|
||||
}
|
||||
|
||||
# Simulation of delimited control using undelimited control
|
||||
@inproceedings{Filinski94,
|
||||
author = {Andrzej Filinski},
|
||||
title = {Representing Monads},
|
||||
booktitle = {{POPL}},
|
||||
pages = {446--457},
|
||||
publisher = {{ACM} Press},
|
||||
year = {1994}
|
||||
}
|
||||
|
||||
# Landin's J operator
|
||||
@article{Landin65,
|
||||
author = {Peter J. Landin},
|
||||
@@ -1356,6 +1375,25 @@
|
||||
type = {AI Memo}
|
||||
}
|
||||
|
||||
# Splitter
|
||||
@inproceedings{QueinnecS91,
|
||||
author = {Christian Queinnec and
|
||||
Bernard P. Serpette},
|
||||
title = {A Dynamic Extent Control Operator for Partial Continuations},
|
||||
booktitle = {{POPL}},
|
||||
pages = {174--184},
|
||||
publisher = {{ACM} Press},
|
||||
year = {1991}
|
||||
}
|
||||
|
||||
# Comparison of (some) delimited control operators
|
||||
@misc{Shan04,
|
||||
author = {Chung{-}chieh Shan},
|
||||
title = {Shift to Control},
|
||||
howpublished = {{ACM SIGPLAN} Scheme Workshop},
|
||||
year = {2004}
|
||||
}
|
||||
|
||||
# MacLisp (catch)
|
||||
@misc{Moon74,
|
||||
author = {David A. Moon},
|
||||
@@ -1560,3 +1598,99 @@
|
||||
publisher = {Cambridge University Press},
|
||||
year = {1999}
|
||||
}
|
||||
|
||||
# Interleaved computation
|
||||
@inproceedings{Milner75,
|
||||
author = {Robin Milner},
|
||||
title = {Processes: A Mathematical Model of Computing Agents},
|
||||
booktitle = {Studies in Logic and the Foundations of Mathematics},
|
||||
publisher = {Elsevier},
|
||||
pages = {157--173},
|
||||
year = {1975}
|
||||
}
|
||||
|
||||
@article{Plotkin76,
|
||||
author = {Gordon D. Plotkin},
|
||||
title = {A Powerdomain Construction},
|
||||
journal = {{SIAM} J. Comput.},
|
||||
volume = {5},
|
||||
number = {3},
|
||||
pages = {452--487},
|
||||
year = {1976}
|
||||
}
|
||||
|
||||
@inproceedings{Wand80,
|
||||
author = {Mitchell Wand},
|
||||
title = {Continuation-Based Multiprocessing},
|
||||
booktitle = {{LISP} Conference},
|
||||
pages = {19--28},
|
||||
publisher = {{ACM}},
|
||||
year = {1980}
|
||||
}
|
||||
|
||||
@inproceedings{HaynesF84,
|
||||
author = {Christopher T. Haynes and
|
||||
Daniel P. Friedman},
|
||||
title = {Engines Build Process Abstractions},
|
||||
booktitle = {{LISP} and Functional Programming},
|
||||
pages = {18--24},
|
||||
publisher = {{ACM}},
|
||||
year = {1984}
|
||||
}
|
||||
|
||||
@techreport{Moggi90,
|
||||
title = {An Abstract View of Programming Languages},
|
||||
author = {Eugenio Moggi},
|
||||
institution = {{LFCS}, The University of Edinburgh},
|
||||
number = {ECS-LFCS-90-113},
|
||||
year = {1990},
|
||||
address = {Scotland, {UK}}
|
||||
}
|
||||
|
||||
@inproceedings{HiebD90,
|
||||
author = {Robert Hieb and
|
||||
R. Kent Dybvig},
|
||||
title = {Continuations and Concurrency},
|
||||
booktitle = {{PPOPP}},
|
||||
pages = {128--136},
|
||||
publisher = {{ACM}},
|
||||
year = {1990}
|
||||
}
|
||||
|
||||
@inproceedings{GanzFW99,
|
||||
author = {Steven E. Ganz and
|
||||
Daniel P. Friedman and
|
||||
Mitchell Wand},
|
||||
title = {Trampolined Style},
|
||||
booktitle = {{ICFP}},
|
||||
pages = {18--27},
|
||||
publisher = {{ACM}},
|
||||
year = {1999}
|
||||
}
|
||||
|
||||
@inproceedings{Papaspyrou01,
|
||||
author = {Nikolaos S. Papspyrou},
|
||||
title = {A resumption monad transformer and its applications in the semantics of concurrency},
|
||||
booktitle = {Proceedings of the 3rd Panhellenic Logic Symposium},
|
||||
address = {Anogia, Greece}
|
||||
}
|
||||
|
||||
@inproceedings{Harrison06,
|
||||
author = {William L. Harrison},
|
||||
title = {The Essence of Multitasking},
|
||||
booktitle = {{AMAST}},
|
||||
series = {Lecture Notes in Computer Science},
|
||||
volume = {4019},
|
||||
pages = {158--172},
|
||||
publisher = {Springer},
|
||||
year = {2006}
|
||||
}
|
||||
|
||||
@article{AtkeyJ15,
|
||||
author = {Robert Atkey and
|
||||
Patricia Johann},
|
||||
title = {Interleaving data and effects},
|
||||
journal = {J. Funct. Program.},
|
||||
volume = {25},
|
||||
year = {2015}
|
||||
}
|
||||
66
thesis.tex
66
thesis.tex
@@ -500,7 +500,7 @@ handlers.
|
||||
Moggi's work gives a precise characterisation of what's \emph{not}
|
||||
an effect}
|
||||
|
||||
\chapter{Control operators}
|
||||
\chapter{Controlling continuations}
|
||||
\label{ch:continuations}
|
||||
|
||||
Undelimited control: Landin's J~\cite{Landin98}, Reynolds'
|
||||
@@ -519,10 +519,31 @@ delimiters in her PhD dissertation~\cite{Talcott85}.
|
||||
%
|
||||
Common Lisp resumable exceptions (condition system)~\cite{Steele90},
|
||||
F~\cite{FelleisenFDM87,Felleisen88}, control/prompt~\cite{SitaramF90},
|
||||
shift/reset~\cite{DanvyF89,DanvyF90}, fcontrol~\cite{Sitaram93},
|
||||
catchcont~\cite{LongleyW08}, effect handlers~\cite{PlotkinP09}.
|
||||
shift/reset~\cite{DanvyF89,DanvyF90}, splitter~\cite{QueinnecS91},
|
||||
fcontrol~\cite{Sitaram93}, catchcont~\cite{LongleyW08}, effect
|
||||
handlers~\cite{PlotkinP09}.
|
||||
|
||||
Continuation marks?
|
||||
|
||||
\section{Notions of continuations}
|
||||
|
||||
Escape continuations, undelimited continuations, delimited
|
||||
continuations, composable continuations.
|
||||
|
||||
\section{First-Class control operators}
|
||||
Describe how effect handlers fit amongst shift/reset, prompt/control,
|
||||
callcc, J, catchcont, etc.
|
||||
|
||||
\subsection{Escape operators}
|
||||
|
||||
\subsection{Undelimited operators}
|
||||
|
||||
\subsection{Delimited operators}
|
||||
Comparison of various delimited control
|
||||
operators~\cite{Shan04}. Simulation of delimited control using
|
||||
undelimited control~\cite{Filinski94}
|
||||
|
||||
\section{Second-Class control operators}
|
||||
Coroutines, async/await, generators/iterators, amb.
|
||||
|
||||
Backtracking: Amb~\cite{McCarthy63}.
|
||||
|
||||
@@ -531,12 +552,8 @@ Coroutines~\cite{DahlDH72} as introduced by Simula
|
||||
Conway, who used coroutines as a code idiom in assembly
|
||||
programs~\cite{Knuth97}.
|
||||
|
||||
\section{Zoo of control operators}
|
||||
Describe how effect handlers fit amongst shift/reset, prompt/control,
|
||||
callcc, J, catchcont, etc.
|
||||
|
||||
\section{Ad-hoc implementation strategies}
|
||||
|
||||
\section{Implementation strategies}
|
||||
Continuation marks. CPS. Stack inspection.
|
||||
|
||||
\part{Design}
|
||||
|
||||
@@ -1979,12 +1996,12 @@ without the recursion operator. We elect to do so to understand
|
||||
exactly which primitive effects deep handlers bring into our resulting
|
||||
calculus.
|
||||
%
|
||||
Deep handlers are defined as folds (catamorphisms) over computation
|
||||
trees, meaning they provide a uniform semantics to the handled
|
||||
operations of a given computation. In contrast, shallow handlers are
|
||||
defined as case-splits over computation trees, and thus, allow a
|
||||
nonuniform semantics to be given to operations. We will discuss this
|
||||
last point in greater detail in
|
||||
Deep handlers~\cite{PlotkinP09,Pretnar10} are defined as folds
|
||||
(catamorphisms) over computation trees, meaning they provide a uniform
|
||||
semantics to the handled operations of a given computation. In
|
||||
contrast, shallow handlers are defined as case-splits over computation
|
||||
trees, and thus, allow a nonuniform semantics to be given to
|
||||
operations. We will discuss this last point in greater detail in
|
||||
Section~\ref{sec:unary-shallow-handlers}.
|
||||
|
||||
|
||||
@@ -2905,6 +2922,8 @@ process may perform.
|
||||
\ea
|
||||
\]
|
||||
%
|
||||
\dhil{Cite resumption monad}
|
||||
%
|
||||
The $\Done$-tag simply carries the return value of type $\alpha$. The
|
||||
$\Suspended$-tag carries a suspended computation, which returns
|
||||
another instance of $\Pstate$, and may or may not perform any further
|
||||
@@ -3365,6 +3384,8 @@ with files.
|
||||
\item The \emph{data region} contains the actual file contents.
|
||||
\end{enumerate}
|
||||
%
|
||||
\dhil{Motivate i-nodes, etc. Real UNIX file system use those structures. Admit simplification: no file handles; no resource leakage}
|
||||
%
|
||||
Figure~\ref{fig:unix-mappings} depicts an example with the three
|
||||
structures and a mapping between them.
|
||||
%
|
||||
@@ -4489,6 +4510,19 @@ into the return case body $N$ for their respective binders.
|
||||
% \section{Dynamic Semantics}
|
||||
% \section{Unifying deep and shallow handlers}
|
||||
|
||||
\section{Related work}
|
||||
\label{sec:unix-related-work}
|
||||
|
||||
\subsection{Interleaving computation}
|
||||
|
||||
\paragraph{The resumption monad} \citet{Milner75},
|
||||
\citet{Plotkin76}, \citet{Moggi90}, \citet{Papaspyrou01}, \citet{Harrison06}, \citet{AtkeyJ15}
|
||||
|
||||
\paragraph{Continuation-based interleaving} \citet{Wand80} \citet{HaynesF84} \citet{GanzFW99} \citet{HiebD90}
|
||||
|
||||
\subsection{Effect-driven concurrency}
|
||||
\citet{BauerP15}, \citet{DolanWSYM15}, \citet{Hillerstrom16}, \citet{DolanEHMSW17}, \citet{Convent17}, \citet{Poulson20}
|
||||
|
||||
\part{Implementation}
|
||||
|
||||
\chapter{Continuation-passing style}
|
||||
|
||||
Reference in New Issue
Block a user