From 7063acb4e7585da3deaa2a0cf8a2b230af933a48 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Daniel=20Hillerstr=C3=B6m?= Date: Tue, 21 Dec 2021 16:14:59 +0000 Subject: [PATCH] Related work --- thesis.tex | 162 ++++++++++++++++++++++++++--------------------------- 1 file changed, 81 insertions(+), 81 deletions(-) diff --git a/thesis.tex b/thesis.tex index 55c39ac..29b797e 100644 --- a/thesis.tex +++ b/thesis.tex @@ -5549,87 +5549,6 @@ functionality of the legacy code. \section{Related work} \label{sec:unix-related-work} -\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} implement a simple lightweight thread scheduler. It is different from @@ -8275,6 +8194,7 @@ The metatheoretic properties of $\HCalc$ carries over to $\HPCalc$. \end{proof} \section{Related work} +\label{sec:related-work-calculi} \paragraph{Row polymorphism} Row polymorphism was originally introduced by \citet{Wand87} as a typing discipline for extensible @@ -8322,6 +8242,86 @@ differentiate between \emph{tame} and \emph{wild} functions, where a tame function is one whose body can be translated and run directly on the database, whereas a wild function cannot. +\paragraph{Programming languages with handlers} The union of the +calculi presented in this chapter make up the essence of the +intermediate representation of the Links programming +language~\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. + \part{Implementation} \label{p:implementation}