diff --git a/sofp-src/sofp-transformers.lyx b/sofp-src/sofp-transformers.lyx index dc0b89544..f710f0d33 100644 --- a/sofp-src/sofp-transformers.lyx +++ b/sofp-src/sofp-transformers.lyx @@ -11991,24 +11991,25 @@ set \end_inset -A -\begin_inset listings -inline true -status open -\begin_layout Plain Layout - -State \end_layout -\end_inset +\begin_layout Standard +\begin_inset Wrap figure +lines 0 +placement l +overhang 0in +width "43col%" +status open --monadic program can then be written without referring to the type signature - -\begin_inset Formula $S\rightarrow A\times S$ +\begin_layout Plain Layout +\begin_inset VSpace -100baselineskip% \end_inset -: + +\end_layout + +\begin_layout Plain Layout \begin_inset listings inline false status open @@ -12040,7 +12041,38 @@ val program: State[S, A] = for { \end_inset -The two functions + +\begin_inset VSpace -80baselineskip% +\end_inset + + +\end_layout + +\end_inset + + +\end_layout + +\begin_layout Standard +A +\begin_inset listings +inline true +status open + +\begin_layout Plain Layout + +State +\end_layout + +\end_inset + +-monadic program can then be written as shown at left, without referring + to the type signature +\begin_inset Formula $S\rightarrow A\times S$ +\end_inset + +. + The two functions \begin_inset listings inline true status open @@ -12064,8 +12096,9 @@ set \end_inset - are sufficient to manipulate the internal state in an arbitrary way. - So, these two functions are the + appear to be sufficient to manipulate the internal state in an arbitrary + way. + So, we regard these two functions as the \begin_inset Quotes eld \end_inset @@ -12150,7 +12183,15 @@ pure \begin_inset Formula $q:\text{State}^{S,A}$ \end_inset - and define + and define functions +\begin_inset Formula $f_{1}$ +\end_inset + + and +\begin_inset Formula $f_{2}$ +\end_inset + + by \begin_inset Formula \[ f_{1}:S\rightarrow A\triangleq q\bef\pi_{1}\quad,\quad\quad f_{2}:S\rightarrow S\triangleq q\bef\pi_{2}\quad. @@ -12212,6 +12253,24 @@ set \end_inset : +\end_layout + +\begin_layout Standard +\begin_inset Wrap figure +lines 0 +placement l +overhang 0in +width "35col%" +status open + +\begin_layout Plain Layout +\begin_inset VSpace -60baselineskip% +\end_inset + + +\end_layout + +\begin_layout Plain Layout \begin_inset listings inline false status open @@ -12244,6 +12303,26 @@ q == for { \end_inset +\begin_inset VSpace 40baselineskip% +\end_inset + + +\end_layout + +\end_inset + + +\end_layout + +\begin_layout Standard +\begin_inset space ~ +\end_inset + + +\begin_inset VSpace -90baselineskip% +\end_inset + + \begin_inset Formula \[ q=\text{get}\triangleright\text{flm}_{\text{State}}\big(s_{1}\rightarrow f_{2}(s_{1})\triangleright\text{set}\triangleright(\_\rightarrow f_{1}(s_{1}))^{\uparrow\text{State}}\big)\quad. @@ -12251,6 +12330,10 @@ q=\text{get}\triangleright\text{flm}_{\text{State}}\big(s_{1}\rightarrow f_{2}(s \end_inset + +\end_layout + +\begin_layout Standard We may refactor any \begin_inset listings inline true @@ -13201,18 +13284,19 @@ status open \begin_layout Plain Layout -implicit def stateTMonadOps[S, Q[_]](implicit monadQ: Monad[Q]): StateMonadOps[S -tateT[Q, S, *], S] = new StateMonadOps[StateT[Q, S, *], S] { +implicit def stateTMonadOps[S, Q[_]: Monad] = new StateMonadOps[StateT[Q, + S, *], S] { \end_layout \begin_layout Plain Layout - def get: StateT[Q, S, S] = StateT(s => monadQ.pure((s, s))) + def get: StateT[Q, S, S] = StateT(s => implicitly[Monad[Q]].pure((s, s))) \end_layout \begin_layout Plain Layout - def set: S => StateT[Q, S, Unit] = s => StateT(_ => monadQ.pure(((), s))) + def set: S => StateT[Q, S, Unit] = s => StateT(_ => implicitly[Monad[Q]].pure(( +(), s))) \end_layout \begin_layout Plain Layout @@ -13263,7 +13347,7 @@ OtherT \end_inset . - By the inductive assumption, we already have a typeclass instance of + By the inductive assumption, we already have a \begin_inset listings inline true status open @@ -13275,7 +13359,7 @@ StateMonadOps \end_inset - for the monad + typeclass instance for the monad \begin_inset listings inline true status open @@ -13379,95 +13463,16 @@ literal "false" \end_layout \begin_layout Standard -While the MTL style provides automatic lifting with somewhat less code than - the direct approach of lifting relation (as developed in the previous section), - several problems remain. - The first problem is the large number of typeclass instances that the libraries - need to maintain. - As we have seen in the example with -\begin_inset listings -inline true -status open - -\begin_layout Plain Layout - -StateMonadOps -\end_layout - -\end_inset - -, just two implicit functions per monad type are in principle sufficient - to define the operation typeclasses for all monad stacks. - So, the length of library code is linear in the number of supported monad - types. - However, for reasons of run-time efficiency, libraries sometimes provide - typeclass instances for many specific combination of monads (say, -\begin_inset listings -inline true -status open - -\begin_layout Plain Layout - -Reader -\end_layout - -\end_inset - - with -\begin_inset listings -inline true -status open - -\begin_layout Plain Layout - -State -\end_layout - -\end_inset - -, -\begin_inset listings -inline true -status open - -\begin_layout Plain Layout - -Either -\end_layout - -\end_inset - - with -\begin_inset listings -inline true -status open - -\begin_layout Plain Layout - -Reader -\end_layout - -\end_inset - -, and so on). - This makes the required number of typeclass instances quadratic in the - number of supported monads. - For this reason, libraries such as -\family typewriter -cats-mtl -\family default - support only a limited number of most frequently used monads. - Adding a new monad to -\family typewriter -cats-mtl -\family default - would require adding a large number of new typeclass implementations. +While the MTL style does provide automatic lifting and requires somewhat + shorter code than the direct approach of lifting relation (as developed + in the previous section), some problems remain. + \end_layout \begin_layout Standard -The second problem is the lack of standard conventions for the effectful - operations. - We have seen that two operations ( +The first problem is the lack of standard conventions or principles for + the choice of effectful operations. + We have seen that the operations \begin_inset listings inline true status open @@ -13491,7 +13496,7 @@ set \end_inset -) are sufficient, in principle, to express any + are sufficient to express any \begin_inset listings inline true status open @@ -13505,83 +13510,6 @@ State -monadic programs. However, it may not be adequate to write code just with those two operations. - For example, suppose a program needs to -\emph on -update -\emph default - the state using a given function of type -\begin_inset Formula $S\rightarrow S$ -\end_inset - -. - An update is equivalent to -\begin_inset listings -inline true -status open - -\begin_layout Plain Layout - -get -\end_layout - -\end_inset - -ting the previous value and immediately -\begin_inset listings -inline true -status open - -\begin_layout Plain Layout - -set -\end_layout - -\end_inset - -ting a new value. - But a program may be required to handle certain state updates in a special - way. - Examples are updates required to be atomic in a concurrent program; updates - wrapped in a database transaction; or updates that must be run on a specially - designated processing thread (such as, the GUI thread that drives the user - interface events). - Special handling of updates cannot be implemented through -\begin_inset listings -inline true -status open - -\begin_layout Plain Layout - -get -\end_layout - -\end_inset - - and -\begin_inset listings -inline true -status open - -\begin_layout Plain Layout - -set -\end_layout - -\end_inset - -; a new effectful operation ( -\begin_inset listings -inline true -status open - -\begin_layout Plain Layout - -update -\end_layout - -\end_inset - -) must be provided to the programmer. \end_layout @@ -13919,6 +13847,86 @@ name "tab:Known-operations-for-some-monads" \begin_layout Standard \noindent +As an example, consider +\emph on +updating +\emph default + the state using a given function of type +\begin_inset Formula $S\rightarrow S$ +\end_inset + +. + In theory, updating is equivalent to +\begin_inset listings +inline true +status open + +\begin_layout Plain Layout + +get +\end_layout + +\end_inset + +ting the previous value and immediately +\begin_inset listings +inline true +status open + +\begin_layout Plain Layout + +set +\end_layout + +\end_inset + +ting a new value. + But a program may be required to handle certain state updates in a special + way. + Examples are updates required to be atomic in a concurrent program; updates + wrapped in a database transaction; or updates that must be run on a specially + designated processing thread (such as, the GUI thread that drives the user + interface events). + Special handling of updates cannot be implemented through +\begin_inset listings +inline true +status open + +\begin_layout Plain Layout + +get +\end_layout + +\end_inset + + and +\begin_inset listings +inline true +status open + +\begin_layout Plain Layout + +set +\end_layout + +\end_inset + +; a new effectful operation ( +\begin_inset listings +inline true +status open + +\begin_layout Plain Layout + +update +\end_layout + +\end_inset + +) must be provided to the programmer. +\end_layout + +\begin_layout Standard Table \begin_inset space ~ \end_inset @@ -13938,11 +13946,11 @@ noprefix "false" status open \begin_layout Plain Layout -The table was compiled using the +Operations were taken from the \family typewriter cats-mtl \family default - documentation and the paper + documentation and the papers \begin_inset Quotes eld \end_inset @@ -13966,8 +13974,7 @@ literal "false" \family default -). - In the paper +) and \begin_inset Quotes eld \end_inset @@ -13991,22 +13998,7 @@ literal "false" \family default -), M. -\begin_inset space ~ -\end_inset - - -\begin_inset Index idx -status collapsed - -\begin_layout Plain Layout -Mauro Jaskelioff -\end_layout - -\end_inset - -Jaskelioff developed a technique that can lift effectful operations systematical -ly to almost all monad stacks. +). \end_layout \end_inset @@ -14046,8 +14038,42 @@ Either \end_layout \begin_layout Standard -The third problem is the lack of a general method of lifting effectful operation -s to arbitrary monad transformers. +The second problem is the lack of a general method for lifting effectful + operations to arbitrary monad transformers. +\begin_inset Foot +status open + +\begin_layout Plain Layout +M. +\begin_inset space ~ +\end_inset + + +\begin_inset Index idx +status collapsed + +\begin_layout Plain Layout +Mauro Jaskelioff +\end_layout + +\end_inset + +Jaskelioff developed a technique that can lift effectful operations systematical +ly to almost all monad stacks; see the paper +\family typewriter + +\begin_inset CommandInset href +LatexCommand href +target "https://www.fceia.unr.edu.ar/~mauro/pubs/monatron.pdf" +literal "false" + +\end_inset + + +\end_layout + +\end_inset + So far, the examples in this subsection were limited to operations with type signatures of the form \begin_inset Formula $L^{A}$ @@ -14413,7 +14439,93 @@ These examples show that lifting an operation to a specific monad transformer s. So, the length of required custom code is quadratic in the number of supported monads and linear in the number of operations. - For this reason, MTL libraries usually support only a limited number of +\end_layout + +\begin_layout Standard +The third problem is the large number of typeclass instances that the libraries + need to maintain. + As we have seen in the example with +\begin_inset listings +inline true +status open + +\begin_layout Plain Layout + +StateMonadOps +\end_layout + +\end_inset + +, just two implicit functions per monad type are in principle sufficient + to define the operation typeclasses for all monad stacks. + This would make the number of typeclass instances linear in the number + of supported monads. + However, for reasons of run-time efficiency, libraries sometimes provide + typeclass instances for many specific combination of monads (say, +\begin_inset listings +inline true +status open + +\begin_layout Plain Layout + +Reader +\end_layout + +\end_inset + + with +\begin_inset listings +inline true +status open + +\begin_layout Plain Layout + +State +\end_layout + +\end_inset + +, +\begin_inset listings +inline true +status open + +\begin_layout Plain Layout + +Either +\end_layout + +\end_inset + + with +\begin_inset listings +inline true +status open + +\begin_layout Plain Layout + +Reader +\end_layout + +\end_inset + +, and so on). + This makes the required number of typeclass instances quadratic in the + number of supported monads. + For this reason, libraries such as +\family typewriter +cats-mtl +\family default + support only a limited number of most frequently used monads. + Adding a new monad to +\family typewriter +cats-mtl +\family default + would require adding a large number of new typeclass implementations. +\end_layout + +\begin_layout Standard +For these reasons, MTL libraries usually support only a limited number of monads and operations. \end_layout