Related work

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}