diff --git a/thesis.bib b/thesis.bib index df72543..6ddf654 100644 --- a/thesis.bib +++ b/thesis.bib @@ -331,7 +331,7 @@ } @article{LuksicP20, - author = {Ziga Luksic and + author = {{\v{Z}}iga Luk{\v{s}}i{\v{c}} and Matija Pretnar}, title = {Local algebraic effect theories}, journal = {J. Funct. Program.}, @@ -3475,4 +3475,12 @@ pages = {339--363}, publisher = {Springer}, year = {2017} +} + +# Žiga Lukšič's PhD thesis on local effect theories +@phdthesis{Ziga20, + author = {{\v{Z}}iga Luk{\v{s}}i{\v{c}}}, + title = {Applications of algebraic effect theories}, + school = {University of Ljubljana, Slovenia}, + year = {2020} } \ No newline at end of file diff --git a/thesis.tex b/thesis.tex index 7b300f7..c8f5fcf 100644 --- a/thesis.tex +++ b/thesis.tex @@ -1617,21 +1617,43 @@ function under a handler that interprets at least $\Get$ and $\Put$. \dhil{Mention the importance of polymorphism in effect tracking} \section{Scope} -Since the inception of effect handlers numerous variations and -extensions of them have been proposed. In this dissertation I am -concerned only with \citeauthor{PlotkinP09}'s deep handlers, their -shallow variation, and parameterised handlers which are a slight -variation of deep handlers. - -\subsection{Some pointers to elsewhere} +Summarised in one sentence this dissertation is about practical +programming language designs for programming with effect handlers, +their foundational implementation techniques, and implications for the +expressive power of their host language. + +Numerous variations and extensions of effect handlers have been +proposed since their inceptions. In this dissertation I restrict my +attention to \citeauthor{PlotkinP09}'s deep handlers, their shallow +variation, and parameterised handlers which are a slight variation of +deep handlers. In particular I work with free algebraic theories, +which is to say my designs do not incorporate equational theories for +effects. Furthermore, I frame my study in terms of simply-typed and +polymorphic $\lambda$-calculi for which I give computational +interpretations in terms of contextual operational semantics and +realise using two foundational operational techniques: continuation +passing style and abstract machine semantics. When it comes to +expressivity studies there are multiple complementary notions of +expressiveness available in the literature; in this dissertation I +work with typed macro-expressiveness and type-respecting +expressiveness notions. + +\subsection{Scope extrusion} The literature on effect handlers is rich, and my dissertation is but one of many on topics related to effect handlers. In this section I provide a few pointers to related work involving effect handlers that I will not otherwise discuss in this dissertation. -Readers interested in the mathematical theory and original development -of effect handlers should consult \citeauthor{Pretnar10}'s PhD -dissertation~\cite{Pretnar10}. +Readers interested in the mathematical foundations and original +development of effect handlers should consult \citeauthor{Pretnar10}'s +PhD dissertation~\cite{Pretnar10}. + +Most programming language treatments of algebraic effects and their +handlers sideline equational theories, despite equational theories +being an important part of the original treatment of effect +handlers. \citeauthor{Ziga20}'s PhD dissertation brings equations back +onto the pitch as \citet{Ziga20} develops a core calculus with a novel +local notion of effect theories. Lexical effect handlers are a variation on \citeauthor{PlotkinP09}'s deep handlers, which provide a form of lexical scoping for effect @@ -1639,7 +1661,7 @@ operations, thus statically binding them to their handlers. % \citeauthor{Geron19}'s PhD dissertation develops the mathematical theory of scoped effect operations, whilst \citet{WuSH14} and -\citet{BiernackiPPS20} studies them from a programming perspective. +\citet{BiernackiPPS20} study them from a programming perspective. To get a grasp of the reasoning principles for effect handlers, interested readers should consult \citeauthor{McLaughlin20}'s PhD @@ -1652,20 +1674,25 @@ techniques for deep handlers due to \citet{BiernackiPPS18}. \citeauthor{Ahman17}'s PhD dissertation is relevant for readers interested in the integration of computational effects into dependent type theories~\cite{Ahman17}. \citeauthor{Ahman17} develops an -intensional \citet{MartinLof84} style effectful dependent type theory -equipped with a novel computational dependent type. - -Effect handlers were conceived in the realm of category theory to give -an algebraic treatment of exception handling~\cite{PlotkinP09}. They -were adopted early by functional programmers, who either added -language-level support for effect handlers~ +intensional \citet{MartinLof84} style dependent type theory equipped +with a novel computational dependent type, which makes it possible to +treat type-dependency in the sequential composition of effectful +computations uniformly. + +% Effect handlers were conceived in the realm of category theory to give +% an algebraic treatment of exception handling~\cite{PlotkinP09}. They +% were adopted early by functional programmers, who either added +% language-level support for effect handlers~ +Functional programmers were early adopters of effect handlers. They +either added language-level support for handlers~ \cite{Hillerstrom15,DolanWSYM15,BiernackiPPS18,Leijen17,BauerP15,BrachthauserSO20a,LindleyMM17,Chiusano20} or embedded them in libraries~\cite{KiselyovSS13,KiselyovI15,KiselyovS16,KammarLO13,BrachthauserS17,Brady13,XieL20}. Thus functional perspectives on effect handlers are plentiful in the -literature. Only a few has studied effect handlers outside the realm -of functional programming: \citet{Brachthauser20} offers an -object-oriented perspective on effect handlers; \citet{Saleh19} +literature. There are only a a few takes on effect handlers outside +functional programming: \citeauthor{Brachthauser20}'s PhD dissertation +contains an object-oriented perspective on effect handlers in +Java~\cite{Brachthauser20}; In \citeauthor{Saleh19}'s PhD dissertation provides a logic programming perspective via an effect handlers extension to Prolog; and \citet{Leijen17b} has an imperative take on effect handlers in C.