From a3273afa5062b46e8d6c6f636a7f9756b7f23076 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Daniel=20Hillerstr=C3=B6m?= Date: Sun, 23 May 2021 15:33:28 +0100 Subject: [PATCH] Combining monads --- thesis.bib | 11 +++++++++ thesis.tex | 68 ++++++++++++++++++++++++++++++++---------------------- 2 files changed, 52 insertions(+), 27 deletions(-) diff --git a/thesis.bib b/thesis.bib index 044c28b..40fddc4 100644 --- a/thesis.bib +++ b/thesis.bib @@ -802,6 +802,17 @@ year = {1992} } +@inproceedings{KingW92, + author = {David J. King and + Philip Wadler}, + title = {Combining Monads}, + booktitle = {Functional Programming}, + series = {Workshops in Computing}, + pages = {134--143}, + publisher = {Springer}, + year = {1992} +} + @inproceedings{JonesW93, author = {Simon L. Peyton Jones and Philip Wadler}, diff --git a/thesis.tex b/thesis.tex index 4204fc6..965db4b 100644 --- a/thesis.tex +++ b/thesis.tex @@ -1327,28 +1327,42 @@ The free monad brings us close to the essence of programming with effect handlers. \subsection{Back to direct-style} -\dhil{The problem with monads is that they do not - compose. Cite~\citet{Espinosa95}, \citet{VazouL16} \citet{McBrideP08}} -% -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 +Monads do not freely compose, because monads must satisfy a +distributive property in order to combine~\cite{KingW92}. Alas, not +every monad has a distributive property. +% +The lack of composition is to an extent remedied by monad +transformers, which provide a programmatic abstraction for stacking +one monad on top of another~\cite{Espinosa95}. The problem with monad +transformers is that they enforce an ordering on effects that affects +the program semantics (c.f. my MSc dissertation for a concrete example +of this~\cite{Hillerstrom15}). + +However, a more fundamental problem with monads is that they break the +basic doctrine of modular abstraction, which says we should program +against an abstract interface, not an implementation. Effectful +programming using monads fixates on the concrete structure first, and +adds effect operations second. As a result monadic effect operations +are intimately tied to the concrete structure of their monad. + +Before moving onto direct-style alternatives, 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. +weaker than monads, they are still capable of encapsulating 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). Another thing worth pointing out is +that it is possible to have a direct-style interface for effectful +programming in the source language, which the compiler can translate +into monadic binds and returns automatically. For a concrete example +of this see the work of \citet{VazouL16}. + +Let us wrap up this crash course in effectful programming by looking +at two approaches for programming in direct-style with effects that +make structured use of delimited control, before finishing with a +brief discussion of effect tracking. \subsubsection{Monadic reflection on state} % @@ -1605,13 +1619,13 @@ 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 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$ 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$. +The principal idea of a \citet{LucassenG88} style 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$ 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