This package is based on "The Operational Monad 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, John Hughes 95, and Ryan Ingram's MonadPrompt package.
To understand what's going on, you'll have to read "The Operational Monad Tutorial". Here, I will first and foremost note the changes with respect to the tutorial.
+Several advanced example monads 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.
Program typeFor 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.
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 ++.
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))
+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". Time will tell which has more merit; for now I have opted for a seamless interaction with monad transformers.
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.
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.)
+ProgramIn the unimo paper, 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.
+ + diff --git a/doc/web/fptools.css b/doc/web/fptools.css new file mode 100644 --- /dev/null +++ b/doc/web/fptools.css @@ -0,0 +1,48 @@ +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; } diff --git a/docs/Documentation.md b/docs/Documentation.md deleted file mode 100644 --- a/docs/Documentation.md +++ /dev/null @@ -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." - - - -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. - diff --git a/docs/Makefile b/docs/Makefile deleted file mode 100644 --- a/docs/Makefile +++ /dev/null @@ -1,38 +0,0 @@ -###################################################################### -### Documentation and examples -.PHONY: website doc - -examples_hs=ListT LogicT PoorMansConcurrency TicTacToe State -examples_lhs=WebSessionState -examples=$(examples_hs:%=%.hs) $(examples_lhs:%=%.lhs) - -documentation=Documentation.html $(examples:%=examples/%.html) examples/operational-examples.tar.gz - -static=index.html examples.html fptools.css - -doc: $(documentation:%=web/%) - -HOST=apfelmus@code.haskell.org:/srv/projects/operational -website: $(documentation:%=web/%) $(static:%=web/%) - rsync $(static:%=web/%) web/Documentation.html $(HOST) - rsync $(examples:%=web/examples/%.html) web/examples/hscolour.css \ - $(HOST)/examples - -###################################################################### -### Generating documentation - -web/Documentation.html : Documentation.md - pandoc --standalone --toc --css=fptools.css \ - --number-sections "$<" > "$@" - -clean: - rm Documentation.html - -web/%.hs.html: %.hs - HsColour "$<" -css -o"$@" -web/%.lhs.html: %.lhs - HsColour "$<" -css -o"$@" - -web/examples/operational-examples.tar.gz: $(examples:%=examples/%) - tar czvf "$@" $^ - diff --git a/docs/examples/ListT.hs b/docs/examples/ListT.hs deleted file mode 100644 --- a/docs/examples/ListT.hs +++ /dev/null @@ -1,56 +0,0 @@ -{------------------------------------------------------------------------------ - Control.Monad.Operational - - Example: - List Monad Transformer - -------------------------------------------------------------------------------} -{-# LANGUAGE GADTs, Rank2Types, FlexibleInstances #-} -module ListT where - -import Control.Monad -import Control.Monad.Operational -import Control.Monad.Trans - -{------------------------------------------------------------------------------ - A direct implementation - type ListT m a = m [a] - would violate the monad laws, but we don't have that problem. -------------------------------------------------------------------------------} -data MPlus m a where - MZero :: MPlus m a - MPlus :: ListT m a -> ListT m a -> MPlus m a - -type ListT m a = ProgramT (MPlus m) m a - - -- *sigh* I want to use type synonyms for type constructors, too; - -- GHC doesn't accept MonadMPlus (ListT m) -instance Monad m => MonadPlus (ProgramT (MPlus m) m) where - mzero = singleton MZero - mplus m n = singleton (MPlus m n) - -runListT :: Monad m => ListT m a -> m [a] -runListT = eval <=< viewT - where - eval :: Monad m => ProgramViewT (MPlus m) m a -> m [a] - eval (Return x) = return [x] - eval (MZero :>>= k) = return [] - eval (MPlus m n :>>= k) = - liftM2 (++) (runListT (m >>= k)) (runListT (n >>= k)) - -testListT :: IO [()] -testListT = runListT $ do - n <- choice [1..5] - lift . print $ "You've chosen the number: " ++ show n - where - choice = foldr1 mplus . map return - - - -- testing the monad laws, from the Haskellwiki - -- http://www.haskell.org/haskellwiki/ListT_done_right#Order_of_printing -a,b,c :: ListT IO () -[a,b,c] = map (lift . putChar) ['a','b','c'] - - -- t1 and t2 have to print the same sequence of letters -t1 = runListT $ ((a `mplus` a) >> b) >> c -t2 = runListT $ (a `mplus` a) >> (b >> c) diff --git a/docs/examples/LogicT.hs b/docs/examples/LogicT.hs deleted file mode 100644 --- a/docs/examples/LogicT.hs +++ /dev/null @@ -1,86 +0,0 @@ -{------------------------------------------------------------------------------ - Control.Monad.Operational - - Example: - Oleg's LogicT monad transformer - - Functions to implement are taken from the corresponding paper - http://okmij.org/ftp/papers/LogicT.pdf - -------------------------------------------------------------------------------} -{-# LANGUAGE GADTs, Rank2Types #-} -module LogicT (LogicT, msplit, observe, bagOfN, interleave) where - -import Control.Monad -import Control.Monad.Operational -import Control.Monad.Trans - -import Data.Maybe - -{------------------------------------------------------------------------------ - LogicT - = A MonadPlus with an additional operation - msplit - which returns the first result and a computation to - produce the remaining results. - - - For example, the function msplit satisfies the laws - - msplit mzero ~> return Nothing - msplit (return a `mplus` m) ~> return (Just (a,m)) - - It turns out that we don't have to make msplit a primitive, - we can implement it by inspection on the argument. In other - words, LogicT will be the same as the ListT monad transformer -------------------------------------------------------------------------------} -import ListT -type LogicT m a = ListT m a - - -- msplit is the lift of a function split in the base monad -msplit :: Monad m => LogicT m a -> LogicT m (Maybe (a, LogicT m a)) -msplit = lift . split - - -- split in the base monad -split :: Monad m => LogicT m a -> m (Maybe (a, LogicT m a)) -split = eval <=< viewT - where - -- apply the laws for msplit - eval :: Monad m => ProgramViewT (MPlus m) m a -> m (Maybe (a, LogicT m a)) - eval (MZero :>>= k) = return Nothing - eval (MPlus m n :>>= k) = do - ma <- split (m >>= k) - case ma of - Nothing -> split (n >>= k) - Just (a,m') -> return $ Just (a, m' `mplus` (n >>= k)) - -- inefficient! - -- `mplus` will add another (>>= return) - -- to n each time it's called. - -- Curing this is not easy. - - -- main interpreter, section 6 in the paper - -- returns the first result, if any; may fail -observe :: Monad m => LogicT m a -> m a -observe m = (fst . fromJust) `liftM` split m - -{------------------------------------------------------------------------------ - Derived functions from the paper -------------------------------------------------------------------------------} - -- return the first n results, section 6 -bagOfN :: Monad m => Maybe Int -> LogicT m a -> LogicT m [a] -bagOfN (Just n) m | n <= 0 = return [] -bagOfN n m = msplit m >>= bagofN' - where - bagofN' Nothing = return [] - bagofN' (Just (x,m')) = (x:) `liftM` bagOfN (fmap pred n) m' - where pred n = n-1 - - -- interleave -interleave :: Monad m => LogicT m a -> LogicT m a -> LogicT m a -interleave m1 m2 = do - r <- msplit m1 - case r of - Nothing -> m2 - Just (a,m1') -> return a `mplus` interleave m2 m1' - - diff --git a/docs/examples/PoorMansConcurrency.hs b/docs/examples/PoorMansConcurrency.hs deleted file mode 100644 --- a/docs/examples/PoorMansConcurrency.hs +++ /dev/null @@ -1,63 +0,0 @@ -{------------------------------------------------------------------------------ - Control.Monad.Operational - - Example: - Koen Claessen's Poor Man's Concurrency Monad - http://www.cs.chalmers.se/~koen/pubs/entry-jfp99-monad.html - -------------------------------------------------------------------------------} -{-# LANGUAGE GADTs, Rank2Types #-} -module PoorMansConcurrency where - -import Control.Monad -import Control.Monad.Operational -import Control.Monad.Trans hiding (lift) - -{------------------------------------------------------------------------------ - A concurrency monad runs several processes in parallel - and supports two operations - - fork -- fork a new process - stop -- halt the current one - - We want this to be a monad transformer, so we also need a function lift - This time, however, we cannot use the monad transformer version ProgramT - because this will leave no room for interleaving different computations - of the base monad. -------------------------------------------------------------------------------} -data ProcessI m a where - Lift :: m a -> ProcessI m a - Stop :: ProcessI m a - Fork :: Process m () -> ProcessI m () - - -type Process m a = Program (ProcessI m) a - -stop = singleton Stop -fork = singleton . Fork -lift = singleton . Lift - - -- interpreter -runProcess :: Monad m => Process m a -> m () -runProcess m = schedule [m] - where - schedule (x:xs) = run (view x) xs - - run :: Monad m => ProgramView (ProcessI m) a -> [Process m a] -> m () - run (Return _) xs = return () -- process finished - run (Lift m :>>= k) xs = m >>= \a -> -- switch process - schedule (xs ++ [k a]) - run (Stop :>>= k) xs = schedule xs -- process halts - run (Fork p :>>= k) xs = schedule (xs ++ [x2,x1]) -- fork new process - where x1 = k (); x2 = p >>= k - - -- example - -- > runProcess example -- warning: runs indefinitely -example :: Process IO () -example = do - write "Start!" - fork (loop "fish") - loop "cat" - -write = lift . putStr -loop s = write s >> loop s diff --git a/docs/examples/State.hs b/docs/examples/State.hs deleted file mode 100644 --- a/docs/examples/State.hs +++ /dev/null @@ -1,60 +0,0 @@ -{------------------------------------------------------------------------------ - Control.Monad.Operational - - Example: - State monad and monad transformer - -------------------------------------------------------------------------------} -{-# LANGUAGE GADTs, Rank2Types, FlexibleInstances #-} -module State where - -import Control.Monad -import Control.Monad.Operational -import Control.Monad.Trans - -{------------------------------------------------------------------------------ - State Monad -------------------------------------------------------------------------------} -data StateI s a where - Get :: StateI s s - Put :: s -> StateI s () - -type State s a = Program (StateI s) a - -evalState :: State s a -> s -> a -evalState = eval . view - where - eval :: ProgramView (StateI s) a -> (s -> a) - eval (Return x) = const x - eval (Get :>>= k) = \s -> evalState (k s ) s - eval (Put s :>>= k) = \_ -> evalState (k ()) s - -put :: s -> StateT s m () -put = singleton . Put - -get :: StateT s m s -get = singleton Get - -testState :: Int -> Int -testState = evalState $ do - x <- get - put (x+2) - get - -{------------------------------------------------------------------------------ - State Monad Transformer -------------------------------------------------------------------------------} -type StateT s m a = ProgramT (StateI s) m a - -evalStateT :: Monad m => StateT s m a -> s -> m a -evalStateT m = \s -> viewT m >>= \p -> eval p s - where - eval :: Monad m => ProgramViewT (StateI s) m a -> (s -> m a) - eval (Return x) = \_ -> return x - eval (Get :>>= k) = \s -> evalStateT (k s ) s - eval (Put s :>>= k) = \_ -> evalStateT (k ()) s - -testStateT = evalStateT $ do - x <- get - lift $ putStrLn "Hello StateT" - put (x+1) diff --git a/docs/examples/TicTacToe.hs b/docs/examples/TicTacToe.hs deleted file mode 100644 --- a/docs/examples/TicTacToe.hs +++ /dev/null @@ -1,175 +0,0 @@ -{------------------------------------------------------------------------------ - Control.Monad.Operational - - Example: - An implementation of the game TicTacToe. - - Each player (human, AI, ...) is implemented in a separate monad - which are then intermingled to run the game. This resembles the - PoorMansConcurrency.hs example. - - - Many thanks to Yves Par`es and Bertram Felgenhauer - http://www.haskell.org/pipermail/haskell-cafe/2010-April/076216.html - -------------------------------------------------------------------------------} -{-# LANGUAGE GADTs, Rank2Types #-} - -import Control.Monad -import Control.Monad.Operational -import Control.Monad.State - -import Data.Either -import Data.List - - -- external libraries needed -import System.Random - -{------------------------------------------------------------------------------ - The Player monad for implementing players (human, AI, ...) - provides two operations - - readBoard -- read the current board position - playMove -- play a move - - to query the current board position and perform a move, respectively. - - Moreover, it's actually a monad transformer intended to be used over IO. - This way, the players can perform IO computations. -------------------------------------------------------------------------------} -data PlayerI a where - ReadBoard :: PlayerI Board - PlayMove :: Int -> PlayerI Bool - -type Player m a = ProgramT PlayerI m a - -readBoard = singleton ReadBoard -playMove = singleton . PlayMove - - -- interpreter -runGame :: Player IO () -> Player IO () -> IO () -runGame player1 player2 = eval' initialGameState player1 player2 - where - eval' game p1 p2 = viewT p1 >>= \p1view -> eval game p1view p2 - - eval :: GameState - -> ProgramViewT PlayerI IO () -> Player IO () - -> IO () - eval game (Return _) _ = return () - eval game (ReadBoard :>>= p1) p2 = eval' game (p1 (board game)) p2 - eval game (PlayMove mv :>>= p1) p2 = - case makeMove mv game of - Nothing -> eval' game (p1 False) p2 - Just game' - | won game' -> let p = activePlayer game in - putStrLn $ "Player " ++ show p ++ " has won!" - | draw game'-> putStrLn $ "It's a draw." - | otherwise -> eval' game' p2 (p1 True) - - -- example: human vs AI -main = do - g <- getStdGen - runGame playerHuman (playerAI g) - -{------------------------------------------------------------------------------ - TicTacToe Board type and logic - - The board looks like this: - - +---+---+---+ some squares already played on - | 1 | 2 | 3 | the empty squares are numbered - +---+---+---+ - | 4 | 5 |OOO| - +---+---+---+ - | 7 |XXX| 9 | - +---+---+---+ -------------------------------------------------------------------------------} -data Symbol = X | O deriving (Eq,Show) -type Square = Either Int Symbol -type Board = [[Square]] -data GameState = Game { board :: Board, activePlayer :: Symbol } - -initialGameState :: GameState -initialGameState = Game (map (map Left) [[1,2,3],[4,5,6],[7,8,9]]) X - - -- list the possible moves to play -possibleMoves :: Board -> [Int] -possibleMoves board = [k | Left k <- concat board] - - -- play a stone at a square -makeMove :: Int -> GameState -> Maybe GameState -makeMove k (Game board player) - | not (k `elem` possibleMoves board) = Nothing -- illegal move - | otherwise = Just $ Game (map (map replace) board) (switch player) - where - replace (Left k') | k' == k = Right player - replace x = x - - switch X = O - switch O = X - - -- has somebody won the game? -won :: GameState -> Bool -won (Game board _) = any full $ diagonals board ++ rows board ++ cols board - where - full [a,b,c] = a == b && b == c - diagonals [[a1,_,b1], - [_ ,c,_ ], - [b2,_,a2]] = [[a1,c,a2],[b1,c,b2]] - rows = id - cols = transpose - - -- is the game a draw? -draw :: GameState -> Bool -draw (Game board _) = null (possibleMoves board) - - -- print the board -showSquare = either (\n -> " " ++ show n ++ " ") (concat . replicate 3 . show) - -showBoard :: Board -> String -showBoard board = - unlines . surround "+---+---+---+" - . map (concat . surround "|". map showSquare) - $ board - where - surround x xs = [x] ++ intersperse x xs ++ [x] - -printBoard = putStr . showBoard - -{------------------------------------------------------------------------------ - Player examples -------------------------------------------------------------------------------} - -- a human player on the command line -playerHuman :: Player IO () -playerHuman = forever $ readBoard >>= liftIO . printBoard >> doMove - where - -- ask the player where to move - doMove :: Player IO () - doMove = do - liftIO . putStrLn $ "At which number would you like to play?" - n <- liftIO getLine - b <- playMove (read n) - unless b $ do - liftIO . putStrLn $ "Position " ++ show n ++ " is already full." - doMove - - -- a random AI, - -- also demonstrates how to use a custom StateT on top - -- of the Player monad -playerAI :: Monad m => StdGen -> Player m () -playerAI = evalStateT ai - where - ai :: Monad m => StateT StdGen (ProgramT PlayerI m) () - ai = forever $ do - board <- lift $ readBoard - n <- uniform (possibleMoves board) -- select a random move - lift $ playMove n - where - -- select one element at random - uniform :: Monad m => [a] -> StateT StdGen m a - uniform xs = do - gen <- get - let (n,gen') = randomR (1,length xs) gen - put gen' - return (xs !! (n-1)) - diff --git a/docs/examples/WebSessionState.lhs b/docs/examples/WebSessionState.lhs deleted file mode 100644 --- a/docs/examples/WebSessionState.lhs +++ /dev/null @@ -1,102 +0,0 @@ -#!/bin/sh runghc -\begin{code} -{------------------------------------------------------------------------------ - Control.Monad.Operational - - Example: - A CGI script that maintains session state - http://www.informatik.uni-freiburg.de/~thiemann/WASH/draft.pdf - -------------------------------------------------------------------------------} -{-# LANGUAGE GADTs, Rank2Types #-} -module WebSessionState where - -import Control.Monad -import Control.Monad.Operational -import Control.Monad.Trans hiding (lift) - -import Data.Char -import Data.Maybe - - -- external libraries needed -import Text.Html as H -import Network.CGI - -{------------------------------------------------------------------------------ - This example shows a "magic" implementation of a web session that - looks like it needs to be executed in a running process, - while in fact it's just a CGI script. - - The key part is a monad, called "Web" for lack of imagination, - which supports a single operation - - ask :: String -> Web String - - which sends a simple minded HTML-Form to the web user - and returns his answer. - - How does this work? The trick is that all previous answers - are logged in a hidden field of the input form. - The CGI script will simply replays this log when called. - In other words, the user state is stored in the input form. - -------------------------------------------------------------------------------} -data WebI a where - Ask :: String -> WebI String - -type Web a = Program WebI a - -ask = singleton . Ask - - -- interpreter -runWeb :: Web H.Html -> CGI CGIResult -runWeb m = do - -- fetch log - log' <- maybe [] (read . urlDecode) `liftM` getInput "log" - -- maybe append form input - f <- maybe id (\answer -> (++ [answer])) `liftM` getInput "answer" - let log = f log' - -- run Web action and output result - output . renderHtml =<< replay m log log - where - replay = eval . view - - eval :: ProgramView WebI H.Html -> [String] -> [String] -> CGI H.Html - eval (Return html) log _ = return html - eval (Ask question :>>= k) log (l:ls) = -- replay answer from log - replay (k l) log ls - eval (Ask question :>>= k) log [] = -- present HTML page to user - return $ htmlQuestion log question - - - -- HTML page with a single form -htmlQuestion log question = htmlEnvelope $ p << question +++ x - where - x = form ! [method "post"] << (textfield "answer" - +++ submit "Next" "" - +++ hidden "log" (urlEncode $ show log)) - -htmlMessage s = htmlEnvelope $ p << s - -htmlEnvelope html = - header << thetitle << "Web Session State demo" - +++ body << html - - - -- example -example :: Web H.Html -example = do - haskell <- ask "What's your favorite programming language?" - if map toLower haskell /= "haskell" - then message "Awww." - else do - ghc <- ask "What's your favorite compiler?" - web <- ask "What's your favorite monad?" - message $ "I like " ++ ghc ++ " too, but " - ++ web ++ " is debatable." - where - message = return . htmlMessage - -main = runCGI . runWeb $ example - -\end{code} diff --git a/docs/web/Documentation.html b/docs/web/Documentation.html deleted file mode 100644 --- a/docs/web/Documentation.html +++ /dev/null @@ -1,635 +0,0 @@ - - - -This package is based on "The Operational Monad 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, John Hughes 95, and Ryan Ingram's MonadPrompt package.
To understand what's going on, you'll have to read "The Operational Monad Tutorial". Here, I will first and foremost note the changes with respect to the tutorial.
Several advanced example monads 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.
Program typeFor 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.
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 ++.
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))
-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". Time will tell which has more merit; for now I have opted for a seamless interaction with monad transformers.
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.
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.)
ProgramIn the unimo paper, 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.
LogicT monad transformer.
-{------------------------------------------------------------------------------ - Control.Monad.Operational - - Example: - List Monad Transformer - -------------------------------------------------------------------------------} -{-# LANGUAGE GADTs, Rank2Types, FlexibleInstances #-} -module ListT where - -import Control.Monad -import Control.Monad.Operational -import Control.Monad.Trans - -{------------------------------------------------------------------------------ - A direct implementation - type ListT m a = m [a] - would violate the monad laws, but we don't have that problem. -------------------------------------------------------------------------------} -data MPlus m a where - MZero :: MPlus m a - MPlus :: ListT m a -> ListT m a -> MPlus m a - -type ListT m a = ProgramT (MPlus m) m a - - -- *sigh* I want to use type synonyms for type constructors, too; - -- GHC doesn't accept MonadMPlus (ListT m) -instance Monad m => MonadPlus (ProgramT (MPlus m) m) where - mzero = singleton MZero - mplus m n = singleton (MPlus m n) - -runListT :: Monad m => ListT m a -> m [a] -runListT = eval <=< viewT - where - eval :: Monad m => ProgramViewT (MPlus m) m a -> m [a] - eval (Return x) = return [x] - eval (MZero :>>= k) = return [] - eval (MPlus m n :>>= k) = - liftM2 (++) (runListT (m >>= k)) (runListT (n >>= k)) - -testListT :: IO [()] -testListT = runListT $ do - n <- choice [1..5] - lift . print $ "You've chosen the number: " ++ show n - where - choice = foldr1 mplus . map return - - - -- testing the monad laws, from the Haskellwiki - -- http://www.haskell.org/haskellwiki/ListT_done_right#Order_of_printing -a,b,c :: ListT IO () -[a,b,c] = map (lift . putChar) ['a','b','c'] - - -- t1 and t2 have to print the same sequence of letters -t1 = runListT $ ((a `mplus` a) >> b) >> c -t2 = runListT $ (a `mplus` a) >> (b >> c) -- diff --git a/docs/web/examples/LogicT.hs.html b/docs/web/examples/LogicT.hs.html deleted file mode 100644 --- a/docs/web/examples/LogicT.hs.html +++ /dev/null @@ -1,96 +0,0 @@ - - - - -
{------------------------------------------------------------------------------ - Control.Monad.Operational - - Example: - Oleg's LogicT monad transformer - - Functions to implement are taken from the corresponding paper - http://okmij.org/ftp/papers/LogicT.pdf - -------------------------------------------------------------------------------} -{-# LANGUAGE GADTs, Rank2Types #-} -module LogicT (LogicT, msplit, observe, bagOfN, interleave) where - -import Control.Monad -import Control.Monad.Operational -import Control.Monad.Trans - -import Data.Maybe - -{------------------------------------------------------------------------------ - LogicT - = A MonadPlus with an additional operation - msplit - which returns the first result and a computation to - produce the remaining results. - - - For example, the function msplit satisfies the laws - - msplit mzero ~> return Nothing - msplit (return a `mplus` m) ~> return (Just (a,m)) - - It turns out that we don't have to make msplit a primitive, - we can implement it by inspection on the argument. In other - words, LogicT will be the same as the ListT monad transformer -------------------------------------------------------------------------------} -import ListT -type LogicT m a = ListT m a - - -- msplit is the lift of a function split in the base monad -msplit :: Monad m => LogicT m a -> LogicT m (Maybe (a, LogicT m a)) -msplit = lift . split - - -- split in the base monad -split :: Monad m => LogicT m a -> m (Maybe (a, LogicT m a)) -split = eval <=< viewT - where - -- apply the laws for msplit - eval :: Monad m => ProgramViewT (MPlus m) m a -> m (Maybe (a, LogicT m a)) - eval (MZero :>>= k) = return Nothing - eval (MPlus m n :>>= k) = do - ma <- split (m >>= k) - case ma of - Nothing -> split (n >>= k) - Just (a,m') -> return $ Just (a, m' `mplus` (n >>= k)) - -- inefficient! - -- `mplus` will add another (>>= return) - -- to n each time it's called. - -- Curing this is not easy. - - -- main interpreter, section 6 in the paper - -- returns the first result, if any; may fail -observe :: Monad m => LogicT m a -> m a -observe m = (fst . fromJust) `liftM` split m - -{------------------------------------------------------------------------------ - Derived functions from the paper -------------------------------------------------------------------------------} - -- return the first n results, section 6 -bagOfN :: Monad m => Maybe Int -> LogicT m a -> LogicT m [a] -bagOfN (Just n) m | n <= 0 = return [] -bagOfN n m = msplit m >>= bagofN' - where - bagofN' Nothing = return [] - bagofN' (Just (x,m')) = (x:) `liftM` bagOfN (fmap pred n) m' - where pred n = n-1 - - -- interleave -interleave :: Monad m => LogicT m a -> LogicT m a -> LogicT m a -interleave m1 m2 = do - r <- msplit m1 - case r of - Nothing -> m2 - Just (a,m1') -> return a `mplus` interleave m2 m1' - - -- diff --git a/docs/web/examples/PoorMansConcurrency.hs.html b/docs/web/examples/PoorMansConcurrency.hs.html deleted file mode 100644 --- a/docs/web/examples/PoorMansConcurrency.hs.html +++ /dev/null @@ -1,73 +0,0 @@ - - - - -
{------------------------------------------------------------------------------ - Control.Monad.Operational - - Example: - Koen Claessen's Poor Man's Concurrency Monad - http://www.cs.chalmers.se/~koen/pubs/entry-jfp99-monad.html - -------------------------------------------------------------------------------} -{-# LANGUAGE GADTs, Rank2Types #-} -module PoorMansConcurrency where - -import Control.Monad -import Control.Monad.Operational -import Control.Monad.Trans hiding (lift) - -{------------------------------------------------------------------------------ - A concurrency monad runs several processes in parallel - and supports two operations - - fork -- fork a new process - stop -- halt the current one - - We want this to be a monad transformer, so we also need a function lift - This time, however, we cannot use the monad transformer version ProgramT - because this will leave no room for interleaving different computations - of the base monad. -------------------------------------------------------------------------------} -data ProcessI m a where - Lift :: m a -> ProcessI m a - Stop :: ProcessI m a - Fork :: Process m () -> ProcessI m () - - -type Process m a = Program (ProcessI m) a - -stop = singleton Stop -fork = singleton . Fork -lift = singleton . Lift - - -- interpreter -runProcess :: Monad m => Process m a -> m () -runProcess m = schedule [m] - where - schedule (x:xs) = run (view x) xs - - run :: Monad m => ProgramView (ProcessI m) a -> [Process m a] -> m () - run (Return _) xs = return () -- process finished - run (Lift m :>>= k) xs = m >>= \a -> -- switch process - schedule (xs ++ [k a]) - run (Stop :>>= k) xs = schedule xs -- process halts - run (Fork p :>>= k) xs = schedule (xs ++ [x2,x1]) -- fork new process - where x1 = k (); x2 = p >>= k - - -- example - -- > runProcess example -- warning: runs indefinitely -example :: Process IO () -example = do - write "Start!" - fork (loop "fish") - loop "cat" - -write = lift . putStr -loop s = write s >> loop s -- diff --git a/docs/web/examples/State.hs.html b/docs/web/examples/State.hs.html deleted file mode 100644 --- a/docs/web/examples/State.hs.html +++ /dev/null @@ -1,70 +0,0 @@ - - - - -
{------------------------------------------------------------------------------ - Control.Monad.Operational - - Example: - State monad and monad transformer - -------------------------------------------------------------------------------} -{-# LANGUAGE GADTs, Rank2Types, FlexibleInstances #-} -module State where - -import Control.Monad -import Control.Monad.Operational -import Control.Monad.Trans - -{------------------------------------------------------------------------------ - State Monad -------------------------------------------------------------------------------} -data StateI s a where - Get :: StateI s s - Put :: s -> StateI s () - -type State s a = Program (StateI s) a - -evalState :: State s a -> s -> a -evalState = eval . view - where - eval :: ProgramView (StateI s) a -> (s -> a) - eval (Return x) = const x - eval (Get :>>= k) = \s -> evalState (k s ) s - eval (Put s :>>= k) = \_ -> evalState (k ()) s - -put :: s -> StateT s m () -put = singleton . Put - -get :: StateT s m s -get = singleton Get - -testState :: Int -> Int -testState = evalState $ do - x <- get - put (x+2) - get - -{------------------------------------------------------------------------------ - State Monad Transformer -------------------------------------------------------------------------------} -type StateT s m a = ProgramT (StateI s) m a - -evalStateT :: Monad m => StateT s m a -> s -> m a -evalStateT m = \s -> viewT m >>= \p -> eval p s - where - eval :: Monad m => ProgramViewT (StateI s) m a -> (s -> m a) - eval (Return x) = \_ -> return x - eval (Get :>>= k) = \s -> evalStateT (k s ) s - eval (Put s :>>= k) = \_ -> evalStateT (k ()) s - -testStateT = evalStateT $ do - x <- get - lift $ putStrLn "Hello StateT" - put (x+1) -- diff --git a/docs/web/examples/TicTacToe.hs.html b/docs/web/examples/TicTacToe.hs.html deleted file mode 100644 --- a/docs/web/examples/TicTacToe.hs.html +++ /dev/null @@ -1,186 +0,0 @@ - - - - -
{------------------------------------------------------------------------------ - Control.Monad.Operational - - Example: - An implementation of the game TicTacToe. - - Each player (human, AI, ...) is implemented in a separate monad - which are then intermingled to run the game. This resembles the - PoorMansConcurrency.hs example. - - - Many thanks to Yves Pars and Bertram Felgenhauer - http://www.haskell.org/pipermail/haskell-cafe/2010-April/076216.html - -------------------------------------------------------------------------------} -{-# LANGUAGE GADTs, Rank2Types #-} -module TicTacToe where - -import Control.Monad -import Control.Monad.Operational -import Control.Monad.State - -import Data.Either -import Data.List - - -- external libraries needed -import System.Random - -{------------------------------------------------------------------------------ - The Player monad for implementing players (human, AI, ...) - provides two operations - - readBoard -- read the current board position - playMove -- play a move - - to query the current board position and perform a move, respectively. - - Moreover, it's actually a monad transformer intended to be used over IO. - This way, the players can perform IO computations. -------------------------------------------------------------------------------} -data PlayerI a where - ReadBoard :: PlayerI Board - PlayMove :: Int -> PlayerI Bool - -type Player m a = ProgramT PlayerI m a - -readBoard = singleton ReadBoard -playMove = singleton . PlayMove - - -- interpreter -runGame :: Player IO () -> Player IO () -> IO () -runGame player1 player2 = eval' initialGameState player1 player2 - where - eval' game p1 p2 = viewT p1 >>= \p1view -> eval game p1view p2 - - eval :: GameState - -> ProgramViewT PlayerI IO () -> Player IO () - -> IO () - eval game (Return _) _ = return () - eval game (ReadBoard :>>= p1) p2 = eval' game (p1 (board game)) p2 - eval game (PlayMove mv :>>= p1) p2 = - case makeMove mv game of - Nothing -> eval' game (p1 False) p2 - Just game' - | won game' -> let p = activePlayer game in - putStrLn $ "Player " ++ show p ++ " has won!" - | draw game'-> putStrLn $ "It's a draw." - | otherwise -> eval' game' p2 (p1 True) - - -- example: human vs AI -main = do - g <- getStdGen - runGame playerHuman (playerAI g) - -{------------------------------------------------------------------------------ - TicTacToe Board type and logic - - The board looks like this: - - +---+---+---+ some squares already played on - | 1 | 2 | 3 | the empty squares are numbered - +---+---+---+ - | 4 | 5 |OOO| - +---+---+---+ - | 7 |XXX| 9 | - +---+---+---+ -------------------------------------------------------------------------------} -data Symbol = X | O deriving (Eq,Show) -type Square = Either Int Symbol -type Board = [[Square]] -data GameState = Game { board :: Board, activePlayer :: Symbol } - -initialGameState :: GameState -initialGameState = Game (map (map Left) [[1,2,3],[4,5,6],[7,8,9]]) X - - -- list the possible moves to play -possibleMoves :: Board -> [Int] -possibleMoves board = [k | Left k <- concat board] - - -- play a stone at a square -makeMove :: Int -> GameState -> Maybe GameState -makeMove k (Game board player) - | not (k `elem` possibleMoves board) = Nothing -- illegal move - | otherwise = Just $ Game (map (map replace) board) (switch player) - where - replace (Left k') | k' == k = Right player - replace x = x - - switch X = O - switch O = X - - -- has somebody won the game? -won :: GameState -> Bool -won (Game board _) = any full $ diagonals board ++ rows board ++ cols board - where - full [a,b,c] = a == b && b == c - diagonals [[a1,_,b1], - [_ ,c,_ ], - [b2,_,a2]] = [[a1,c,a2],[b1,c,b2]] - rows = id - cols = transpose - - -- is the game a draw? -draw :: GameState -> Bool -draw (Game board _) = null (possibleMoves board) - - -- print the board -showSquare = either (\n -> " " ++ show n ++ " ") (concat . replicate 3 . show) - -showBoard :: Board -> String -showBoard board = - unlines . surround "+---+---+---+" - . map (concat . surround "|". map showSquare) - $ board - where - surround x xs = [x] ++ intersperse x xs ++ [x] - -printBoard = putStr . showBoard - -{------------------------------------------------------------------------------ - Player examples -------------------------------------------------------------------------------} - -- a human player on the command line -playerHuman :: Player IO () -playerHuman = forever $ readBoard >>= liftIO . printBoard >> doMove - where - -- ask the player where to move - doMove :: Player IO () - doMove = do - liftIO . putStrLn $ "At which number would you like to play?" - n <- liftIO getLine - b <- playMove (read n) - unless b $ do - liftIO . putStrLn $ "Position " ++ show n ++ " is already full." - doMove - - -- a random AI, - -- also demonstrates how to use a custom StateT on top - -- of the Player monad -playerAI :: Monad m => StdGen -> Player m () -playerAI = evalStateT ai - where - ai :: Monad m => StateT StdGen (ProgramT PlayerI m) () - ai = forever $ do - board <- lift $ readBoard - n <- uniform (possibleMoves board) -- select a random move - lift $ playMove n - where - -- select one element at random - uniform :: Monad m => [a] -> StateT StdGen m a - uniform xs = do - gen <- get - let (n,gen') = randomR (1,length xs) gen - put gen' - return (xs !! (n-1)) - -- diff --git a/docs/web/examples/WebSessionState.lhs.html b/docs/web/examples/WebSessionState.lhs.html deleted file mode 100644 --- a/docs/web/examples/WebSessionState.lhs.html +++ /dev/null @@ -1,112 +0,0 @@ - - - - -
{------------------------------------------------------------------------------ - Control.Monad.Operational - - Example: - A CGI script that maintains session state - http://www.informatik.uni-freiburg.de/~thiemann/WASH/draft.pdf - -------------------------------------------------------------------------------} -{-# LANGUAGE GADTs, Rank2Types #-} -module WebSessionState where - -import Control.Monad -import Control.Monad.Operational -import Control.Monad.Trans hiding (lift) - -import Data.Char -import Data.Maybe - - -- external libraries needed -import Text.Html as H -import Network.CGI - -{------------------------------------------------------------------------------ - This example shows a "magic" implementation of a web session that - looks like it needs to be executed in a running process, - while in fact it's just a CGI script. - - The key part is a monad, called "Web" for lack of imagination, - which supports a single operation - - ask :: String -> Web String - - which sends a simple minded HTML-Form to the web user - and returns his answer. - - How does this work? The trick is that all previous answers - are logged in a hidden field of the input form. - The CGI script will simply replays this log when called. - In other words, the user state is stored in the input form. - -------------------------------------------------------------------------------} -data WebI a where - Ask :: String -> WebI String - -type Web a = Program WebI a - -ask = singleton . Ask - - -- interpreter -runWeb :: Web H.Html -> CGI CGIResult -runWeb m = do - -- fetch log - log' <- maybe [] (read . urlDecode) `liftM` getInput "log" - -- maybe append form input - f <- maybe id (\answer -> (++ [answer])) `liftM` getInput "answer" - let log = f log' - -- run Web action and output result - output . renderHtml =<< replay m log log - where - replay = eval . view - - eval :: ProgramView WebI H.Html -> [String] -> [String] -> CGI H.Html - eval (Return html) log _ = return html - eval (Ask question :>>= k) log (l:ls) = -- replay answer from log - replay (k l) log ls - eval (Ask question :>>= k) log [] = -- present HTML page to user - return $ htmlQuestion log question - - - -- HTML page with a single form -htmlQuestion log question = htmlEnvelope $ p << question +++ x - where - x = form ! [method "post"] << (textfield "answer" - +++ submit "Next" "" - +++ hidden "log" (urlEncode $ show log)) - -htmlMessage s = htmlEnvelope $ p << s - -htmlEnvelope html = - header << thetitle << "Web Session State demo" - +++ body << html - - - -- example -example :: Web H.Html -example = do - haskell <- ask "What's your favorite programming language?" - if map toLower haskell /= "haskell" - then message "Awww." - else do - ghc <- ask "What's your favorite compiler?" - web <- ask "What's your favorite monad?" - message $ "I like " ++ ghc ++ " too, but " - ++ web ++ " is debatable." - where - message = return . htmlMessage - -main = runCGI . runWeb $ example - -\end{code} - - diff --git a/docs/web/examples/hscolour.css b/docs/web/examples/hscolour.css deleted file mode 100644 --- a/docs/web/examples/hscolour.css +++ /dev/null @@ -1,5 +0,0 @@ -.hs-keyglyph, .hs-layout { color: red; } -.hs-keyword { color: blue; } -.hs-comment, .hs-comment a { color: green; } -.hs-str, .hs-chr { color: teal; } -.hs-keyword,.hs-conid, .hs-varid, .hs-conop, .hs-varop, .hs-num, .hs-cpp, .hs-sel, .hs-definition {} diff --git a/docs/web/fptools.css b/docs/web/fptools.css deleted file mode 100644 --- a/docs/web/fptools.css +++ /dev/null @@ -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; } diff --git a/docs/web/index.html b/docs/web/index.html deleted file mode 100644 --- a/docs/web/index.html +++ /dev/null @@ -1,24 +0,0 @@ -