operational 0.2.2.1 → 0.2.3.2
raw patch · 11 files changed
+439/−552 lines, 11 filesdep ~basedep ~mtlPVP ok
version bump matches the API change (PVP)
Dependency ranges changed: base, mtl
API changes (from Hackage documentation)
+ Control.Monad.Operational: instance MonadReader r m => MonadReader r (ProgramT instr m)
Files
- CHANGELOG +15/−2
- doc/Documentation.md +0/−248
- doc/Readme.md +15/−0
- doc/design.md +67/−0
- doc/examples/Readme.md +20/−0
- doc/proofs.md +190/−0
- doc/tutorial-changes.md +116/−0
- doc/web/Documentation.html +0/−218
- doc/web/fptools.css +0/−48
- operational.cabal +5/−6
- src/Control/Monad/Operational.hs +11/−30
CHANGELOG view
@@ -1,7 +1,21 @@ Changelog --------- +operational - 0.2.3.1++* bump dependency `mtl >= 1.1 && < 2.3`.++operational - 0.2.3.0++* added instance for `MonadReader` class+* clean up documentation++operational - 0.2.2.0++* add utility function `interpretWithMonad`+ operational - 0.2.1.0+ * minor change: eta-reduce `Program` and `ProgramView` type synonyms operational - 0.2.0.3@@ -13,8 +27,7 @@ * changed name of view type to `ProgramView` * added instances for mtl classes * new function `liftProgram` to embed `Program` in `ProgramT`--* new example TicTacToe.hs+* new example `TicTacToe.hs` * various documentation updates operational - 0.1.0.0
− doc/Documentation.md
@@ -1,248 +0,0 @@-% Documentation for the "operational" package-% Heinrich Apfelmus-% Sun, 18 Apr 2010 13:06:16 +0200-- [tutorial]: http://themonadreader.wordpress.com/2010/01/26/issue-15/- [unimo]: http://web.cecs.pdx.edu/~cklin/papers/unimo-143.pdf "Chuan-kai Lin. Programming Monads Operationally with Unimo."- [hughes]: http://citeseer.ist.psu.edu/hughes95design.html "John Hughes. The Design of a Pretty-printing Library."- [prompt]: http://hackage.haskell.org/package/MonadPrompt "Ryan Ingram's Monad Prompt Package."--<!-- *The HTML version of this document is generated automatically from the corresponding markdown file, don't change it!* -->--Introduction-============-This package is based on ["The Operational Monad Tutorial"][tutorial] and this documentation describes its extension to a production-quality library. In other words, the "magic" gap between relevant paper and library implementation is documented here.--Take note that this this library is only ~50 lines of code, yet the documentation even includes a proof! :-)--Sources and inspiration for this library include [Chuan-kai Lin's unimo paper][unimo], [John Hughes 95][hughes], and [Ryan Ingram's `MonadPrompt` package][prompt].--Using this Library-=================-To understand what's going on, you'll have to read ["The Operational Monad Tutorial"][tutorial]. Here, I will first and foremost note the changes with respect to the tutorial.--Several advanced [example monads](./examples.html) demonstrate how to put this library to good use. In the source distribution, the corresponding source files can also be found in the `.docs/examples` folder.--Changes to the `Program` type-------------------------------For efficiency reasons, the type `Program` representing a list of instructions is now *abstract*. A function `view` is used to inspect the first instruction, it returns a type-- data ProgramView instr a where- Return :: a -> ProgramView instr a- (:>>=) :: instr a -> (a -> Program instr b) -> ProgramView instr b--which is much like the old `Program` type, except that `Then` was renamed to `:>>=` and that the subsequent instructions stored in the second argument of `:>>=` are stored in the type `Program`, not `ProgramView`.- -To see an example of the new style, here the interpreter for the stack machine from the tutorial:-- interpret :: StackProgram a -> (Stack Int -> a)- interpret = eval . view- where- eval :: ProgramView StackInstruction a -> (Stack Int -> a)- eval (Push a :>>= is) stack = interpret (is ()) (a:stack)- eval (Pop :>>= is) (a:stack) = interpret (is a ) stack- eval (Return a) stack = a--So-called "view functions" like `view` are a common way of inspecting data structures that have been made abstract for reasons of efficiency; see for example `viewL` and `viewR` in [`Data.Sequence`][containers].-- [containers]: http://hackage.haskell.org/package/containers-0.3.0.0--Efficiency------------Compared to the original type from the tutorial, `Program` now supports `>>=` in O(1) time in most use cases. This means that left-biased nesting like-- let- nestLeft :: Int -> StackProgram Int- nestLeft 0 = return 0- nestLeft n = nestLeft (n-1) >>= push- in- interpret (nestLeft n) []- -will now take O(n) time. In contrast, the old `Program` type from the tutorial would have taken O(n^2) time, similar to `++` for lists taking quadratic time in when nested to the left.--However, this does *not* hold in a *persistent* setting. In particular, the example-- let- p = nestLeft n- v1 = view p- v2 = view p- v3 = view p- in- v1 `seq` v2 `seq` v3--will take O(n) time for each call of `view` instead of O(n) the first time and O(1) for the other calls. But since monads are usually used ephemerally, this is much less a restriction than it would be for lists and `++`.--Monad Transformers--------------------Furthermore, `Program` is actually a type synonym and expressed in terms of a monad transformer `ProgramT`-- type Program instr a = ProgramT instr Identity a--Likewise, `view` is a specialization of `viewT` to the identity monad. This change is transparent (except for error messages on type errors) for users who are happy with just `Program` but very convenient for those users who want to use it as a monad transformer.--The key point about the transformer version `ProgramT` is that in addition to the monad laws, it automatically satisfies the lifting laws for monad transformers as well-- lift . return = return- lift m >>= lift . g = lift (m >>= g)--The corresponding view function `viewT` now returns the type `m (ViewT instr m a)`. It's not immediately apparent why this return type will do, but it's straightforward to work with, like in the following implementation of the list monad transformer:-- data PlusI m a where- Zero :: PlusI m a- Plus :: ListT m a -> ListT m a -> PlusI m a- - type ListT m a = ProgramT (PlusI m) m a- - runList :: Monad m => ListT m a -> m [a]- runList = eval <=< viewT- where- eval :: Monad m => ProgramViewT (PlusI m) m a -> m [a]- eval (Return x) = return [x]- eval (Zero :>>= k) = return []- eval (Plus m n :>>= k) =- liftM2 (++) (runList (m >>= k)) (runList (n >>= k))---Alternatives to Monad Transformers------------------------------------By the way, note that monad transformers are not the only way to build larger monads from smaller ones; a similar effect can be achieved with the direct sum of instructions sets. For instance, the monad-- Program (StateI s :+: ExceptionI e) a-- data (f :+: g) a = Inl (f a) | Inr (g a) -- a fancy Either--is a combination of the state monad-- type State a = Program (StateI s) a-- data StateI s a where- Put :: s -> StateI s ()- Get :: StateI s s--and the error monad-- type Error e a = Program (ErrorI e) a-- data ErrorI e a where- Throw :: e -> ErrorI e ()- Catch :: ErrorI e a -> (e -> ErrorI e a) -> ErrorI e a--The "sum of signatures" approach and the `(:+:)` type constructor are advocated in [Wouter Swierstra's "Data Types a la carte"][a la carte]. Time will tell which has more merit; for now I have opted for a seamless interaction with monad transformers.-- [a la carte]: http://www.cse.chalmers.se/~wouter/Publications/DataTypesALaCarte.pdf "Wouter Swierstra. Data types à la carte."---Design and Implementation-=========================-Proof of the monad laws (Sketch)----------------------------------The key point of this library is of course that the `view` and `viewT` functions respect the monad laws. While this seems obvious from the definition, the proof is actually not straightforward.--First, we restrict ourselves to `view`, i.e. the version without monad transformers. In fact, I don't have a full proof for the version with monad transformers, more about that in the next section.--Second, we use a sloppy, but much more suitable notation, namely we write----------- --------------------------`>>=` instead of `Bind`-`return` instead of `Lift` for the identity monad-`i,j,k,`... for primitive instructions----------------------------------------------------------------Then, the `view` function becomes-- view (return a) = Return a- view (return a >>= g) = g a -- left unit- view ((m >>= f) >>= g) = view (m >>= (\x -> f x >>= g) -- associativity- view (i >>= g) = i :>>= g- view i = i :>>= return -- right unit--Clearly, `view` uses the monad laws to rewrite it's argument. But we want to show that whenever two expressions-- e1,e2 :: Program instr a--can be transformed into each other by rewriting them with the monad laws in *any* fashion (remember that `>>=` and `return` are constructors), then `view` will map them to the same result. More formally, we have an equivalence relation-- e1 ~ e2 iff e1 and e2 are the same modulo monad laws--and want to show-- e1 ~ e2 => view e1 = view e2 (some notion of equality)--Now, this needs proof because `view` is like a term rewriting system and there is no guarantee that two equivalent terms will be rewritten to the same normal form.--Trying to attack this problem with term rewriting and critical pairs is probably hopeless and not very enlightening. After all, the theorem should be obvious because two equivalent expressions should have the same *first instruction* `i`. Well, we can formalize this with the help of a *normal form*-- data NF instr a where- Return' :: a -> NF instr a- (:>>=') :: instr a -> (a -> NF instr b) -> NF instr b--This is the old program type and the key observation is that `NF instr` is already a monad.-- instance Monad (NF inst) where- (Return' a) >>= g = g a- (m :>>=' f) >>= g = m :>>= (\x -> f x >>= g)--(I'll skip the short calculation and coinduction argument that this really fulfills the monad laws.) We can define a normalization function-- normalize :: Program instr a -> NF instr a- normalize (m >>= g) = normalize m >>=' normalize g- normalize (return a) = Return' a- normalize i = i :>>=' Return'--which has the now obvious property that-- e1 ~ e2 => normalize e1 = normalize e2--Now, the return type of `view` is akin to a *head normal form*, hence-- normalize (view e1) = normalize (view e2) - => view e1 = view e2--(for some suitable extension of `normalize` to the `ProgramView` type.) But since `view` only uses monad laws to rewrite its argument, we also have-- e1 ~ view e1 => normalize e1 = normalize (view e1)--and this concludes the proof, which pretty much only showed that two equivalent expressions have the same instruction list and hence `view` gives equal results.--Monad Transformers--------------------The monad transformer case is more hairy, I have no proof here. (If you read this by accident: don't worry, it's still correct. This is for proof nerds only.)--The main difficulty is that the equation-- return = lift . return--is an equation for the already existing `return` constructor and the notion of "first instruction" no longer applies. Namely, we have-- m = return m >>= id = lift (return m) >>= id--and it's not longer clear what a suitable normal form might be. It appears that `viewT` rewrites the term as follows-- lift m >>= g- = lift m >>= (\x -> lift (return (g x)) >>= id)- = (lift m >>= lift . return . g) >>= id- = lift (m >>= return . g) >>= id--(To be continued.)---Other Design Choices-====================-Recursive type definitions with `Program`-------------------------------------------In the [unimo paper][unimo], the instructions carry an additional parameter that "unties" recursive type definition. For example, the instructions for `MonadPlus` are written-- data PlusI unimo a where- Zero :: PlusI unimo a- Plus :: unimo a -> unimo a -> PlusI unimo a--The type constructor variable `unimo` will be tied to `Unimo PlusI`.--In this library, I have opted for the conceptually simpler approach that requires the user to tie the recursion himself-- data PlusI a where- Zero :: PlusI a- Plus :: Program PlusI a -> Program PlusI a -> Plus I a--I am not sure whether this has major consequences for composeablity; at the moment I believe that the former style can always be recovered from an implementation in the latter style.-
+ doc/Readme.md view
@@ -0,0 +1,15 @@+This folder contains various documentation for the `operational` package.++Files:++<dl>+<dt><a href="design.md"><code>design.md</code></a>+ <dd>Describes miscellanous design decisions.+<dt><a href="examples/"><code>examples/</code></a>+ <dd>Extensive <b>code examples</b>.+<dt><a href="proofs.md"><code>proofs.md</code></a>+ <dd>Proofs that the implementation is correct: monad laws, monad transformer classes.+<dt><a href="tutorial-changes.md"><code>tutorial-changes.md</code></a>+ <dd>Documents changes how the library API and implementation differs from the Operational Monad Tutorial.+</dl>+
+ doc/design.md view
@@ -0,0 +1,67 @@+This document discusses miscellaneous design decisions and remarks for the `operational` library. This is mainly so that I can still remember them in a couple of years.++Lifting control operations+--------------------------+The monad transformer `ProgramT` can automatically lift operations from the base monad, notably those from `MonadState` and `MonadIO`.++Until recently, I thought that this is restricted to algebraic operations and cannot be done for control operations. (For more on this nomenclature, see a [remark by Conor McBride][conor].) However, it turns that it can actually be done for some control operations as well!++ [conor]: http://www.haskell.org/pipermail/haskell-cafe/2010-April/076185.html++For instance, the `MonadReader` class has a control operation `local`. The point is that it is subject to the following laws++ local :: MonadReader r m => (r -> r) -> m a -> m a++ local r (lift m) = lift (local r m)+ local r (return a) = return a+ local r (m >>= k) = local r m >>= local r . k++Together with the requirement that the new instructions introduced by `ProgramT` do not interfere with the corresponding effect,++ local r (singleton instr) = singleton instr++these laws specify a unique lifting.++In other words, we can lift control operations whenever they obey laws that relate to `>>=` and `return`.++`mapMonad`+----------+Limestraël [has suggested][1] that the module `Control.Monad.Operational` includes a function++ mapMonad :: (Monad m, Monad n)+ => (forall a. m a -> n a) -> ProgramT instr m a -> ProgramT instr n a++which changes the base monad for the `ProgramT` monad transformer. A possible implementation is++ mapMonad f = id' <=< lift . f . viewT+ where+ id' (Return a) = return a+ id' (i :>>= k) = singleton i >>= mapMonad f . k++However, for the time being, I have [opted against][1] adding this function because there is no guarantee that the mapping function `forall. m a -> n a` actually preserves the argument.+++ [1]: http://www.haskell.org/pipermail/haskell-cafe/2010-May/077094.html+ [2]: http://www.haskell.org/pipermail/haskell-cafe/2010-May/077097.html+++Recursive type definitions with `Program`+-----------------------------------------+In the [unimo paper][unimo], the instructions carry an additional parameter that "unties" recursive type definition. For example, the instructions for `MonadPlus` are written++ data PlusI unimo a where+ Zero :: PlusI unimo a+ Plus :: unimo a -> unimo a -> PlusI unimo a++The type constructor variable `unimo` will be tied to `Unimo PlusI`.++In this library, I have opted for the conceptually simpler approach that requires the user to tie the recursion himself++ data PlusI a where+ Zero :: PlusI a+ Plus :: Program PlusI a -> Program PlusI a -> Plus I a++I am not sure whether this has major consequences for composeablity; at the moment I believe that the former style can always be recovered from an implementation in the latter style.+++ [unimo]: http://web.cecs.pdx.edu/~cklin/papers/unimo-143.pdf "Chuan-kai Lin. Programming Monads Operationally with Unimo."
+ doc/examples/Readme.md view
@@ -0,0 +1,20 @@+Example Code for the *operational* package+==========================================++<dl>+<dt><a href="BreadthFirstParsing.hs">BreadthFirstParsing.hs</a>+ <dd>An breadth-first implementation of parser combinators.+ As this implementation does not back-track, we avoid a common space leak.+<dt><a href="LogicT.hs">LogicT.hs</a>+ <dd>Oleg Kiselyov's <code>LogicT</code> monad transformer.+<dt><a href="ListT.hs">ListT.hs</a>+ <dd>Correct implementation of the list monad transformer.+<dt><a href="PoorMansConcurrency.hs">PoorMansConcurrency.hs</a>+ <dd>Koen Claessen's poor man's concurrency monad, implements cooperative multitasking.+<dt><a href="State.hs">State.hs</a>+ <dd>Very simple example showing how to implement the state monad.+<dt><a href="TicTacToe.hs">TicTacToe.hs</a>+ <dd>The game of TicTacToe. Mix and mash humans and AI as you like; players are implemented in a special monad that looks like there is only one player playing.+<dt><a href="WebSessionState.lhs">WebSessionState.lhs</a>+ <dd>CGI Script that is written in a style seems to require exeution in a persistent process, but actually stores a log of the session in the client.+</dl>
+ doc/proofs.md view
@@ -0,0 +1,190 @@+Correctness Proofs+==================++This document collects correctness proofs for the `operational` library.++ [tutorial]: http://apfelmus.nfshost.com/articles/operational-monad.html++Monad laws+----------++For reasons of efficiency, the `Program` type is not implemented as a list of instructions as presented in the [The Operational Monad Tutorial][tutorial]. However, this means that we now have to prove that the implementations of `view` and `viewT` *respect the monad laws*.++In particular, we say that two programs++ e1, e2 :: Program instr a++are *equivalent*, `e1 ~ e2`, if they can be transformed into each other by applying the monad laws on the constructors. For instance, the expressions++ e1 = ((m `Bind` f) `Bind` g+ e2 = m `Bind` (\a -> f a `Bind` g)++are equivalent for any expressions `m`, `f` and `g`. Our goal is to show that the `view` functions give the same result for equivalent expressions:++ e1 ~ e2 => view e1 = view e2++The `ProgramView` type is equipped with an appropriate equality relation:++ (Return a1) = (Return a2) iff a1 = a2+ (i1 :>>= k1) = (i2 :>>= k2) iff i1 = i2 and k1 x ~ k2 x for all x++### Normal form: list of instructions++The key observation for the proof is the following: As in the [tutorial][], the `Program` type represents a list of instructions. The representation is redundant for the purpose of efficiency, but different expressions should still correspond to the same list of instructions if they are equivalent. After all, equivalence is just about the associativity of the `Bind` operation. This also means that the first instruction, and hence the result of `view` should be unique for each equivalence class.++For simplicity, let us first focus on the pure `Program` type and postpone the case `ProgramT` for monad transformers later.++We can formalize the intuition above by introducing the following types of *normal form*++ data NF instr a where+ Return' :: a -> NF instr a+ (:>>=') :: instr a -> (a -> NF instr b) -> NF instr b++which is simply the list of instructions from the [tutorial][]. Now, we know that `NF` is a monad++ instance Monad (NF instr) where+ return = Return'+ (Return' a) >>= k = k a+ (m :>>=' g) >>= k = m :>>=' (\a -> g a :>>=' k)++In particular, it fulfills the monad laws. (Actually we would have to prove that by using coinduction, but I leave that as an exercise.)++We can now map each `Program` to its normal form++ normalize :: Program instr a -> NF instr a+ normalize (m `Bind` k) = normalize m >>= normalize k+ normalize (Return a) = return a+ normalize (Instr i) = i :>>=' return++In particular, note that this function is a morphism and `NF` fulfills the monad laws. Hence, equivalent programs will be mapped to the same normal form, i.e.++ e1 ~ e2 => normalize e1 = normalize e2+++How does this observation help us? Note that the `view` only uses the monad laws to rewrite a `Program`. Using a somewhat sloppy notation, we express this as++ e1 ~ view e1++where we intepret a view `i :>>= k` as the "obvious" `Program` expression `Bind (Instr i) k` where the left argument of the `Bind` constructor is an instruction. Furthermore, we can think of the `ProgramView` type as a head normal form. In other words, applying `normalize` to an expression of the form `view e1` will not change the first instruction, which means++ normalize (view e1) = normalize (view e2) => view e1 = view e2++(The requires a coinductive argument for the tail of instructions.)++Taking these three implications together, we see that++ e1 ~ e2 => view e1 = view e2++as desired.++### Normal form for monad transformers++A similar technique can be used to show that the monad laws also hold for the monad transformer version `ProgramT`. The key observation here is that the normal form is an *effectful list of instructions*++ newtype NFT instr m a = JoinLift (m (NFT' instr m a))++ data NFT' instr m a where+ Return' :: a -> NFT' instr m a+ (:>>=') :: instr a -> (a -> NFT instr m b) -> NFT' instr m b++This is in very close analogy to the "effectful list"++ type ListT m a = m (ListT' m a)+ data ListT' m a = Nil | Cons a (ListT m a)++For example, if the monad `m` is the state monad, then this type represents a list whose tail depends on the current state.++First, we convince ourselves that the `NFT` type is indeed a monad transformer. The corresponding functions are implemented as++ instance Monad m => Monad (NFT instr m) where+ return a = JoinLift (return (Return' a))+ + (JoinLift m) >>= k = JoinLift (m >>= f)+ where+ f (Return' a) = k a+ f (i :>>=' f) = return $ i :>>= (\a -> f a >>= k)++ instance MonadTrans (NFT instr) where+ lift m = JoinLift (fmap Return' m)+ + singleton i = JoinLift (return (i :>>=' return))++It is somewhat tedious to check the monad laws and the lifting laws, so we skip this step here.+++Having convinced ourselves that the normal form type `NFT` is, in fact, a monad transformer, we can define a morphism++ normalize :: ProgramT instr m a -> NFT instr m a+ normalize (Lift m) = lift m+ normalize (m `Bind` k) = m >>= k+ normalize (Instr i) = singleton i++and obtain that equivalent programs are mapped to equal normal forms. Similar to the pure case, normalizing the result of `viewT` will not change the first instruction, and we can conclude that the result `viewT` only depends on the normal form of the argument.+++Lifting monads+--------------++The normal forms are also useful for proving that class instances can be lifted from a base monad `m` to the monad `ProgramT instr m`.++### Instructions and control operations++Some monads only feature "algebraic" instructions which have the form++ instr :: a1 -> a2 -> ... -> m b++so that the types `a1`, `a2`, etc. of the parameters do not contain the monad `m` again. For example, the state monad has two instructions++ get :: State s s+ put :: s -> State s ()++of precisely this form. Lifting these kinds of instructions is straightforward, i.e. the `ProgramT instr State` monad is also a state monad.++ instance (MonadState s m) => MonadState s (ProgramT instr m) where+ get = lift get+ put = lift . put +++However, some monads feature *control operations*, which are instructions that contain the monad `m` in the argument. Essentially, they can change the *control flow*. For example, the `MonadPlus` class contains an instruction++ mplus :: MonadPlus m => m a -> m a -> m a++that combines the control flows of two monadic arguments.++For more on the distinction between algebraic operation and control operation, see also a [discussion by Conor McBride][conor].++ [conor]: http://www.haskell.org/pipermail/haskell-cafe/2010-April/076185.html++### MonadReader++The main feature of the `MonadReader` class is an algebraic operation++ ask :: MonadReader m r => m r++but unfortunately, it also includes a control operation++ local :: MonadReader m r => (r -> r) -> m r -> m r++and it is not clear whether this can be lifted to the `ProgramT` transformer. We certainly expect the following law to hold++ local r (lift m) = lift (local f m)++Fortunately, this control operation is very benign, in that it is actually a monad morphism++ local r (return a) = return a+ local r (m >>= k) = local r m >>= local r . k++Imposing that the lifted control operation should also be a morphism, we can define it for normal forms as follows++ local :: MonadReader m r => (r -> r)+ -> ProgramT instr m a -> ProgramT instr m a+ local r (JoinLift m) = JoinLift $ local r (m >>= return . f)+ where+ f (Return' a) = return a+ f (i :>>=' k) = singleton i >>= local r . k+ +Again, it is somewhat tedious to check that this definition fulfills the lifting and morphism laws. However, we have now succeeded in lifting a control operation!++++
+ doc/tutorial-changes.md view
@@ -0,0 +1,116 @@++ [tutorial]: http://apfelmus.nfshost.com/articles/operational-monad.html++The `operational` library is based on ["The Operational Monad Tutorial"][tutorial], but features a slightly different API and implementation.++This document describes how the library has been changed compared to the tutorial.+++Changes to the `Program` type+-----------------------------+For efficiency reasons, the type `Program` representing a list of instructions is now *abstract*. A function `view` is used to inspect the first instruction, it returns a type++ data ProgramView instr a where+ Return :: a -> ProgramView instr a+ (:>>=) :: instr a -> (a -> Program instr b) -> ProgramView instr b++which is much like the old `Program` type, except that `Then` was renamed to `:>>=` and that the subsequent instructions stored in the second argument of `:>>=` are stored in the type `Program`, not `ProgramView`.+ +To see an example of the new style, here the interpreter for the stack machine from the tutorial:++ interpret :: StackProgram a -> (Stack Int -> a)+ interpret = eval . view+ where+ eval :: ProgramView StackInstruction a -> (Stack Int -> a)+ eval (Push a :>>= is) stack = interpret (is ()) (a:stack)+ eval (Pop :>>= is) (a:stack) = interpret (is a ) stack+ eval (Return a) stack = a++So-called "view functions" like `view` are a common way of inspecting data structures that have been made abstract for reasons of efficiency; see for example `viewL` and `viewR` in [`Data.Sequence`][containers].++ [containers]: http://hackage.haskell.org/package/containers++Efficiency+----------+Compared to the original type from the tutorial, `Program` now supports `>>=` in O(1) time in most use cases. This means that left-biased nesting like++ let+ nestLeft :: Int -> StackProgram Int+ nestLeft 0 = return 0+ nestLeft n = nestLeft (n-1) >>= push+ in+ interpret (nestLeft n) []+ +will now take O(n) time. In contrast, the old `Program` type from the tutorial would have taken O(n^2) time, similar to `++` for lists taking quadratic time in when nested to the left.++However, this does *not* hold in a *persistent* setting. In particular, the example++ let+ p = nestLeft n+ v1 = view p+ v2 = view p+ v3 = view p+ in+ v1 `seq` v2 `seq` v3++will take O(n) time for each call of `view` instead of O(n) the first time and O(1) for the other calls. But since monads are usually used ephemerally, this is much less a restriction than it would be for lists and `++`.++Monad Transformers+------------------+Furthermore, `Program` is actually a type synonym and expressed in terms of a monad transformer `ProgramT`++ type Program instr a = ProgramT instr Identity a++Likewise, `view` is a specialization of `viewT` to the identity monad. This change is transparent (except for error messages on type errors) for users who are happy with just `Program` but very convenient for those users who want to use it as a monad transformer.++The key point about the transformer version `ProgramT` is that in addition to the monad laws, it automatically satisfies the lifting laws for monad transformers as well++ lift . return = return+ lift m >>= lift . g = lift (m >>= g)++The corresponding view function `viewT` now returns the type `m (ViewT instr m a)`. It's not immediately apparent why this return type will do, but it's straightforward to work with, like in the following implementation of the list monad transformer:++ data PlusI m a where+ Zero :: PlusI m a+ Plus :: ListT m a -> ListT m a -> PlusI m a+ + type ListT m a = ProgramT (PlusI m) m a+ + runList :: Monad m => ListT m a -> m [a]+ runList = eval <=< viewT+ where+ eval :: Monad m => ProgramViewT (PlusI m) m a -> m [a]+ eval (Return x) = return [x]+ eval (Zero :>>= k) = return []+ eval (Plus m n :>>= k) =+ liftM2 (++) (runList (m >>= k)) (runList (n >>= k))++++Alternatives to Monad Transformers+----------------------------------+By the way, note that monad transformers are not the only way to build larger monads from smaller ones; a similar effect can be achieved with the direct sum of instructions sets. For instance, the monad++ Program (StateI s :+: ExceptionI e) a++ data (f :+: g) a = Inl (f a) | Inr (g a) -- a fancy Either++is a combination of the state monad++ type State a = Program (StateI s) a++ data StateI s a where+ Put :: s -> StateI s ()+ Get :: StateI s s++and the error monad++ type Error e a = Program (ErrorI e) a++ data ErrorI e a where+ Throw :: e -> ErrorI e ()+ Catch :: ErrorI e a -> (e -> ErrorI e a) -> ErrorI e a++The "sum of signatures" approach and the `(:+:)` type constructor are advocated in [Wouter Swierstra's "Data Types a la carte"][a la carte]. Time will tell which has more merit; for now I have opted for a seamless interaction with monad transformers.++ [a la carte]: http://www.cse.chalmers.se/~wouter/Publications/DataTypesALaCarte.pdf "Wouter Swierstra. Data types à la carte."
− doc/web/Documentation.html
@@ -1,218 +0,0 @@-<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd">-<html xmlns="http://www.w3.org/1999/xhtml">-<head>- <meta http-equiv="Content-Type" content="text/html; charset=utf-8" />- <meta name="generator" content="pandoc" />- <meta name="author" content="Heinrich Apfelmus" />- <meta name="date" content="Sun, 18 Apr 2010 13:06:16 +0200" />- <title>Documentation for the "operational" package</title>- <link rel="stylesheet" href="fptools.css" type="text/css" />-</head>-<body>-<h1 class="title">Documentation for the "operational" package</h1>-<div id="TOC">-<ul>-<li><a href="#introduction"><span class="toc-section-number">1</span> Introduction</a></li>-<li><a href="#using-this-library"><span class="toc-section-number">2</span> Using this Library</a><ul>-<li><a href="#changes-to-the-program-type"><span class="toc-section-number">2.1</span> Changes to the <code>Program</code> type</a></li>-<li><a href="#efficiency"><span class="toc-section-number">2.2</span> Efficiency</a></li>-<li><a href="#monad-transformers"><span class="toc-section-number">2.3</span> Monad Transformers</a></li>-<li><a href="#alternatives-to-monad-transformers"><span class="toc-section-number">2.4</span> Alternatives to Monad Transformers</a></li>-</ul></li>-<li><a href="#design-and-implementation"><span class="toc-section-number">3</span> Design and Implementation</a><ul>-<li><a href="#proof-of-the-monad-laws-sketch"><span class="toc-section-number">3.1</span> Proof of the monad laws (Sketch)</a></li>-<li><a href="#monad-transformers-1"><span class="toc-section-number">3.2</span> Monad Transformers</a></li>-</ul></li>-<li><a href="#other-design-choices"><span class="toc-section-number">4</span> Other Design Choices</a><ul>-<li><a href="#recursive-type-definitions-with-program"><span class="toc-section-number">4.1</span> Recursive type definitions with <code>Program</code></a></li>-</ul></li>-</ul>-</div>-<!-- *The HTML version of this document is generated automatically from the corresponding markdown file, don't change it!* -->--<h1 id="introduction"><a href="#TOC"><span class="header-section-number">1</span> Introduction</a></h1>-<p>This package is based on <a href="http://themonadreader.wordpress.com/2010/01/26/issue-15/">"The Operational Monad Tutorial"</a> and this documentation describes its extension to a production-quality library. In other words, the "magic" gap between relevant paper and library implementation is documented here.</p>-<p>Take note that this this library is only ~50 lines of code, yet the documentation even includes a proof! :-)</p>-<p>Sources and inspiration for this library include <a href="http://web.cecs.pdx.edu/~cklin/papers/unimo-143.pdf" title="Chuan-kai Lin. Programming Monads Operationally with Unimo.">Chuan-kai Lin's unimo paper</a>, <a href="http://citeseer.ist.psu.edu/hughes95design.html" title="John Hughes. The Design of a Pretty-printing Library.">John Hughes 95</a>, and <a href="http://hackage.haskell.org/package/MonadPrompt" title="Ryan Ingram's Monad Prompt Package.">Ryan Ingram's <code>MonadPrompt</code> package</a>.</p>-<h1 id="using-this-library"><a href="#TOC"><span class="header-section-number">2</span> Using this Library</a></h1>-<p>To understand what's going on, you'll have to read <a href="http://themonadreader.wordpress.com/2010/01/26/issue-15/">"The Operational Monad Tutorial"</a>. Here, I will first and foremost note the changes with respect to the tutorial.</p>-<p>Several advanced <a href="./examples.html">example monads</a> demonstrate how to put this library to good use. In the source distribution, the corresponding source files can also be found in the <code>.docs/examples</code> folder.</p>-<h2 id="changes-to-the-program-type"><a href="#TOC"><span class="header-section-number">2.1</span> Changes to the <code>Program</code> type</a></h2>-<p>For efficiency reasons, the type <code>Program</code> representing a list of instructions is now <em>abstract</em>. A function <code>view</code> is used to inspect the first instruction, it returns a type</p>-<pre><code>data ProgramView instr a where- Return :: a -> ProgramView instr a- (:>>=) :: instr a -> (a -> Program instr b) -> ProgramView instr b-</code></pre>-<p>which is much like the old <code>Program</code> type, except that <code>Then</code> was renamed to <code>:>>=</code> and that the subsequent instructions stored in the second argument of <code>:>>=</code> are stored in the type <code>Program</code>, not <code>ProgramView</code>.</p>-<p>To see an example of the new style, here the interpreter for the stack machine from the tutorial:</p>-<pre><code>interpret :: StackProgram a -> (Stack Int -> a)-interpret = eval . view- where- eval :: ProgramView StackInstruction a -> (Stack Int -> a)- eval (Push a :>>= is) stack = interpret (is ()) (a:stack)- eval (Pop :>>= is) (a:stack) = interpret (is a ) stack- eval (Return a) stack = a-</code></pre>-<p>So-called "view functions" like <code>view</code> are a common way of inspecting data structures that have been made abstract for reasons of efficiency; see for example <code>viewL</code> and <code>viewR</code> in <a href="http://hackage.haskell.org/package/containers-0.3.0.0"><code>Data.Sequence</code></a>.</p>-<h2 id="efficiency"><a href="#TOC"><span class="header-section-number">2.2</span> Efficiency</a></h2>-<p>Compared to the original type from the tutorial, <code>Program</code> now supports <code>>>=</code> in O(1) time in most use cases. This means that left-biased nesting like</p>-<pre><code>let- nestLeft :: Int -> StackProgram Int- nestLeft 0 = return 0- nestLeft n = nestLeft (n-1) >>= push-in- interpret (nestLeft n) []-</code></pre>-<p>will now take O(n) time. In contrast, the old <code>Program</code> type from the tutorial would have taken O(n^2) time, similar to <code>++</code> for lists taking quadratic time in when nested to the left.</p>-<p>However, this does <em>not</em> hold in a <em>persistent</em> setting. In particular, the example</p>-<pre><code>let- p = nestLeft n- v1 = view p- v2 = view p- v3 = view p-in- v1 `seq` v2 `seq` v3-</code></pre>-<p>will take O(n) time for each call of <code>view</code> instead of O(n) the first time and O(1) for the other calls. But since monads are usually used ephemerally, this is much less a restriction than it would be for lists and <code>++</code>.</p>-<h2 id="monad-transformers"><a href="#TOC"><span class="header-section-number">2.3</span> Monad Transformers</a></h2>-<p>Furthermore, <code>Program</code> is actually a type synonym and expressed in terms of a monad transformer <code>ProgramT</code></p>-<pre><code>type Program instr a = ProgramT instr Identity a-</code></pre>-<p>Likewise, <code>view</code> is a specialization of <code>viewT</code> to the identity monad. This change is transparent (except for error messages on type errors) for users who are happy with just <code>Program</code> but very convenient for those users who want to use it as a monad transformer.</p>-<p>The key point about the transformer version <code>ProgramT</code> is that in addition to the monad laws, it automatically satisfies the lifting laws for monad transformers as well</p>-<pre><code>lift . return = return-lift m >>= lift . g = lift (m >>= g)-</code></pre>-<p>The corresponding view function <code>viewT</code> now returns the type <code>m (ViewT instr m a)</code>. It's not immediately apparent why this return type will do, but it's straightforward to work with, like in the following implementation of the list monad transformer:</p>-<pre><code>data PlusI m a where- Zero :: PlusI m a- Plus :: ListT m a -> ListT m a -> PlusI m a--type ListT m a = ProgramT (PlusI m) m a--runList :: Monad m => ListT m a -> m [a]-runList = eval <=< viewT- where- eval :: Monad m => ProgramViewT (PlusI m) m a -> m [a]- eval (Return x) = return [x]- eval (Zero :>>= k) = return []- eval (Plus m n :>>= k) =- liftM2 (++) (runList (m >>= k)) (runList (n >>= k))-</code></pre>-<h2 id="alternatives-to-monad-transformers"><a href="#TOC"><span class="header-section-number">2.4</span> Alternatives to Monad Transformers</a></h2>-<p>By the way, note that monad transformers are not the only way to build larger monads from smaller ones; a similar effect can be achieved with the direct sum of instructions sets. For instance, the monad</p>-<pre><code>Program (StateI s :+: ExceptionI e) a--data (f :+: g) a = Inl (f a) | Inr (g a) -- a fancy Either-</code></pre>-<p>is a combination of the state monad</p>-<pre><code>type State a = Program (StateI s) a--data StateI s a where- Put :: s -> StateI s ()- Get :: StateI s s-</code></pre>-<p>and the error monad</p>-<pre><code>type Error e a = Program (ErrorI e) a--data ErrorI e a where- Throw :: e -> ErrorI e ()- Catch :: ErrorI e a -> (e -> ErrorI e a) -> ErrorI e a-</code></pre>-<p>The "sum of signatures" approach and the <code>(:+:)</code> type constructor are advocated in <a href="http://www.cse.chalmers.se/~wouter/Publications/DataTypesALaCarte.pdf" title="Wouter Swierstra. Data types à la carte.">Wouter Swierstra's "Data Types a la carte"</a>. Time will tell which has more merit; for now I have opted for a seamless interaction with monad transformers.</p>-<h1 id="design-and-implementation"><a href="#TOC"><span class="header-section-number">3</span> Design and Implementation</a></h1>-<h2 id="proof-of-the-monad-laws-sketch"><a href="#TOC"><span class="header-section-number">3.1</span> Proof of the monad laws (Sketch)</a></h2>-<p>The key point of this library is of course that the <code>view</code> and <code>viewT</code> functions respect the monad laws. While this seems obvious from the definition, the proof is actually not straightforward.</p>-<p>First, we restrict ourselves to <code>view</code>, i.e. the version without monad transformers. In fact, I don't have a full proof for the version with monad transformers, more about that in the next section.</p>-<p>Second, we use a sloppy, but much more suitable notation, namely we write</p>-<table>-<tbody>-<tr class="odd">-<td align="left"><code>>>=</code></td>-<td align="center">instead of <code>Bind</code></td>-</tr>-<tr class="even">-<td align="left"><code>return</code></td>-<td align="center">instead of <code>Lift</code> for the identity monad</td>-</tr>-<tr class="odd">-<td align="left"><code>i,j,k,</code>...</td>-<td align="center">for primitive instructions</td>-</tr>-</tbody>-</table>-<p>Then, the <code>view</code> function becomes</p>-<pre><code>view (return a) = Return a-view (return a >>= g) = g a -- left unit-view ((m >>= f) >>= g) = view (m >>= (\x -> f x >>= g) -- associativity-view (i >>= g) = i :>>= g-view i = i :>>= return -- right unit-</code></pre>-<p>Clearly, <code>view</code> uses the monad laws to rewrite it's argument. But we want to show that whenever two expressions</p>-<pre><code>e1,e2 :: Program instr a-</code></pre>-<p>can be transformed into each other by rewriting them with the monad laws in <em>any</em> fashion (remember that <code>>>=</code> and <code>return</code> are constructors), then <code>view</code> will map them to the same result. More formally, we have an equivalence relation</p>-<pre><code>e1 ~ e2 iff e1 and e2 are the same modulo monad laws-</code></pre>-<p>and want to show</p>-<pre><code>e1 ~ e2 => view e1 = view e2 (some notion of equality)-</code></pre>-<p>Now, this needs proof because <code>view</code> is like a term rewriting system and there is no guarantee that two equivalent terms will be rewritten to the same normal form.</p>-<p>Trying to attack this problem with term rewriting and critical pairs is probably hopeless and not very enlightening. After all, the theorem should be obvious because two equivalent expressions should have the same <em>first instruction</em> <code>i</code>. Well, we can formalize this with the help of a <em>normal form</em></p>-<pre><code>data NF instr a where- Return' :: a -> NF instr a- (:>>=') :: instr a -> (a -> NF instr b) -> NF instr b-</code></pre>-<p>This is the old program type and the key observation is that <code>NF instr</code> is already a monad.</p>-<pre><code>instance Monad (NF inst) where- (Return' a) >>= g = g a- (m :>>=' f) >>= g = m :>>= (\x -> f x >>= g)-</code></pre>-<p>(I'll skip the short calculation and coinduction argument that this really fulfills the monad laws.) We can define a normalization function</p>-<pre><code>normalize :: Program instr a -> NF instr a-normalize (m >>= g) = normalize m >>=' normalize g-normalize (return a) = Return' a-normalize i = i :>>=' Return'-</code></pre>-<p>which has the now obvious property that</p>-<pre><code>e1 ~ e2 => normalize e1 = normalize e2-</code></pre>-<p>Now, the return type of <code>view</code> is akin to a <em>head normal form</em>, hence</p>-<pre><code> normalize (view e1) = normalize (view e2) -=> view e1 = view e2-</code></pre>-<p>(for some suitable extension of <code>normalize</code> to the <code>ProgramView</code> type.) But since <code>view</code> only uses monad laws to rewrite its argument, we also have</p>-<pre><code>e1 ~ view e1 => normalize e1 = normalize (view e1)-</code></pre>-<p>and this concludes the proof, which pretty much only showed that two equivalent expressions have the same instruction list and hence <code>view</code> gives equal results.</p>-<h2 id="monad-transformers-1"><a href="#TOC"><span class="header-section-number">3.2</span> Monad Transformers</a></h2>-<p>The monad transformer case is more hairy, I have no proof here. (If you read this by accident: don't worry, it's still correct. This is for proof nerds only.)</p>-<p>The main difficulty is that the equation</p>-<pre><code>return = lift . return-</code></pre>-<p>is an equation for the already existing <code>return</code> constructor and the notion of "first instruction" no longer applies. Namely, we have</p>-<pre><code>m = return m >>= id = lift (return m) >>= id-</code></pre>-<p>and it's not longer clear what a suitable normal form might be. It appears that <code>viewT</code> rewrites the term as follows</p>-<pre><code> lift m >>= g-= lift m >>= (\x -> lift (return (g x)) >>= id)-= (lift m >>= lift . return . g) >>= id-= lift (m >>= return . g) >>= id-</code></pre>-<p>(To be continued.)</p>-<h1 id="other-design-choices"><a href="#TOC"><span class="header-section-number">4</span> Other Design Choices</a></h1>-<h2 id="recursive-type-definitions-with-program"><a href="#TOC"><span class="header-section-number">4.1</span> Recursive type definitions with <code>Program</code></a></h2>-<p>In the <a href="http://web.cecs.pdx.edu/~cklin/papers/unimo-143.pdf" title="Chuan-kai Lin. Programming Monads Operationally with Unimo.">unimo paper</a>, the instructions carry an additional parameter that "unties" recursive type definition. For example, the instructions for <code>MonadPlus</code> are written</p>-<pre><code>data PlusI unimo a where- Zero :: PlusI unimo a- Plus :: unimo a -> unimo a -> PlusI unimo a-</code></pre>-<p>The type constructor variable <code>unimo</code> will be tied to <code>Unimo PlusI</code>.</p>-<p>In this library, I have opted for the conceptually simpler approach that requires the user to tie the recursion himself</p>-<pre><code>data PlusI a where- Zero :: PlusI a- Plus :: Program PlusI a -> Program PlusI a -> Plus I a-</code></pre>-<p>I am not sure whether this has major consequences for composeablity; at the moment I believe that the former style can always be recovered from an implementation in the latter style.</p>-</body>-</html>
− doc/web/fptools.css
@@ -1,48 +0,0 @@-body {- font-family: Verdana, sans-serif;- width: 43em;- margin: 1ex 3em 1ex;-}--div {- font-family: sans-serif;- color: black;- background: white-}--h1, h2, h3, h4, h5, h6, p.title, h1 > a:visited, h2 > a:visited, h1 > a:link, h2 > a:link { color: #005A9C; text-decoration:none; }--h1 { font: 170% sans-serif; }-h2 { font: 140% sans-serif; }-h3 { font: 120% sans-serif; }-h4 { font: bold 100% sans-serif; }-h5 { font: italic 100% sans-serif; }-h6 { font: small-caps 100% sans-serif; }--pre {- font-family: monospace;- border-width: 1px;- border-style: solid;- padding: 0.3em;- color: maroon;-}--pre.screen { color: #006400; }-pre.programlisting { color: maroon; }--div.example {- margin: 1ex 0em;- border: solid #412e25 1px;- padding: 0ex 0.4em;-}--div.example, div.example-contents {- background-color: #fffcf5;-}--a:link { color: #0000C8; }-a:hover { background: #FFFFA8; }-a:active { color: #D00000; }-a:visited { color: #680098; }--h1 > a { color: #000; }
operational.cabal view
@@ -1,5 +1,5 @@ Name: operational-Version: 0.2.2.1+Version: 0.2.3.2 Synopsis: Implementation of difficult monads made easy with operational semantics. Description:@@ -16,18 +16,17 @@ License-file: LICENSE Author: Heinrich Apfelmus Maintainer: Heinrich Apfelmus <apfelmus quantentunnel de>-Copyright: (c) Heinrich Apfelmus 2010-2011+Copyright: (c) Heinrich Apfelmus 2010-2013 Homepage: http://haskell.org/haskellwiki/Operational Stability: Provisional build-type: Simple cabal-version: >= 1.6 extra-source-files: CHANGELOG- doc/Documentation.md+ doc/*.md doc/examples/*.hs doc/examples/*.lhs- doc/web/fptools.css- doc/web/Documentation.html+ doc/examples/*.md flag buildExamples description: Build example executables.@@ -39,7 +38,7 @@ Library hs-source-dirs: src- build-depends: base == 4.* , mtl >= 1.1 && < 2.2.0+ build-depends: base == 4.* , mtl >= 1.1 && < 2.4.0 ghc-options: -Wall extensions: GADTs, Rank2Types, ScopedTypeVariables, UndecidableInstances,
src/Control/Monad/Operational.hs view
@@ -29,7 +29,7 @@ -- Those commented out cannot be instantiated. For reasons see below. -- import Control.Monad.Cont.Class -- import Control.Monad.Error.Class--- import Control.Monad.Reader.Class+import Control.Monad.Reader.Class import Control.Monad.State.Class -- import Control.Monad.Writer.Class @@ -293,17 +293,11 @@ * All of these instances need UndecidableInstances, because they do not satisfy the coverage condition.- - * We can only make instances of those classes- that do not contain control operators. Control operators are- functions like- - listen :: m a -> m (a,w)- - that take arguments of type m a and cannot be implemented with lift .+ Most of the instance in the mtl package itself have the same issue. - See also Conor McBride's remark on haskell-cafe:- http://www.haskell.org/pipermail/haskell-cafe/2010-April/076185.html+ * Lifting algebraic operations is easy,+ lifting control operations is more elaborate, but sometimes possible.+ See the design notes in `doc/design.md`. ------------------------------------------------------------------------------} instance (MonadState s m) => MonadState s (ProgramT instr m) where get = lift get@@ -312,23 +306,10 @@ instance (MonadIO m) => MonadIO (ProgramT instr m) where liftIO = lift . liftIO -{- Attempt to lift control operators anyway. WARNING: HERE BE DRAGONS-- -- lift a control operation with a single argument- -- Unfortunately, I don't have a specifications in terms of laws yet- -- I think it makes use of- -- liftControlOp1 f (lift m >>= k) = lift m >>= liftControlOp1 f . k- -- and is therefore completely useless.-liftControlOp1 :: Monad m =>- (m a -> m b) -> (ProgramT instr m a -> ProgramT instr m b)-liftControlOp1 f = join . lift . (eval <=< viewT)- where- eval :: ProgramViewT instr m a -> m (ProgramT instr m a)- eval (Return a) = f (return a)- eval (i :>>= k) = i :>>= liftControlOp1 f . k+instance (MonadReader r m) => MonadReader r (ProgramT instr m) where+ ask = lift ask+ + local r (Lift m) = Lift (local r m)+ local r (m `Bind` k) = local r m `Bind` (local r . k)+ local r (Instr i) = Instr i -instance (MonadWriter w m) => MonadWriter w (ProgramT instr m) where- tell = lift . tell- listen = liftControlOp1 listen- pass = liftControlOp1 pass--}