X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=blobdiff_plain;f=monad_transformers.mdwn;h=3b5312c155d0a1552bfd9d0cd4f8b400aea8b2e6;hp=9f26d615fe3869836d1254b7ecded0ae67a11176;hb=18ab1e2a09a6c59fd4385c7f83ba2acf11b90daa;hpb=ad057986df1ce9482dc2aa3ced6db6be072893e5

diff --git a/monad_transformers.mdwn b/monad_transformers.mdwn
index 9f26d615..3b5312c1 100644
--- a/monad_transformers.mdwn
+++ b/monad_transformers.mdwn
@@ -116,6 +116,10 @@ Then if you want to use an `S`-specific monad like `puts succ` inside `MS`, you'
 
 	# MS.(...elevate (S.puts succ) ...)
 
+Each monad transformer's `elevate` function will be defined differently. They have to obey the following laws:
+
+*	`Outer.elevate (Inner.unit a) <~~> Outer.unit a`
+*	`Outer.elevate (Inner.bind u f) <~~> Outer.bind (Outer.elevate u) (fun a -> Outer.elevate (f a))`
 
 We said that when T encloses M, you can rely on T's interface to be most exposed. That is intuitive. What you cannot also assume is that the implementing type has a Tish structure surrounding an Mish structure. Often it will be reverse: a ListT(Maybe) is implemented by a `'a list option`, not by an `'a option list`. Until you've tried to write the code to a monadic transformer library yourself, this will probably remain counter-intuitive. But you don't need to concern yourself with it in practise. Think of what you have as a ListT(Maybe); don't worry about whether the underlying implementation is as an `'a list option` or an `'a option list` or as something more complicated.
 
@@ -156,7 +160,7 @@ When Maybe is on the inside, on the other hand, a failure means the whole comput
 	Exception: Failure "bye".
 -->
 
-Here's an example wrapping List around Maybe, and vice versa:
+Here's an example wrapping Maybe around List, and vice versa:
 
 	# module LM = List_monad.T(Maybe_monad);;
 	# module ML = Maybe_monad.T(List_monad);;
@@ -248,7 +252,7 @@ then `list_bind u f` would be `concat [[]; [2]; [2; 4]; [2; 4; 8]]`, that is `[2
 	                         |  |
 	                         4  8
 
-Except, as we mentioned, our implementation of the Tree monad incorporates an Optionish layer too. So `f' 2` should be not `Leaf 2` but `Some (Leaf 2)`. What if `f'` also mapped `1` to `None` and `4` to `Some (Node (Leaf 2, Leaf 4))`. Then binding the tree `Node (Leaf 1, Node (Leaf 2, Leaf 4))` to `f'` would delete thr branch corresponding to the original `Leaf 1`, and would splice in the results for `f' 2` and `f' 4`, yielding:
+Except, as we mentioned, our implementation of the Tree monad incorporates an Optionish layer too. So `f' 2` should be not `Leaf 2` but `Some (Leaf 2)`. What if `f'` also mapped `1` to `None` and `4` to `Some (Node (Leaf 2, Leaf 4))`. Then binding the tree `Node (Leaf 1, Node (Leaf 2, Leaf 4))` (really the tree itself needs to be wrapped in a `Some`, too, but let me neglect that) to `f'` would delete the branch corresponding to the original `Leaf 1`, and would splice in the results for `f' 2` and `f' 4`, yielding:
 
 	 .                        
 	_|__  >>=  f' ~~>