From 1945a7307cbcedb064cf17daaacf8a6e98dd08fa Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Daniel=20Hillerstr=C3=B6m?= Date: Sun, 23 May 2021 14:12:35 +0100 Subject: [PATCH] Yallop's thesis --- thesis.bib | 8 ++++++++ thesis.tex | 36 ++++++++++++++++++++++++++---------- 2 files changed, 34 insertions(+), 10 deletions(-) diff --git a/thesis.bib b/thesis.bib index 6ddf654..044c28b 100644 --- a/thesis.bib +++ b/thesis.bib @@ -3483,4 +3483,12 @@ title = {Applications of algebraic effect theories}, school = {University of Ljubljana, Slovenia}, year = {2020} +} + +# Jeremy Yallop's phd thesis +@phdthesis{Yallop10, + author = {Jeremy Yallop}, + title = {Abstraction for web programming}, + school = {The University of Edinburgh, {UK}}, + year = {2010} } \ No newline at end of file diff --git a/thesis.tex b/thesis.tex index bc83b43..4204fc6 100644 --- a/thesis.tex +++ b/thesis.tex @@ -1330,9 +1330,25 @@ effect handlers. \dhil{The problem with monads is that they do not compose. Cite~\citet{Espinosa95}, \citet{VazouL16} \citet{McBrideP08}} % -Another problem is that monads break the basic doctrine of modular -abstraction, which we should program against an abstract interface, -not an implementation. A monad is a concrete implementation. +The inherent problems with monads is that they break the basic +doctrine of modular abstraction, which says we should program against +an abstract interface, not an implementation. A monad is a concrete +implementation. Monadic effect operations are intimately tied to the +concrete monad structure. + +It is worth mentioning \citeauthor{McBrideP08}'s idioms (known as +applicative functors in Haskell) as an alternative to monadic +programming~\cite{McBrideP08}. Idioms provide an applicative style for +programming with effects. Even though idioms are computationally +weaker than monads, they are still capable of simulating a wide range +of computational effects whose realisation do not require the full +monad structure (consult \citet{Yallop10} for a technical analysis of +idioms and monads). + +We will wrap up this crash course in effectful programming by looking +at two techniques for programming in direct-style with effects that +make use of delimited control before finishing with a brief discussion +of effect tracking. \subsubsection{Monadic reflection on state} % @@ -1586,16 +1602,16 @@ A benefit of using monads for effectful programming is that we get effect tracking `for free' (some might object to this statement and claim we paid for it by having to program in monadic style). Effect tracking is a useful tool for making programming with effects less -prone to error in much the same way a static type system is useful -detecting a wide range of potential runtime errors at compile -time. +prone to error in much the same way a static type system is useful for +detecting a wide range of potential runtime errors at compile time. The principal idea of an effect system is to annotate computation types with the collection of effects that their inhabitants are -allowed to perform, e.g. the type $A \to B \eff E$ denotes a function -that accepts a value of type $A$ as input and ultimately returns a -value of type $B$. As it computes the $B$ value it is allowed to use -the operations given by the effect signature $E$. +allowed to perform, e.g. the type $A \to B \eff E$ is inhabited by +functions that accept a value of type $A$ as input and ultimately +return a value of type $B$. As an inhabitant computes the $B$ value it +is allowed to perform the effect operations mentioned by the effect +signature $E$. This typing discipline fits nicely with the effect handlers-style of programming. The $\Do$ construct provides a mechanism for injecting an