1
0
mirror of https://github.com/dhil/phd-dissertation synced 2026-03-13 11:08:25 +00:00

Compare commits

...

2 Commits

2 changed files with 193 additions and 25 deletions

View File

@@ -3,7 +3,7 @@
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}, address = {Scotland, {UK}},
month = aug, month = aug,
year = 2015 year = 2015
} }
@@ -13,9 +13,10 @@
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}, address = {Scotland, {UK}},
optmonth = aug, optmonth = aug,
year = 2016, year = 2016,
type = {{MSc(R)} Dissertation}
} }
# OCaml handlers # OCaml handlers
@@ -97,7 +98,7 @@
@phdthesis{Pretnar10, @phdthesis{Pretnar10,
author = {Matija Pretnar}, author = {Matija Pretnar},
title = {Logic and handling of algebraic effects}, title = {Logic and handling of algebraic effects},
school = {The University of Edinburgh, {UK}}, school = {The University of Edinburgh, Scotland, {UK}},
year = {2010} year = {2010}
} }
@@ -239,28 +240,28 @@
@phdthesis{McLaughlin20, @phdthesis{McLaughlin20,
author = {Craig McLaughlin}, author = {Craig McLaughlin},
title = {Relational Reasoning for Effects and Handlers}, title = {Relational Reasoning for Effects and Handlers},
school = {The University of Edinburgh, {UK}}, school = {The University of Edinburgh, Scotland, {UK}},
year = {2020} year = {2020}
} }
@phdthesis{Ahman17, @phdthesis{Ahman17,
author = {Danel Ahman}, author = {Danel Ahman},
title = {Fibred Computational Effects}, title = {Fibred Computational Effects},
school = {The University of Edinburgh, {UK}}, school = {The University of Edinburgh, Scotland, {UK}},
year = {2017} year = {2017}
} }
@phdthesis{Fowler19, @phdthesis{Fowler19,
author = {Simon Fowler}, author = {Simon Fowler},
title = {Typed concurrent functional programming with channels, actors and sessions}, 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} year = {2019}
} }
@phdthesis{Kammar14, @phdthesis{Kammar14,
author = {Ohad Kammar}, author = {Ohad Kammar},
title = {Algebraic theory of type-and-effect systems}, title = {Algebraic theory of type-and-effect systems},
school = {The University of Edinburgh, {UK}}, school = {The University of Edinburgh, Scotland, {UK}},
year = {2014} year = {2014}
} }
@@ -320,7 +321,7 @@
author = {Leo Poulson}, author = {Leo Poulson},
title = {Asynchronous Effect Handling}, title = {Asynchronous Effect Handling},
school = {School of Informatics, The University of Edinburgh}, school = {School of Informatics, The University of Edinburgh},
address = {Scotland}, address = {Scotland, {UK}},
year = 2020, year = 2020,
} }
@@ -457,6 +458,14 @@
year = {2017} 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 # Shonky
@misc{McBride16, @misc{McBride16,
title={Shonky}, title={Shonky},
@@ -837,7 +846,7 @@
howpublished = {{ML Workshop}} howpublished = {{ML Workshop}}
} }
# Delimited Control # Dynamic binding
@inproceedings{KiselyovSS06, @inproceedings{KiselyovSS06,
author = {Oleg Kiselyov and author = {Oleg Kiselyov and
Chung{-}chieh Shan and Chung{-}chieh Shan and
@@ -1171,6 +1180,16 @@
year = {1994} 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 # Landin's J operator
@article{Landin65, @article{Landin65,
author = {Peter J. Landin}, author = {Peter J. Landin},
@@ -1356,6 +1375,25 @@
type = {AI Memo} 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) # MacLisp (catch)
@misc{Moon74, @misc{Moon74,
author = {David A. Moon}, author = {David A. Moon},
@@ -1560,3 +1598,99 @@
publisher = {Cambridge University Press}, publisher = {Cambridge University Press},
year = {1999} 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}
}

View File

@@ -500,7 +500,7 @@ handlers.
Moggi's work gives a precise characterisation of what's \emph{not} Moggi's work gives a precise characterisation of what's \emph{not}
an effect} an effect}
\chapter{Control operators} \chapter{Controlling continuations}
\label{ch:continuations} \label{ch:continuations}
Undelimited control: Landin's J~\cite{Landin98}, Reynolds' 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}, Common Lisp resumable exceptions (condition system)~\cite{Steele90},
F~\cite{FelleisenFDM87,Felleisen88}, control/prompt~\cite{SitaramF90}, F~\cite{FelleisenFDM87,Felleisen88}, control/prompt~\cite{SitaramF90},
shift/reset~\cite{DanvyF89,DanvyF90}, fcontrol~\cite{Sitaram93}, shift/reset~\cite{DanvyF89,DanvyF90}, splitter~\cite{QueinnecS91},
catchcont~\cite{LongleyW08}, effect handlers~\cite{PlotkinP09}. 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}. 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 Conway, who used coroutines as a code idiom in assembly
programs~\cite{Knuth97}. programs~\cite{Knuth97}.
\section{Zoo of control operators} \section{Implementation strategies}
Describe how effect handlers fit amongst shift/reset, prompt/control, Continuation marks. CPS. Stack inspection.
callcc, J, catchcont, etc.
\section{Ad-hoc implementation strategies}
\part{Design} \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 exactly which primitive effects deep handlers bring into our resulting
calculus. calculus.
% %
Deep handlers are defined as folds (catamorphisms) over computation Deep handlers~\cite{PlotkinP09,Pretnar10} are defined as folds
trees, meaning they provide a uniform semantics to the handled (catamorphisms) over computation trees, meaning they provide a uniform
operations of a given computation. In contrast, shallow handlers are semantics to the handled operations of a given computation. In
defined as case-splits over computation trees, and thus, allow a contrast, shallow handlers are defined as case-splits over computation
nonuniform semantics to be given to operations. We will discuss this trees, and thus, allow a nonuniform semantics to be given to
last point in greater detail in operations. We will discuss this last point in greater detail in
Section~\ref{sec:unary-shallow-handlers}. Section~\ref{sec:unary-shallow-handlers}.
@@ -2905,6 +2922,8 @@ process may perform.
\ea \ea
\] \]
% %
\dhil{Cite resumption monad}
%
The $\Done$-tag simply carries the return value of type $\alpha$. The The $\Done$-tag simply carries the return value of type $\alpha$. The
$\Suspended$-tag carries a suspended computation, which returns $\Suspended$-tag carries a suspended computation, which returns
another instance of $\Pstate$, and may or may not perform any further 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. \item The \emph{data region} contains the actual file contents.
\end{enumerate} \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 Figure~\ref{fig:unix-mappings} depicts an example with the three
structures and a mapping between them. structures and a mapping between them.
% %
@@ -4489,6 +4510,19 @@ into the return case body $N$ for their respective binders.
% \section{Dynamic Semantics} % \section{Dynamic Semantics}
% \section{Unifying deep and shallow handlers} % \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} \part{Implementation}
\chapter{Continuation-passing style} \chapter{Continuation-passing style}