diff --git a/thesis.bib b/thesis.bib index 4bd5bbe..cdae2a6 100644 --- a/thesis.bib +++ b/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}, @@ -1559,4 +1568,81 @@ title = {Purely functional data structures}, 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{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{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} } \ No newline at end of file diff --git a/thesis.tex b/thesis.tex index 7d8cce5..e1f1fe6 100644 --- a/thesis.tex +++ b/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' @@ -522,7 +522,24 @@ F~\cite{FelleisenFDM87,Felleisen88}, control/prompt~\cite{SitaramF90}, shift/reset~\cite{DanvyF89,DanvyF90}, 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} + +\section{Second-Class control operators} +Coroutines, async/await, generators/iterators, amb. Backtracking: Amb~\cite{McCarthy63}. @@ -531,12 +548,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 +1992,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 +2918,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 +3380,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 +4506,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{HaynesF84} \citet{GanzFW99} + +\subsection{Effect-driven concurrency} +\citet{BauerP15}, \citet{DolanWSYM15}, \citet{Hillerstrom16}, \citet{DolanEHMSW17}, \citet{Convent17}, \citet{Poulson20} + \part{Implementation} \chapter{Continuation-passing style}