From d12889536183e381b1e58ac630d919404bb012e7 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Daniel=20Hillerstr=C3=B6m?= Date: Fri, 5 Feb 2021 12:30:13 +0000 Subject: [PATCH] Some related work --- thesis.bib | 86 +++++++++++++++++++++++++++++++++++++----------------- thesis.tex | 83 ++++++++++++++++++++++++++++++++++++++++++++++++++-- 2 files changed, 141 insertions(+), 28 deletions(-) diff --git a/thesis.bib b/thesis.bib index 3ab8dc2..234e5a1 100644 --- a/thesis.bib +++ b/thesis.bib @@ -319,6 +319,13 @@ year = {2020} } +@phdthesis{Geron19, + author = {Bram Geron}, + title = {Defined Algebraic Operations}, + school = {University of Birmingham, England, {UK}}, + year = 2019 +} + # Asynchronous effects @article{AhmanP21, author = {Danel Ahman and @@ -509,6 +516,59 @@ year = {2017} } +@inproceedings{Leijen05, + author = {Daan Leijen}, + title = {Extensible records with scoped labels}, + booktitle = {Trends in Functional Programming}, + series = {Trends in Functional Programming}, + volume = {6}, + pages = {179--194}, + publisher = {Intellect}, + year = {2005} +} + +# Helium +@article{BiernackiPPS18, + author = {Dariusz Biernacki and + Maciej Pir{\'{o}}g and + Piotr Polesiuk and + Filip Sieczkowski}, + title = {Handle with care: relational interpretation of algebraic effects and + handlers}, + journal = {Proc. {ACM} Program. Lang.}, + volume = {2}, + number = {{POPL}}, + pages = {8:1--8:30}, + year = {2018} +} + +@article{BiernackiPPS19, + author = {Dariusz Biernacki and + Maciej Pir{\'{o}}g and + Piotr Polesiuk and + Filip Sieczkowski}, + title = {Abstracting algebraic effects}, + journal = {Proc. {ACM} Program. Lang.}, + volume = {3}, + number = {{POPL}}, + pages = {6:1--6:28}, + year = {2019} +} + +@article{BiernackiPPS20, + author = {Dariusz Biernacki and + Maciej Pir{\'{o}}g and + Piotr Polesiuk and + Filip Sieczkowski}, + title = {Binders by day, labels by night: effect instances via lexically scoped + handlers}, + journal = {Proc. {ACM} Program. Lang.}, + volume = {4}, + number = {{POPL}}, + pages = {48:1--48:29}, + year = {2020} +} + # Haskell implementations @inproceedings{KiselyovSS13, author = {Oleg Kiselyov and @@ -1014,20 +1074,6 @@ year = {1986} } -@article{BiernackiPPS18, - author = {Dariusz Biernacki and - Maciej Pir{\'{o}}g and - Piotr Polesiuk and - Filip Sieczkowski}, - title = {Handle with care: relational interpretation of algebraic effects and - handlers}, - journal = {{PACMPL}}, - volume = {2}, - number = {{POPL}}, - pages = {8:1--8:30}, - year = {2018} -} - # Capability passing style @phdthesis{Brachthauser20, author = {Jonathan Immanuel Brachth{\"{a}}user}, @@ -1073,18 +1119,6 @@ year = {2020} } -@article{BrachthauserSO18, - author = {Jonathan Immanuel Brachth{\"{a}}user and - Philipp Schuster and - Klaus Ostermann}, - title = {Effect handlers for the masses}, - journal = {Proc. {ACM} Program. Lang.}, - volume = {2}, - number = {{OOPSLA}}, - pages = {111:1--111:27}, - year = {2018} -} - # explicit effect subtyping @inproceedings{SalehKPS18, author = {Amr Hany Saleh and diff --git a/thesis.tex b/thesis.tex index bb43776..4b0698e 100644 --- a/thesis.tex +++ b/thesis.tex @@ -5466,7 +5466,7 @@ handled recursively. % \[ \bl - \schedule : \List~(\Pstate~\alpha~\{\Fork:\Bool;\varepsilon\}) \to \List~\alpha \eff \varepsilon\\ + \schedule : \List~(\Pstate~\alpha~\{\Fork:\Bool;\varepsilon\}~\theta) \to \List~\alpha \eff \varepsilon\\ \schedule~ps \defas \ba[t]{@{}l} \Let\;run \revto @@ -7940,7 +7940,86 @@ complete is the $\init$ process. \section{Related work} \label{sec:unix-related-work} -\paragraph{Programming languages with handlers} +\paragraph{Programming languages with handlers} The work presented in +this chapter has been retrofitted on to the programming language +Links~\cite{HillerstromL16,HillerstromL18}. A closely related +programming language with handlers is \citeauthor{Leijen17}'s Koka, +which has been retrofitted with ordinary deep and parameterised effect +handlers~\cite{Leijen17}. In Koka effects are nominal, meaning an +effect and its constructors must be declared before use, which is +unlike the structural approach taken in this chapter. Koka also tracks +effects via an effect system based on \citeauthor{Leijen05}-style row +polymorphism~\cite{Leijen05,Leijen14}, where rows are interpreted as +multisets which means an effect can occur multiple times in an effect +row. The ability to repeat effects provide a form for effect scoping +in the sense that an effect instance can shadow another. A handler +handles only the first instance of a repeated effect, leaving the +remaining instances for another handler. Consequently, the order of +repeated effect instances matter and it can therefore be situational +useful to manipulate the order of repeated instances by way of +so-called \emph{effect masking}. +% +The notion of effect masking was formalised by \citet{BiernackiPPS18} +and generalised by \citet{ConventLMM20}. +% + +\citet{BiernackiPPS18} designed Helium, which is a programming +language that features a rich module system, deep handlers, and +\emph{lexical} handlers~\cite{BiernackiPPS20}. Lexical handlers +\emph{bind} effectful operations to specific handler +instances. Operations remain bound for the duration of +computation. This makes the nature of lexical handlers more static +than ordinary deep handlers, as for example it is not possible to +dynamically overload the interpretation of residual effects of a +resumption invocation as in Section~\ref{sec:tiny-unix-env}. +% +The mathematical foundations for lexical handlers has been developed +by \citet{Geron19}. + +The design of the Effekt language by \citet{BrachthauserSO20b} +resolves around the idea of lexical handlers for efficiency. Effekt +takes advantage of the static nature of lexical handlers to eliminate +the dynamic handler lookup at runtime by tying the correct handler +instance directly to an operation +invocation~\cite{BrachthauserS17,SchusterBO20}. The effect system of +Effekt is based on intersection types, which provides a limited form +of effect polymorphism~\cite{BrachthauserSO20b}. A design choice that +means it does not feature first-class functions. + +The Frank language by \citet{LindleyMM17} is born and bred on shallow +effect handlers. One of the key novelties of Frank is $n$-ary shallow +handlers, which generalise ordinary unary shallow handlers to be able +to handle multiple computations simultaneously. Another novelty is the +effect system, which is based on a variation of +\citeauthor{Leijen05}-style row polymorphism, where the programmer +rarely needs to mention effect variables. This is achieved by +insisting that the programmer annotates each input argument with the +particular effects handled at the particular argument position as well +as declaring what effects needs to be handled by the ambient +context. Each annotation is essentially an incomplete row. They are +made complete by concatenating them and inserting a fresh effect +variable. + +\citeauthor{BauerP15}'s Eff language was the first programming +language designed from the ground up with effect handlers in mind. It +features only deep handlers~\cite{BauerP15}. A previous iteration of +the language featured an explicit \emph{effect instance} system. An +effect instance is a sort of generative interface, where the +operations are unique to each instance. As a result it is possible to +handle two distinct instances of the same effect differently in a +single computation. Their system featured a type-and-effect system +with support for effect inference~\cite{Pretnar13,BauerP13}, however, +the effect instance system was later dropped to in favour of a vanilla +nominal approach to effects and handlers. + +Multicore OCaml is, at the time of writing, an experimental branch of +the OCaml programming language, which aims to extend OCaml with effect +handlers for multicore and concurrent +programming~\cite{DolanWM14,DolanWSYM15}. The current incarnation +features untracked nominal effects and deep handlers with single-use +resumptions. + +\dhil{Possibly move to the introduction or background} \paragraph{Effect-driven concurrency} In their tutorial of the Eff programming language \citet{BauerP15}