From 9ba7def07bce63a1ea2c945bab6829a1de3b30d0 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Daniel=20Hillerstr=C3=B6m?= Date: Mon, 17 May 2021 23:13:01 +0100 Subject: [PATCH] WIP --- macros.tex | 66 +++++++--- thesis.bib | 88 +++++++++++--- thesis.tex | 349 ++++++++++++++++++++++++++++++++++++++++++++--------- 3 files changed, 408 insertions(+), 95 deletions(-) diff --git a/macros.tex b/macros.tex index 53a1680..e33dae9 100644 --- a/macros.tex +++ b/macros.tex @@ -359,6 +359,9 @@ \newcommand{\getF}{\dec{get}} \newcommand{\putF}{\dec{put}} \newcommand{\fmap}{\dec{fmap}} +\newcommand{\toggle}{\dec{toggle}} +\newcommand{\incrEven}{\dec{incrEven}} +\newcommand{\even}{\dec{even}} % Abstract machine \newcommand{\cek}[1]{\ensuremath{\langle #1 \rangle}} @@ -535,24 +538,6 @@ \newcommand{\OCaml}{OCaml} -% Tikz figures -\newcommand\toggle{ -\begin{tikzpicture}[->,>=stealth',level/.style={sibling distance = 5cm/##1, - level distance = 1.5cm}] -\node [opnode] {$\Get~\Unit$} - child{ node [opnode] {$\Put~\False$} - child{ node [leaf] {$\True$} - edge from parent node[left] {$\Unit$}} - edge from parent node[above left] {$\True$} - } - child{ node [opnode] {$\Put~v$} - child{ node [leaf] {$\False$} - edge from parent node[right] {$\res{()}$}} - edge from parent node[above right] {$\res{\False}$} - } -; -\end{tikzpicture}} - %% %% Asymptotic improvement macros %% @@ -646,4 +631,47 @@ ; \end{tikzpicture}} -\newenvironment{twoeqs}{\ba[t]{@{}r@{~}c@{~}l@{~}c@{~}r@{~}c@{~}l@{}}}{\ea} \ No newline at end of file +\newenvironment{twoeqs}{\ba[t]{@{}r@{~}c@{~}l@{~}c@{~}r@{~}c@{~}l@{}}}{\ea} + +\newcommand{\compTreeEx}{ + \begin{tikzpicture}[->,>=stealth',level/.style={sibling distance = 2.0cm/##1, + level distance = 2.0cm}] +\node (root) [opnode] {$\getF$} + child { node [yshift=15] {$\dots$} + edge from parent {} + } + child { node [opnode] {$\putF$} + child { node {$\True$} + edge from parent node[left] {$\Unit$} + } + edge from parent node[yshift=5,left] {$-2$} + } + child { node [opnode] {$\putF$} + child { node {$\False$} + edge from parent node[left] {$\Unit$} + } + edge from parent node[yshift=2,left] {$-1$} + } + child { node [opnode] {$\putF$} + child { node {$\True$} + edge from parent node[left] {$\Unit$} + } + edge from parent node[left] {$0$} + } + child { node [opnode] {$\putF$} + child { node {$\False$} + edge from parent node[right] {$\Unit$} + } + edge from parent node[yshift=2,right] {$1$} + } + child { node [opnode] {$\putF$} + child { node {$\True$} + edge from parent node[right] {$\Unit$} + } + edge from parent node[yshift=5,right] {$2$} + } + child { node [yshift=15] {$\dots$} + edge from parent {} + } +; +\end{tikzpicture}} \ No newline at end of file diff --git a/thesis.bib b/thesis.bib index c9917c1..deea924 100644 --- a/thesis.bib +++ b/thesis.bib @@ -57,7 +57,7 @@ title = {Concurrent System Programming with Effect Handlers}, booktitle = {{TFP}}, OPTseries = {Lecture Notes in Computer Science}, - series = {LNCS}, + series = {{LNCS}}, volume = {10788}, pages = {98--117}, publisher = {Springer}, @@ -147,7 +147,7 @@ title = {Handlers of Algebraic Effects}, booktitle = {{ESOP}}, OPTseries = {Lecture Notes in Computer Science}, - series = {LNCS}, + series = {{LNCS}}, volume = {5502}, pages = {80--94}, publisher = {Springer}, @@ -188,7 +188,7 @@ title = {Adequacy for Algebraic Effects}, booktitle = {FoSSaCS}, OPTseries = {Lecture Notes in Computer Science}, - series = {LNCS}, + series = {{LNCS}}, volume = {2030}, pages = {1--24}, publisher = {Springer}, @@ -460,7 +460,7 @@ title = {Runners in Action}, booktitle = {{ESOP}}, OPTseries = {Lecture Notes in Computer Science}, - series = {LNCS}, + series = {{LNCS}}, volume = {12075}, pages = {29--55}, publisher = {Springer}, @@ -482,7 +482,7 @@ title = {Resource-Dependent Algebraic Effects}, booktitle = {Trends in Functional Programming}, OPTseries = {Lecture Notes in Computer Science}, - series = {LNCS}, + series = {{LNCS}}, volume = {8843}, pages = {18--33}, publisher = {Springer}, @@ -673,7 +673,7 @@ title = {Fusion for Free - Efficient Algebraic Effect Handlers}, booktitle = {{MPC}}, OPTseries = {Lecture Notes in Computer Science}, - series = {LNCS}, + series = {{LNCS}}, volume = {9129}, pages = {302--322}, publisher = {Springer}, @@ -712,7 +712,7 @@ title = {Links: Web Programming Without Tiers}, booktitle = {{FMCO}}, OPTseries = {Lecture Notes in Computer Science}, - series = {LNCS}, + series = {{LNCS}}, volume = {4709}, pages = {266--296}, publisher = {Springer}, @@ -793,7 +793,7 @@ title = {Monads for Functional Programming}, booktitle = {Advanced Functional Programming}, OPTseries = {Lecture Notes in Computer Science}, - series = {LNCS}, + series = {{LNCS}}, volume = {925}, pages = {24--52}, publisher = {Springer}, @@ -810,6 +810,18 @@ year = {2008} } +@inproceedings{Gibbons12, + author = {Jeremy Gibbons}, + title = {Unifying Theories of Programming with Monads}, + booktitle = {{UTP}}, + OPTseries = {Lecture Notes in Computer Science}, + series = {{LNCS}}, + volume = {7681}, + pages = {23--67}, + publisher = {Springer}, + year = {2012} +} + @inproceedings{PauwelsSM19, author = {Koen Pauwels and Tom Schrijvers and @@ -817,7 +829,7 @@ title = {Handling Local State with Global State}, booktitle = {{MPC}}, OPTseries = {Lecture Notes in Computer Science}, - series = {LNCS}, + series = {{LNCS}}, volume = {11825}, pages = {18--44}, publisher = {Springer}, @@ -834,6 +846,30 @@ year = {2011} } +@book{Borceux94, + author = {Francis Borceux}, + title = {Handbook of Categorical Algebra}, + series = {Encyclopedia of Mathematics and its Applications}, + volume = {1}, + collection= {Encyclopedia of Mathematics and its Applications}, + OPTdoi = {10.1017/CBO9780511525858}, + publisher = {Cambridge University Press}, + year = 1994, + place = {Cambridge} +} + +@book{MacLane71, + author = {Saunders MacLane}, + title = {Categories for the Working Mathematician}, + series = {Graduate Texts in Mathematics, Vol. 5}, + pages = {ix+262}, + publisher = {Springer-Verlag}, + address = {New York}, + year = 1971 +} + + + # Hop.js @inproceedings{SerranoP16, author = {Manuel Serrano and @@ -916,7 +952,7 @@ Mitchell Wand}, title = {Continuation Semantics in Typed Lambda-Calculi (Summary)}, booktitle = {Logic of Programs}, - series = {LNCS}, + series = {{LNCS}}, volume = {193}, pages = {219--224}, publisher = {Springer}, @@ -1019,7 +1055,7 @@ title = {A Dynamic Interpretation of the {CPS} Hierarchy}, booktitle = {{APLAS}}, OPTseries = {Lecture Notes in Computer Science}, - series = {LNCS}, + series = {{LNCS}}, volume = {7705}, pages = {296--311}, publisher = {Springer}, @@ -1147,7 +1183,7 @@ title = {Shallow Effect Handlers}, booktitle = {{APLAS}}, OPTseries = {Lecture Notes in Computer Science}, - series = {LNCS}, + series = {{LNCS}}, volume = {11275}, pages = {415--435}, publisher = {Springer}, @@ -1258,7 +1294,7 @@ title = {Explicit Effect Subtyping}, booktitle = {{ESOP}}, OPTseries = {Lecture Notes in Computer Science}, - series = {LNCS}, + series = {{LNCS}}, volume = {10801}, pages = {327--354}, publisher = {Springer}, @@ -1858,7 +1894,7 @@ title = {Towards a theory of type structure}, booktitle = {Symposium on Programming}, OPTseries = {Lecture Notes in Computer Science}, - series = {LNCS}, + series = {{LNCS}}, volume = {19}, pages = {408--423}, publisher = {Springer}, @@ -1945,7 +1981,7 @@ title = {On the Expressive Power of Programming Languages}, booktitle = {{ESOP}}, OPTseries = {Lecture Notes in Computer Science}, - series = {LNCS}, + series = {{LNCS}}, volume = {432}, pages = {134--151}, publisher = {Springer}, @@ -1988,7 +2024,7 @@ Type}, booktitle = {CiE}, OPTseries = {Lecture Notes in Computer Science}, - series = {LNCS}, + series = {{LNCS}}, volume = {5028}, pages = {389--402}, publisher = {Springer}, @@ -2188,7 +2224,7 @@ title = {The Essence of Multitasking}, booktitle = {{AMAST}}, OPTseries = {Lecture Notes in Computer Science}, - series = {LNCS}, + series = {{LNCS}}, volume = {4019}, pages = {158--172}, publisher = {Springer}, @@ -2977,7 +3013,8 @@ author = {Alex K. Simpson}, title = {Lazy Functional Algorithms for Exact Real Functionals}, booktitle = {{MFCS}}, - series = {Lecture Notes in Computer Science}, + OPTseries = {Lecture Notes in Computer Science}, + series = {{LNCS}}, volume = {1450}, pages = {456--464}, publisher = {Springer}, @@ -3174,7 +3211,8 @@ Dmitry Lomov}, title = {The F{\#} Asynchronous Programming Model}, booktitle = {{PADL}}, - series = {Lecture Notes in Computer Science}, + OPTseries = {Lecture Notes in Computer Science}, + series = {{LNCS}}, volume = {6539}, pages = {175--189}, publisher = {Springer}, @@ -3197,4 +3235,16 @@ year = 1954, language = {eng}, keywords = {Fiction}, +} + +# Correspondence between monadic effects and effect systems +@article{WadlerT03, + author = {Philip Wadler and + Peter Thiemann}, + title = {The marriage of effects and monads}, + journal = {{ACM} Trans. Comput. Log.}, + volume = {4}, + number = {1}, + pages = {1--32}, + year = {2003} } \ No newline at end of file diff --git a/thesis.tex b/thesis.tex index 8966395..3fc2f2b 100644 --- a/thesis.tex +++ b/thesis.tex @@ -388,6 +388,11 @@ Evidently, control is a pervasive phenomenon in programming. However, not every control phenomenon is equal in terms of programmability and expressiveness. +\section{This thesis in a nutshell} +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. + \section{Why first-class control matters} \subsection{Flavours of control} @@ -399,22 +404,45 @@ expressiveness. \section{State of effectful programming} -\subsection{Dark age of impurity} +The evolution of effectful programming has gone through several +characteristic phases. In this section I will provide a brief overview +of how effectful programming has evolved as well as providing a brief +introduction to the core concepts concerned with each phase. + +\subsection{Early days of direct-style} -\subsection{Monadic enlightenment} +\subsection{Monadic epoch} During the late 80s and early 90s monads rose to prominence as a -practical program structuring idiom for effectful -programming. Notably, they form the foundations for effectful -programming in Haskell, which adds special language-level support for -programming with monads~\cite{JonesABBBFHHHHJJLMPRRW99}. +practical programming idiom for structuring effectful +programming~\cite{Moggi89,Moggi91,Wadler92,Wadler92b,JonesW93,Wadler95,JonesABBBFHHHHJJLMPRRW99}. +% +The concept of monad has its origins in category theory and its +mathematical nature is well-understood~\cite{MacLane71,Borceux94}. The +emergence of monads as a programming abstraction began when +\citet{Moggi89,Moggi91} proposed to use monads as the basis for +denoting computational effects in denotational semantics such as +exceptions, state, nondeterminism, interactive input and +output. \citet{Wadler92,Wadler95} popularised monadic programming by +putting \citeauthor{Moggi89}'s proposal to use in functional +programming by demonstrating how monads increase the ease at which +programs may be retrofitted with computational effects. +% +In practical programming terms, monads may be thought of as +constituting a family of design patterns, where each pattern gives +rise to a distinct effect with its own operations. +% +% Notably, they form the foundations for effectful programming in +% Haskell, which adds special language-level support for programming +% with monads~\cite{JonesABBBFHHHHJJLMPRRW99}. % \begin{definition} - A monad is a triple $(T, \Return, \bind)$ where $T$ is some unary - type constructor, $\Return$ is an operation that lifts an arbitrary - value into the monad (sometimes this operation is called `the unit - operation'), and $\bind$ is an application operator the monad (this - operator is pronounced `bind'). Implementations of $\Return$ and - $\bind$ must conform to the following interface. + A monad is a triple $(T^{\TypeCat \to \TypeCat}, \Return, \bind)$ + where $T$ is some unary type constructor, $\Return$ is an operation + that lifts an arbitrary value into the monad (sometimes this + operation is called `the unit operation'), and $\bind$ is the + application operator of the monad (this operator is pronounced + `bind'). Adequate implementations of $\Return$ and $\bind$ must + conform to the following interface. % \[ \bl @@ -431,43 +459,155 @@ programming with monads~\cite{JonesABBBFHHHHJJLMPRRW99}. \end{reductions} \end{definition} % -Monads have given rise to various popular control-oriented programming -abstractions, e.g. the async/await idiom has its origins in monadic +Monads have a proven track record of successful applications. + +Monads have also given rise to various popular control-oriented +programming abstractions, e.g. the asynchronous programming idiom +async/await has its origins in monadic programming~\cite{Claessen99,LiZ07,SymePL11}. -\subsection{Option monad} -The $\Option$ type is a unary type constructor with two data -constructors, i.e. $\Option~A \defas [\Some:A|\None]$. +% \subsection{Option monad} +% The $\Option$ type is a unary type constructor with two data +% constructors, i.e. $\Option~A \defas [\Some:A|\None]$. -\begin{definition} The option monad is a monad equipped with a single - failure operation. +% \begin{definition} The option monad is a monad equipped with a single +% failure operation. +% % +% \[ +% \ba{@{~}l@{\qquad}@{~}r} +% \multicolumn{2}{l}{T~A \defas \Option~A} \smallskip\\ +% \multirow{2}{*}{ +% \bl +% \Return : A \to T~A\\ +% \Return \defas \lambda x.\Some~x +% \el} & +% \multirow{2}{*}{ +% \bl +% \bind ~: T~A \to (A \to T~B) \to T~B\\ +% \bind ~\defas \lambda m.\lambda k.\Case\;m\;\{\None \mapsto \None;\Some~x \mapsto k~x\} +% \el}\\ & \smallskip\\ +% \multicolumn{2}{l}{ +% \bl +% \fail : A \to T~A\\ +% \fail \defas \lambda x.\None +% \el} +% \ea +% \] +% % +% \end{definition} + +\subsubsection{State monad} +% +The state monad provides a way to encapsulate a state cell. +% +\begin{definition} + The state monad is defined over some fixed state type $S$. % \[ - \ba{@{~}l@{\qquad}@{~}r} - \multicolumn{2}{l}{T~A \defas \Option~A} \smallskip\\ + \ba{@{~}l@{\qquad\quad}@{~}r} + \multicolumn{2}{l}{T~A \defas S \to A \times S} \smallskip\\ \multirow{2}{*}{ \bl \Return : A \to T~A\\ - \Return \defas \lambda x.\Some~x + \Return~x\defas \lambda st.\Record{x;st} \el} & \multirow{2}{*}{ \bl \bind ~: T~A \to (A \to T~B) \to T~B\\ - \bind ~\defas \lambda m.\lambda k.\Case\;m\;\{\None \mapsto \None;\Some~x \mapsto k~x\} - \el}\\ & \smallskip\\ - \multicolumn{2}{l}{ - \bl - \fail : A \to T~A\\ - \fail \defas \lambda x.\None - \el} + \bind ~\defas \lambda m.\lambda k.\lambda st. \Let\;\Record{x;st'} = m~st\;\In\; (k~x)~st' + \el} \\ & % space hack to avoid the next paragraph from + % floating into the math environment. + \ea + \] + % + The $\Return$ of the monad is a state-accepting function of type + $S \to A \times S$ that returns its first argument paired with the + current state. The bind operator also produces a state-accepting + function of type $S \to A \times S$. The bind operator first + supplies the current state $st$ to the monad argument $m$. This + application yields a value result of type $A$ and an updated state + $st'$. The result is supplied to the continuation $k$, which + produces another state accepting function that gets applied to the + previously computed state value $st'$. + + The state monad is equipped with two dual operations for accessing + and modifying the state encapsulated within the monad. + % + \[ + \ba{@{~}l@{\qquad\quad}@{~}r} + \multirow{2}{*}{ + \bl + \getF : \UnitType \to T~S\\ + \getF~\Unit \defas \lambda st. \Record{st;st} + \el} & + \multirow{2}{*}{ + \bl + \putF : S \to T~\UnitType\\ + \putF~st \defas \lambda st'.\Record{\Unit;st} + \el} \\ & % space hack to avoid the next paragraph from + % floating into the math environment. \ea \] % + Interactions between the two operations satisfy the following + equations~\cite{Gibbons12}. + % + \begin{reductions} + \slab{Get\textrm{-}put} & \getF\,\Unit \bind (\lambda st.\putF~st) &=& \Return\;\Unit\\ + \slab{Put\textrm{-}put} & \putF~st \bind (\lambda st.\putF~st') &=& \putF~st'\\ + \slab{Put\textrm{-}get} & \putF~st \bind (\lambda\Unit.\getF\,\Unit) &=& \putF~st \bind (\lambda \Unit.\Return\;st) + \end{reductions} + % + The first equation captures the intuition that getting a value and + then putting has no observable effect on the state cell. The second + equation states that only the latter of two consecutive puts is + observable. The third equation states that performing a get + immediately after putting a value is equivalent to returning that + value. \end{definition} -\subsection{State monad} +The literature often presents the state monad with a fourth equation, +which states that $\getF$ is idempotent. However, this equation is +redundant as it is derivable from the first and third equations. -\subsection{Continuation monad} +The following bit toggling function illustrates a use of the state +monad. +% +\[ + \bl + T~A \defas \Int \to (A \times \Int)\smallskip\\ + \incrEven : \UnitType \to T~\Bool\\ + \incrEven~\Unit \defas \getF + \bind (\lambda st. + \putF\,(1+st) + \bind \lambda\Unit. \Return\;(\even~st))) + \el +\] +% +We fix the state type of our monad to be the integer type. The type +signature of the function $\incrEven$ may be read as describing a +thunk that returns a boolean value, and whilst computing this boolean +value the function may perform any effectful operations given by the +monad $T$~\cite{Moggi91,Wadler92}, i.e. $\getF$ and +$\putF$. Operationally, the function retrieves the current value of +the state cell via the invocation of $\getF$. The bind operator passes +this value onto the continuation, which increments the value and +invokes $\putF$. The continuation applies a predicate +$\even : \Int \to \Bool$ to the original state value to test whether +its parity is even. The structure of the monad means that the result +of running this computation gives us a pair consisting of boolean +value indicating whether the initial state was even and the final +state value. For instance, if the initial state value is $\True$, then +the computation yields +% +\[ + \incrEven~\Unit~4 \reducesto^+ \Record{\True;5}, +\] +% +where the first component contains the initial state value and the +second component contains the final state value. + +\subsubsection{Continuation monad} As in J.R.R. Tolkien's fictitious Middle-earth~\cite{Tolkien54} there exists one monad to rule them all, one monad to realise them, one monad to subsume them all, and in the term language bind them. This @@ -483,7 +623,7 @@ powerful monad is the \emph{continuation monad}. \multirow{2}{*}{ \bl \Return : A \to T~A\\ - \Return \defas \lambda x.\lambda k.k~x + \Return~x\defas \lambda k.k~x \el} & \multirow{2}{*}{ \bl @@ -502,26 +642,78 @@ $m$ to an anonymous function that accepts a value $x$ of type $A$. This value $x$ is supplied to the immediate continuation $k$ alongside the current continuation $f$. -Scheme's undelimited control operator $\Callcc$ is definable as a -monadic operation on the continuation monad~\cite{Wadler92}. +If we instantiate $R = S \to A \times S$ for some type $S$ then we +can implement the state monad inside the continuation monad. % \[ - \bl - \Callcc : ((A \to T~B) \to T~A) \to T~A\\ - \Callcc \defas \lambda f.\lambda k. f\,(\lambda x.\lambda.k'.k~x)~k - \el + \ba{@{~}l@{\qquad\quad}@{~}r} + \multirow{2}{*}{ + \bl + \getF : \UnitType \to T~S\\ + \getF~\Unit \defas \lambda k.\lambda st.k~st~st + \el} & + \multirow{2}{*}{ + \bl + \putF : S \to T~\UnitType\\ + \putF~st \defas \lambda k.\lambda st'.k~\Unit~st + \el} \\ & % space hack to avoid the next paragraph from + % floating into the math environment. + \ea \] +% +The $\getF$ operation takes as input a (binary) continuation $k$ of +type $S \to S \to A \times S$ and produces a state-accepting function +that applies the continuation to the given state $st$. The first +occurrence of $st$ is accessible to the caller of $\getF$, whilst the +second occurrence passes the value $st$ onto the next operation +invocation on the monad. The operation $\putF$ works in the same +way. The primary difference is that $\putF$ does not return the value +of the state cell; instead it returns simply the unit value $\Unit$. +% +Using this continuation monad we can interpret $\incrEven$. +% +\[ + \incrEven~\Unit~(\lambda x.\lambda st. \Record{x;st})~4 \reducesto^+ \Record{\True;5} +\] +% +The initial continuation $(\lambda x.\lambda st. \Record{x;st})$ +corresponds to the $\Return$ of the state monad. -\subsection{Free monad} +% Scheme's undelimited control operator $\Callcc$ is definable as a +% monadic operation on the continuation monad~\cite{Wadler92}. +% % +% \[ +% \bl +% \Callcc : ((A \to T~B) \to T~A) \to T~A\\ +% \Callcc \defas \lambda f.\lambda k. f\,(\lambda x.\lambda.k'.k~x)~k +% \el +% \] + +\subsubsection{Free monad} +% +\begin{figure} + \centering + \compTreeEx + \caption{Computation tree for $\incrEven$.}\label{fig:comptree} +\end{figure} +% Just like other monads the free monad satisfies the monad laws, however, unlike other monads the free monad does not perform any computation \emph{per se}. Instead the free monad builds an abstract representation of the computation in form of a computation tree, whose interior nodes correspond to an invocation of some operation on the monad, where each outgoing edge correspond to a possible continuation -of the operation; the leaves correspond to return values. The meaning -of a free monadic computation is ascribed by a separate function, or -interpreter, that traverses the computation tree. +of the operation; the leaves correspond to return +values. Figure~\ref{fig:comptree} depicts the computation tree for the +$\incrEven$ function. This particular computation tree has infinite +width, because the operation $\getF$ has infinitely many possible +continuations (we take the denotation of $\Int$ to be +$\mathbb{Z}$). Contrary, each $\putF$ node has only one outgoing edge, +because $\putF$ has only a single possible continuation, namely, the +trivial continuation $\Unit$. + +The meaning of a free monadic computation is ascribed by a separate +function, or interpreter, that traverses the computation tree. The shape of computation trees is captured by the following generic type definition. @@ -549,11 +741,23 @@ operation is another computation tree node. % \[ \bl - T~A \defas \Free~F~A \smallskip\\ - \Return : A \to T~A\\ - \Return \defas \lambda x.\return~x\\ - \bind ~: T~A \to (A \to T~B) \to T~B\\ - \bind ~\defas \lambda m.\lambda k.\Case\;m\;\{\return~x \mapsto k~x;\OpF~y \mapsto \OpF\,(\fmap\,(\lambda m'. m' \bind k)\,y)\} + \ba{@{~}l@{\qquad}@{~}r} + \multicolumn{2}{l}{T~A \defas \Free~F~A} \smallskip\\ + \multirow{2}{*}{ + \bl + \Return : A \to T~A\\ + \Return~x \defas \return~x + \el} & + \multirow{2}{*}{ + \bl + \bind ~: T~A \to (A \to T~B) \to T~B\\ + \bind ~\defas \lambda m.\lambda k.\Case\;m\;\{ + \bl + \return~x \mapsto k~x;\\ + \OpF~y \mapsto \OpF\,(\fmap\,(\lambda m'. m' \bind k)\,y)\} + \el + \el}\\ & \\ & + \ea \el \] % @@ -563,7 +767,7 @@ operation is another computation tree node. \[ \bl \DoF : F~A \to \Free~F~A\\ - \DoF \defas \lambda op.\OpF\,(\fmap\,(\lambda x.\return~x)\,op) + \DoF~op \defas \OpF\,(\fmap\,(\lambda x.\return~x)\,op) \el \] % @@ -571,21 +775,52 @@ operation is another computation tree node. \[ \bl - \dec{FreeState}~S~R \defas [\Get:S \to R|\Put:\Record{S;R}|\Done] \smallskip\\ + \dec{FreeState}~S~R \defas [\Get:S \to R|\Put:\Record{S;R}] \smallskip\\ \fmap~f~x \defas \Case\;x\;\{ \bl \Get~k \mapsto \Get\,(\lambda st.f\,(k~st));\\ - \Put~st'~k \mapsto \Put\,\Record{st';f~k};\\ - \Done \mapsto \Done\} - \el \smallskip\\ - \getF : \UnitType \to T~S\\ - \getF~\Unit \defas \DoF~(\Get\,(\lambda x.x)))\\ - \putF : S \to T~\UnitType\\ - \putF~st \defas \DoF~(\Put\,\Record{st;\Unit}) + \Put~st'~k \mapsto \Put\,\Record{st';f~k}\} + \el \el \] +% +\[ + \ba{@{~}l@{\qquad\quad}@{~}r} + \multirow{2}{*}{ + \bl + \getF : \UnitType \to T~S\\ + \getF~\Unit \defas \DoF~(\Get\,(\lambda x.x)) + \el} & + \multirow{2}{*}{ + \bl + \putF : S \to T~\UnitType\\ + \putF~st \defas \DoF~(\Put\,\Record{st;\Unit}) + \el} \\ & % space hack to avoid the next paragraph from + % floating into the math environment. + \ea +\] +% +\[ + \bl + \runState : S \to \Free\,(\dec{FreeState}~S)\,A \to A \times S\\ + \runState~st~m \defas + \Case\;m\;\{ + \ba[t]{@{~}l@{~}c@{~}l} + \return~x &\mapsto& (x, st);\\ + \OpF\,(\Get~k) &\mapsto& \runState~st~(k~st);\\ + \OpF\,(\Put\,\Record{st';k}) &\mapsto& \runState~st'~k + \}\ea + \el +\] +% +\[ + \runState~4~(\incrEven~\Unit) \reducesto^+ \Record{\True;5} +\] + +\subsection{Back to direct-style} + -\subsection{Direct-style revolution} +\subsubsection{Effect tracking} \section{Contributions}