dhil
/
phd-dissertation
mirror of https://github.com/dhil/phd-dissertation
1
0
Fork 0
Code Issues Releases Wiki Activity
Browse Source

Some notes on control operators and resumptions.

master
Daniel Hillerström 5 years ago
parent
de8158d6ec
commit
5e7ce98c0e
2 changed files with 138 additions and 22 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Unified View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 102
      thesis.bib
  2. 58
      thesis.tex

102
thesis.bib
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},
@ -1560,3 +1569,80 @@
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{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}
}

58
thesis.tex
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'
@ -522,7 +522,24 @@ F~\cite{FelleisenFDM87,Felleisen88}, control/prompt~\cite{SitaramF90},
shift/reset~\cite{DanvyF89,DanvyF90}, fcontrol~\cite{Sitaram93}, shift/reset~\cite{DanvyF89,DanvyF90}, fcontrol~\cite{Sitaram93},
catchcont~\cite{LongleyW08}, effect handlers~\cite{PlotkinP09}. 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}. 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 Conway, who used coroutines as a code idiom in assembly
programs~\cite{Knuth97}. 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} \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 exactly which primitive effects deep handlers bring into our resulting
calculus. 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}. Section~\ref{sec:unary-shallow-handlers}.
@ -2905,6 +2918,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 +3380,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 +4506,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{HaynesF84} \citet{GanzFW99}
\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}

Write Preview
Loading…
Cancel
Save