packages feed

operational (empty) → 0.1.0.0

raw patch · 13 files changed

+1519/−0 lines, 13 filesdep +basedep +mtlsetup-changed

Dependencies added: base, mtl

Files

+ LICENSE view
@@ -0,0 +1,31 @@+(c) 2010 Heinrich Apfelmus++All rights reserved.++Redistribution and use in source and binary forms, with or without+modification, are permitted provided that the following conditions+are met:++1. Redistributions of source code must retain the above copyright+notice, this list of conditions and the following disclaimer.++2. Redistributions in binary form must reproduce the above copyright+notice, this list of conditions and the following disclaimer in the+documentation and/or other materials provided with the distribution.++3. Neither the name of the author nor the names of his contributors+may be used to endorse or promote products derived from this software+without specific prior written permission.++THIS SOFTWARE IS PROVIDED BY THE CONTRIBUTORS ``AS IS'' AND ANY EXPRESS+OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED+WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE+DISCLAIMED.  IN NO EVENT SHALL THE AUTHORS OR CONTRIBUTORS BE LIABLE FOR+ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL+DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS+OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION)+HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT,+STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN+ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE+POSSIBILITY OF SUCH DAMAGE.+~                          
+ Setup.hs view
@@ -0,0 +1,36 @@+module Main where++-- Cabal+import Distribution.Simple++import Distribution.Simple.Setup ( fromFlag, HaddockFlags(..) )+import Distribution.Simple.LocalBuildInfo ( LocalBuildInfo(..) )+import Distribution.Simple.BuildPaths ( haddockPref )+import Distribution.Simple.Utils ( setupMessage )+import Distribution.PackageDescription++import Distribution.Verbosity ++-- Base+import System.FilePath ((</>))+import System.Directory(copyFile)+++main :: IO ()+main = defaultMainWithHooks myHooks+    where+    -- also install additional HTML documentation+    myHooks   = simpleUserHooks { postHaddock = myDocs }++    -- cobbled together from the source of Distribution.Simple.Haddock+myDocs _ flags pkg_descr lbi = do+    let verbosity = fromFlag (haddockVerbosity flags)+    let distPref  = fromFlag (haddockDistPref flags)+    let target    = haddockPref distPref pkg_descr </> "Documentation.html"+    +    let srcFiles  = extraSrcFiles $ localPkgDescr $ lbi+    let source    = buildDir lbi </> "doc" </> "Documentation.html"+    +    setupMessage verbosity "Installing extra documentation for" $+        packageId pkg_descr+    putStrLn (concat srcFiles) -- copyFile source target
+ docs/Documentation.html view
@@ -0,0 +1,588 @@+<!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>+  <title>Documentation for the &quot;operational&quot; package</title>+  <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, 24 Jan 2010 11:57:24 +0100" />+  <link rel="stylesheet" href="docbook.css" type="text/css" />+</head>+<body>+<h1 class="title">Documentation for the &quot;operational&quot; package</h1>+<div id="TOC"+><ul+  ><li+    ><a href="#introduction"+      >Introduction</a+      ></li+    ><li+    ><a href="#using-this-library"+      >Using this Library</a+      ><ul+      ><li+	><a href="#changes-to-the-Program-type"+	  >Changes to the <code+	    >Program</code+	    > type</a+	  ></li+	><li+	><a href="#efficiency"+	  >Efficiency</a+	  ></li+	><li+	><a href="#monad-transformers"+	  >Monad Transformers</a+	  ></li+	><li+	><a href="#alternatives-to-monad-transformers"+	  >Alternatives to Monad Transformers</a+	  ></li+	></ul+      ></li+    ><li+    ><a href="#design-and-implementation"+      >Design and Implementation</a+      ><ul+      ><li+	><a href="#proof-of-the-monad-laws-sketch"+	  >Proof of the monad laws (Sketch)</a+	  ></li+	><li+	><a href="#monad-transformers-1"+	  >Monad Transformers</a+	  ></li+	></ul+      ></li+    ><li+    ><a href="#other-design-choices"+      >Other Design Choices</a+      ><ul+      ><li+	><a href="#recursive-type-definitions-with-Program"+	  >Recursive type definitions with <code+	    >Program</code+	    ></a+	  ></li+	></ul+      ></li+    ></ul+  ></div+>+<p+><em+  >The HTML version of this document is generated automatically from the corresponding markdown file, don't change it!</em+  ></p+><div id="introduction"+><h1+  ><a href="#TOC"+    >Introduction</a+    ></h1+  ><p+  >This package is based on <a href="http://themonadreader.wordpress.com/2010/01/26/issue-15/"+    >&quot;The Operational Monad Tutorial&quot;</a+    > and this documentation describes its extension to a production-quality library. In other words, the &quot;magic&quot; gap between relevant paper and library implementation is documented here.</p+  ><p+  >Take not 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+  ></div+><div id="using-this-library"+><h1+  ><a href="#TOC"+    >Using this Library</a+    ></h1+  ><p+  >To understand what's going on, you'll have to read &quot;The Operational Monad Tutorial&quot;. Here, I will first and foremost note the changes with respect to the tutorial.</p+  ><p+  >Several advanced example monads demonstrate how to put this library to good use. They are located in the <a href="./examples"+    ><code+      >./docs/examples</code+      ></a+    > folder.</p+  ><div id="changes-to-the-Program-type"+  ><h2+    ><a href="#TOC"+      >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; returning a type</p+    ><pre+    ><code+      >data Prompt instr a where+    Return :: a -&gt; Prompt instr a+    (:&gt;&gt;=) :: instr a -&gt; (a -&gt; Program instr b) -&gt; Prompt instr b+</code+      ></pre+    ><p+    >which is much like the old <code+      >Program</code+      > type, except that <code+      >Then</code+      > was renamed to <code+      >(:&gt;&gt;=)</code+      >. The name <code+      >Prompt</code+      > was chosen in homage to the <a href="http://hackage.haskell.org/package/MonadPrompt" title="Ryan Ingram's Monad Prompt Package."+      ><code+	>MonadPrompt</code+	> package</a+      >.</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 -&gt; (Stack Int -&gt; a)+interpret = eval . view+    where+    eval :: Prompt StackInstruction a -&gt; (Stack Int -&gt; a)+    eval (Push a :&gt;&gt;= is) stack     = interpret (is ()) (a:stack)+    eval (Pop    :&gt;&gt;= is) (a:stack) = interpret (is a ) stack+    eval (Return a)       stack     = a+</code+      ></pre+    ><p+    >So-called &quot;view functions&quot; 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+    ></div+  ><div id="efficiency"+  ><h2+    ><a href="#TOC"+      >Efficiency</a+      ></h2+    ><p+    >The <code+      >Program</code+      > type supports <code+      >(&gt;&gt;=)</code+      > in constant time, albeit with the big caveat that this is only the case when not used in a persistent fashion. However, this is much less a restriction with monads than it would be with lists and <code+      >(++)</code+      >.</p+    ><p+    >More precisely, consider</p+    ><pre+    ><code+      >leftAssociative :: Int -&gt; StackProgram Int+leftAssociative 0 = return 1+leftAssociative n = leftAssociative (n-1) &gt;&gt;= push+</code+      ></pre+    ><p+    >and the expression</p+    ><pre+    ><code+      >interpret (leftAssociative n) []+</code+      ></pre+    ><p+    >Evaluating this will now take O(n) instead of O(n^2) time for the old <code+      >Program</code+      > type from the tutorial. However, persistent use like</p+    ><pre+    ><code+      >let p  = leftAssociative n+    v1 = view p+    v2 = view p+    v3 = view p+in v1 `seq` v2 `seq` v3+</code+      ></pre+    ><p+    >will now 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.</p+    ></div+  ><div id="monad-transformers"+  ><h2+    ><a href="#TOC"+      >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 &gt;&gt;= lift . g  =  lift (m &gt;&gt;= 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 entirely clear 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 -&gt; ListT m a -&gt; PlusI m a++type ListT m a = ProgramT (PlusI m) m a++runList :: Monad m =&gt; ListT m a -&gt; m [a]+runList = eval &lt;=&lt; viewT+    where+    eval :: Monad m =&gt; PromptT (PlusI m) m a -&gt; m [a]+    eval (Return x)        = return [x]+    eval (Zero     :&gt;&gt;= g) = return []+    eval (Plus m n :&gt;&gt;= g) =+        liftM2 (++) (runList (m &gt;&gt;= g)) (runList (n &gt;&gt;= g))+</code+      ></pre+    ></div+  ><div id="alternatives-to-monad-transformers"+  ><h2+    ><a href="#TOC"+      >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 -&gt; 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 -&gt; ErrorI e ()+    Catch :: ErrorI e a -&gt; (e -&gt; ErrorI e a) -&gt; ErrorI e a+</code+      ></pre+    ><p+    >The &quot;sum of signatures&quot; 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 &#65533; la carte."+      >Wouter Swierstra's &quot;Data Types a la carte&quot;</a+      >. Time will tell which has more merit; for now I have opted for a seamless interaction with monad transformers.</p+    ></div+  ></div+><div id="design-and-implementation"+><h1+  ><a href="#TOC"+    >Design and Implementation</a+    ></h1+  ><div id="proof-of-the-monad-laws-sketch"+  ><h2+    ><a href="#TOC"+      >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+    ><tr class="header"+      ><th align="left"+	></th+	><th align="center"+	></th+	></tr+      ><tr class="odd"+      ><td align="left"+	><code+	  >&gt;&gt;=</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+      ></table+    ><p+    >Then, the <code+      >view</code+      > function becomes</p+    ><pre+    ><code+      >view (return a)        = Return a+view (return a  &gt;&gt;= g) = g a                           -- left unit+view ((m &gt;&gt;= f) &gt;&gt;= g) = view (m &gt;&gt;= (\x -&gt; f x &gt;&gt;= g) -- associativity+view (i         &gt;&gt;= g) = i :&gt;&gt;= g+view  i                = i :&gt;&gt;= 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+      >&gt;&gt;=</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  =&gt;   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 -&gt; NF instr a+    (:&gt;&gt;=') :: instr a -&gt; (a -&gt; NF instr b) -&gt; 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) &gt;&gt;= g = g a+    (m :&gt;&gt;=' f) &gt;&gt;= g = m :&gt;&gt;= (\x -&gt; f x &gt;&gt;= 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 -&gt; NF instr a+normalize (m &gt;&gt;= g)  = normalize m &gt;&gt;=' normalize g+normalize (return a) = Return' a+normalize  i         = i :&gt;&gt;=' Return'+</code+      ></pre+    ><p+    >which has the now obvious property that</p+    ><pre+    ><code+      >e1 ~ e2  =&gt;  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) +=&gt; view e1 = view e2+</code+      ></pre+    ><p+    >(for some suitable extension of <code+      >normalize</code+      > to the <code+      >Prompt</code+      > type.) But since <code+      >view</code+      > only uses monad laws to rewrite its argument, we also have</p+    ><pre+    ><code+      >e1 ~ view e1  =&gt;  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+    ></div+  ><div id="monad-transformers-1"+  ><h2+    ><a href="#TOC"+      >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 &quot;first instruction&quot; no longer applies. Namely, we have</p+    ><pre+    ><code+      >m  =  return m &gt;&gt;= id  =  lift (return m) &gt;&gt;= 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 &gt;&gt;= g+= lift m &gt;&gt;= (\x -&gt; lift (return (g x)) &gt;&gt;= id)+= (lift m &gt;&gt;= lift . return . g) &gt;&gt;= id+= lift (m &gt;&gt;= return . g) &gt;&gt;= id+</code+      ></pre+    ><p+    >(To be continued.)</p+    ></div+  ></div+><div id="other-design-choices"+><h1+  ><a href="#TOC"+    >Other Design Choices</a+    ></h1+  ><div id="recursive-type-definitions-with-Program"+  ><h2+    ><a href="#TOC"+      >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 &quot;unties&quot; 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 -&gt; unimo a -&gt; 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 -&gt; Program PlusI a -&gt; 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+    ></div+  ></div+>+</body>+</html>+
+ docs/Documentation.md view
@@ -0,0 +1,248 @@+% Documentation for the "operational" package+% Heinrich Apfelmus+% Sun, 24 Jan 2010 11:57:24 +0100++  [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 not 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". 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. They are located in the [`./docs/examples`](./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; returning a type++    data Prompt instr a where+        Return :: a -> Prompt instr a+        (:>>=) :: instr a -> (a -> Program instr b) -> Prompt instr b++which is much like the old `Program` type, except that `Then` was renamed to `(:>>=)`. The name `Prompt` was chosen in homage to the [`MonadPrompt` package][prompt].+ +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 :: Prompt 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+----------+The `Program` type supports `(>>=)` in constant time, albeit with the big caveat that this is only the case when not used in a persistent fashion. However, this is much less a restriction with monads than it would be with lists and `(++)`.++More precisely, consider++    leftAssociative :: Int -> StackProgram Int+    leftAssociative 0 = return 1+    leftAssociative n = leftAssociative (n-1) >>= push++and the expression++    interpret (leftAssociative n) []++Evaluating this will now take O(n) instead of O(n^2) time for the old `Program` type from the tutorial. However, persistent use like++    let p  = leftAssociative n+        v1 = view p+        v2 = view p+        v3 = view p+    in v1 `seq` v2 `seq` v3++will now take O(n) time for each call of `view` instead of O(n) the first time and O(1) for the other calls.+++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 entirely clear 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 => PromptT (PlusI m) m a -> m [a]+        eval (Return x)        = return [x]+        eval (Zero     :>>= g) = return []+        eval (Plus m n :>>= g) =+            liftM2 (++) (runList (m >>= g)) (runList (n >>= g))+++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 `Prompt` 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.+
+ docs/Makefile view
@@ -0,0 +1,12 @@+######################################################################+### Documentation and examples++.PHONY: doc++doc: Documentation.html+Documentation.html : Documentation.md docbook.css +	pandoc --standalone --toc --css=docbook.css "$<" > "$@"++clean:+	rm Documentation.html+
+ docs/docbook.css view
@@ -0,0 +1,35 @@+body {+    font-family: Verdana, sans-serif;+    width: 43em;+    margin: 1ex auto 1ex;+}++pre {+    font-family: monospace;+    font-size: 1em;+    display: block;+    padding: 10px;+    border: 1px solid #bbb;+    background-color: #eee;+    color: #000;   +    overflow: auto;+    border-radius: 2.5px;+    -moz-border-radius: 2.5px;+    margin: 0.5em 2em;+}++h1 { font-size:150%; }+h2 { font-size:120%; }++a {+    text-decoration: none;+    border-bottom: 1px dotted #000;+    color: #333;+}++a:hover {+    background-color: #777;+    color: #fff;+}++        
+ docs/examples/ListT.hs view
@@ -0,0 +1,56 @@+{------------------------------------------------------------------------------+    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 => PromptT (MPlus m) m a -> m [a]+    eval (Return x)         = return [x]+    eval (MZero     :>>= g) = return []+    eval (MPlus m n :>>= g) =+        liftM2 (++) (runListT (m >>= g)) (runListT (n >>= g))++testListT :: IO [()]+testListT = runListT $ do+    k <- choice [1..5]+    lift . print $ "You've chosen the number: " ++ show k+    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)
+ docs/examples/LogicT.hs view
@@ -0,0 +1,86 @@+{------------------------------------------------------------------------------+    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, FlexibleInstances #-}+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 => PromptT (MPlus m) m a -> m (Maybe (a, LogicT m a))+    eval (MZero     :>>= g) = return Nothing+    eval (MPlus m n :>>= g) = do+        ma <- split (m >>= g)+        case ma of+            Nothing     -> split (n >>= g)+            Just (a,m') -> return $ Just (a, m' `mplus` (n >>= g))+                                --            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'++
+ docs/examples/PoorMansConcurrency.hs view
@@ -0,0 +1,63 @@+{------------------------------------------------------------------------------+    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, FlexibleInstances #-}+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 => Prompt (ProcessI m) a -> [Process m a] -> m ()+    run (Return _)      xs = return ()                 -- process finished+    run (Lift m :>>= g) xs = m >>= \a ->               -- switch process+                             schedule (xs ++ [g a])+    run (Stop   :>>= g) xs = schedule xs               -- process halts+    run (Fork p :>>= g) xs = schedule (xs ++ [x2,x1])  -- fork new process+        where x1 = g (); x2 = p >>= g++    -- 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
+ docs/examples/State.hs view
@@ -0,0 +1,60 @@+{------------------------------------------------------------------------------+    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 :: Prompt (StateI s) a -> (s -> a)+    eval (Return x)     = const x+    eval (Get   :>>= g) = \s -> evalState (g s ) s+    eval (Put s :>>= g) = \_ -> evalState (g ()) 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 => PromptT (StateI s) m a -> (s -> m a)+    eval (Return x)     = \_ -> return x+    eval (Get   :>>= g) = \s -> evalStateT (g s ) s+    eval (Put s :>>= g) = \_ -> evalStateT (g ()) s++testStateT = evalStateT $ do+    x <- get+    lift $ putStrLn "Hello StateT"+    put (x+1)
+ docs/examples/WebSessionState.lhs view
@@ -0,0 +1,102 @@+#!/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, FlexibleInstances #-}+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 :: Prompt WebI H.Html -> [String] -> [String] -> CGI H.Html+    eval (Return html)         log _      = return html+    eval (Ask question :>>= g) log (l:ls) = -- replay answer from log+        replay (g l) log ls+    eval (Ask question :>>= g) 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}
+ operational.cabal view
@@ -0,0 +1,43 @@+Name:               operational+Version:            0.1.0.0+Synopsis:           Implement monads by specifying operational semantics.+Description:+  Tiny library for implementing monads by specifying the primitive instructions+  and their operational semantics. The monad laws will hold automatically.+  Can also be used to define monad transformers,+  the lifting laws are, again, automatic.+  +  Accompanies the article: \"The Operational Monad Tutorial\",+  published in Issue 15 of The Monad.Reader <http://themonadreader.wordpress.com/2010/01/26/issue-15/>.+  +  Related packages: MonadPrompt <http://hackage.haskell.org/package/MonadPrompt>.+  +Category:           Control, Monads+License:            BSD3+License-file:       LICENSE+Author:             Heinrich Apfelmus+Maintainer:         Heinrich Apfelmus <apfelmus quantentunnel de>+Copyright:          (c) Heinrich Apfelmus 2010+Homepage:           http://projects.haskell.org/operational/+Stability:          Provisional++build-type:         Simple+cabal-version:      >= 1.6+extra-source-files: docs/*.css+                    docs/*.html+                    docs/*.md+                    docs/Makefile+                    docs/examples/*.hs+                    docs/examples/*.lhs+                    +source-repository head+    type:           darcs+    location:       http://code.haskell.org/operational+++Library+    hs-source-dirs:     src+    build-depends:      base == 4.* , mtl == 1.1.*+    ghc-options:        -Wall+    extensions:         GADTs+    exposed-modules:    Control.Monad.Operational
+ src/Control/Monad/Operational.hs view
@@ -0,0 +1,159 @@+{-# LANGUAGE GADTs #-}+{-| Implement monads by specifying primitive instructions and their operational semantics.++This package is based on the \"The Operational Monad Tutorial\", published in Issue 15 of The Monad.Reader <http://themonadreader.wordpress.com/>.++You are reading the API reference. For more thorough documentation including design and implementation notes as well as a correctness proof, please consult the included @doc/Documentation.html@.++This API reference includes only basic example code. More intricate examples are available in the @doc/examples@ directory.++-}+module Control.Monad.Operational (+    -- * Basic usage+    Program, singleton, Prompt, view,+    -- $example+    +    -- * Monad transformer+    ProgramT, PromptT(..), viewT+    -- $exampleT+    +    ) where++import Control.Monad.Identity+import Control.Monad.Trans+import Control.Applicative++{------------------------------------------------------------------------------+   Program+------------------------------------------------------------------------------}+{-| The abstract data type 'Program instr a' represents programs.++    * The type constructor @instr :: * -> *@ indexes the primitive instructions.+    +    * @a@ is the return type of a program.+    +    @'Program' instr@ is always a monad and+    automatically obeys the monad laws.+-}+type Program instr a = ProgramT instr Identity a++-- | View type for inspecting the first instruction.+--   It has two constructors 'Return' and @:>>=@.+--   (For technical reasons, they are documented at 'PromptT'.)+type Prompt instr a  = PromptT instr Identity a++-- | View function for inspecting the first instruction.+view :: Program instr a -> Prompt instr a+view = runIdentity . viewT++{- $example++/Example/++Stack machine from \"The Operational Monad Tutorial\".++@+    data StackInstruction a where+        Push :: Int -> StackInstruction ()+        Pop  :: StackInstruction Int+@++@+    type StackProgram a = Program StackInstruction a+@++@+    interpret :: StackProgram a -> (Stack Int -> a)+    interpret = eval . view+        where+        eval :: Prompt 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+@++Note that since 'Prompt' is a GADT, the type annotation for @eval@ is mandatory.++-}++{------------------------------------------------------------------------------+    ProgramT - monad transformer+------------------------------------------------------------------------------}+{-| The abstract data type @'ProgramT' instr m a@ represents programs.++    * The type constructor @instr :: * -> *@ indexes the primitive instructions.+    +    * @m@ is the base monad, embedded with 'lift'.++    * @a@ is the return type of a program.+    +    @'ProgramT' instr m@ is a monad transformer and+    automatically obey both the monad and the lifting laws.+-}+data ProgramT instr m a where+    Lift   :: m a -> ProgramT instr m a+    Bind   :: ProgramT instr m b -> (b -> ProgramT instr m a)+           -> ProgramT instr m a+    Instr  :: instr a -> ProgramT instr m a++instance Monad m => Monad (ProgramT instr m) where+    return = Lift . return+    (>>=)  = Bind++instance MonadTrans (ProgramT instr) where+    lift   = Lift++instance Monad m => Functor (ProgramT instr m) where+    fmap   = liftM++instance Monad m => Applicative (ProgramT instr m) where+    pure   = return+    (<*>)  = ap++-- | Program made from a single primitive instruction.+singleton :: instr a -> ProgramT instr m a+singleton = Instr++-- | View type for inspecting the first instruction.+data PromptT instr m a where+    Return :: a -> PromptT instr m a+    (:>>=) :: instr b -> (b -> ProgramT instr m a ) -> PromptT instr m a++-- | View function for inspecting the first instruction.+viewT :: Monad m => ProgramT instr m a -> m (PromptT instr m a)+viewT (Lift m)                = m >>= return . Return+viewT ((Lift m)     `Bind` g) = m >>= viewT . g+viewT ((m `Bind` g) `Bind` h) = viewT (m `Bind` (\x -> g x `Bind` h))+viewT ((Instr i)    `Bind` g) = return (i :>>= g)+viewT (Instr i)               = return (i :>>= return)++{- $exampleT++/Example/++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 => PromptT (PlusI m) m a -> m [a]+        eval (Return x)        = return [x]+        eval (Zero     :>>= g) = return []+        eval (Plus m n :>>= g) =+            liftM2 (++) (runList (m >>= g)) (runList (n >>= g))+@++Note that since 'Prompt' is a GADT, the type annotation for @eval@ is mandatory.++-}