From: Jim Date: Sat, 4 Apr 2015 15:41:31 +0000 (-0400) Subject: Merge branch 'working' X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=commitdiff_plain;h=9fa2ebb32617d76b9dde81b4d6adfada2f15d48d;hp=16c94123a19df2a70cb8c11d661bdbd2f72b4e10 Merge branch 'working' * working: add/update monad code --- diff --git a/code/arith1.ml b/code/arith1.ml new file mode 100644 index 00000000..71f66cd4 --- /dev/null +++ b/code/arith1.ml @@ -0,0 +1,39 @@ +type num = int -> int +type contents = Num of num | Op of (num -> num) | Op2 of (num -> num -> num) +type tree = Leaf of contents | Branch of tree * tree | Error + +let mid a = fun _ -> a;; (* K *) + +let map2 f u v x = f (u x) (v x);; (* S *) + +let rec eval (t:tree) = match t with + | Leaf _ -> t + | Branch (Leaf (Op f), b2) -> (match (eval b2) with + | Leaf (Num n) -> Leaf (Num (f n)) + | _ -> Error) + | Branch (Leaf (Op2 f), b2) -> (match (eval b2) with + | Leaf (Num n) -> Leaf (Op (f n)) + | _ -> Error) + | Branch (b1, b2) -> eval (Branch (eval b1, eval b2)) + | _ -> Error + + +(* to get an arithmetic function, type, e.g., "(+)". + to get times instead of comment, type "( * )". *) + +(* Encoding of (+ 1 (* (/ 6 x) 4)) *) +let t1 = Branch ((Branch ((Leaf (Op2 (map2 (+)))), + (Leaf (Num (mid 1))))), + (Branch ((Branch ((Leaf (Op2 (map2 ( * ))), + (Branch ((Branch ((Leaf (Op2 (map2 (/)))), + (Leaf (Num (mid 6))))), + (Leaf (Num (fun x -> x)))))))), + (Leaf (Num (mid 4))))));; + + +(* try + +match eval t1 with Leaf (Num f) -> f 2;; + +The answer should be 13. +*) diff --git a/exercises/_assignment8.mdwn b/exercises/_assignment8.mdwn index 1c7fdfaf..8e28810c 100644 --- a/exercises/_assignment8.mdwn +++ b/exercises/_assignment8.mdwn @@ -1,84 +1,46 @@ - Binding more than one variable at a time ---------------------------------------- -It requires some cleverness to use the link monad to bind more than -one variable at a time. Whereas in the standard Reader monad a single -environment can record any number of variable assignments, because -Jacobson's monad only tracks a single dependency, binding more than -one pronoun requires layering the monad. (Jacobson provides some -special combinators, but we can make do with the ingredients already -defined.) - -Let's take the following sentence as our target, with the obvious -binding relationships: - -
-    John believes Mary said he thinks she's cute.
-     |             |         |         |
-     |             |---------|---------|
-     |                       |
-     |-----------------------|
-
- -It will be convenient to -have a counterpart to the lift operation that combines a monadic -functor with a non-monadic argument: - -
-    let g f v = ap (unit f) v;;
-    let g2 u a = ap u (unit a);;
-
- -As a first step, we'll bind "she" by "Mary": +1. Jacobson's reader monad only allows for establishing a single binding +relationship at a time. It requires considerable cleverness to deploy +her combinators in a way that establishes multiple binding +relationships, as in -
-believes (z said (g2 (g thinks (g cute she)) she) mary) john
+    John_x thinks Mary_y said he_x likes her_y.
 
-~~> believes (said (thinks (cute mary) he) mary) john
-
+See her 1999 paper for details. -As usual, there is a trail of *g*'s leading from the pronoun up to the -*z*. Next, we build a trail from the other pronoun ("he") to its -binder ("John"). +Here is [[code for the simple arithmetic reader monad discussed in the +lecture notes|code/arith1.ml]]. It computes +`\x. (+ 1 (* (/ 6 x) 4))`. Your task is to modify it to compute +`\x\y.(+ 1 (* (/ 6 x) y))`. You will need to modify five lines. +The first one is the type of a boxed int. Instead of `type num = int +-> int`, you'll need -
-believes
-  said 
-    thinks (cute she) he
-    Mary
-  John
+    type num = int -> int -> int
 
-believes
-  z said
-    (g2 ((g thinks) (g cute she))) he
-    Mary
-  John
+The second and third are the definitions of mid and map2.  The fourth
+is the one that encodes the variable x, the line that begins `(Leaf
+(Num (fun x -> ...`.  The fifth line you need to modify is the one
+that replaces "4" with "y".  When you have these lines modified,
+you should be able to execute the following expression:
 
-z believes
-  (g2 (g (z said)
-         (g (g2 ((g thinks) (g cute she))) 
-            he))
-      Mary)
-  John
-
+ # match eval t2 with Leaf (Num f) -> f 2 4;; + - : int = 13 -In the first interation, we build a chain of *g*'s and *g2*'s from the -pronoun to be bound ("she") out to the level of the first argument of -*said*. +2. Based on the evaluator code from the assignment from week 7, +enhance the code to handle an arbitrary set of free variables. +Return to the original code (before executing the modifications +required by exercise 1). -In the second iteration, we treat the entire structure as ordinary -functions and arguments, without "seeing" the monadic region. Once -again, we build a chain of *g*'s and *g2*'s from the currently -targeted pronoun ("he") out to the level of the first argument of -*believes*. (The new *g*'s and *g2*'s are the three leftmost). +Start like this: -
-z believes (g2 (g (z said) (g (g2 ((g thinks) (g cute she))) he)) mary) john
+    type env = string -> int
+    type num = env -> int
+    let g = fun var -> match var with "x" -> 2 | "y" -> 4 | _ -> 0;;
 
-~~> believes (said (thinks (cute mary) john) mary) john
-
+When you have it working, try -Obviously, we can repeat this strategy for any configuration of pronouns -and binders. + # match eval t2 with Leaf (Num f) -> f g;; + - : int = 13 diff --git a/index.mdwn b/index.mdwn index 3dd65ea8..a71eb4db 100644 --- a/index.mdwn +++ b/index.mdwn @@ -163,10 +163,21 @@ Practical advice for working with OCaml and/or Haskell (will be posted someday); (**Week 8**) Thursday March 26 -> Topics: [[Safe division with monads|topics/week8_safe_division_with_monads]] +> Topics: [[Safe division with monads|topics/week8_safe_division_with_monads]]; [[Long but useful ramble|topics/week8_ramble]] (**Week 9**) Thursday April 2 -> Topics: Programming with mutable state; the State monad; using multiple monads together +> Topics: [[Using the OCaml Monad library|/topics/week9_using_monad_library]]; the State monad; Programming with mutable state; Using multiple monads together + +> Here are some OCaml libraries: [[Juli8|code/juli8.ml]] and [[Monad|code/monad.ml]]. We'll write up explanations of these soon. But quickly, before you `#use "juli8.ml"`, you have to run this in your OCaml session. (I have these lines in my `~/.ocamlinit` file, so they run every time OCaml starts up: + +> #load "str.cma";; +> module Std = struct +> include Pervasives +> module List = List +> module Random = Random +> module String = String +> end + +
+(+ 1 (* (/ 6 2) 4)) in tree format:
 
  ___________
  |         |
@@ -46,12 +51,13 @@ _|__    ___|___
         /  6
-This computation should reduce to 13. But given a specific reduction -strategy, we can watch the order in which the computation proceeds. -Following on the lambda evaluator developed during the previous -homework, let's adopt the following reduction strategy: +No matter which arithmetic operation we begin with, this computation +should eventually reduce to 13. Given a specific reduction strategy, +we can watch the order in which the computation proceeds. Following +on the lambda evaluator developed during the previous homework, let's +adopt the following reduction strategy: - In order to reduce (head arg), do the following in order: + In order to reduce an expression of the form (head arg), do the following in order: 1. Reduce head to h' 2. Reduce arg to a'. 3. If (h' a') is a redex, reduce it. @@ -78,10 +84,12 @@ processing the left branch, then moving to the right branch, and finally processing the results of the two subcomputation. (This is called depth-first postorder traversal of the tree.) +[diagram with arrows traversing the tree] + It will be helpful to see how the types change as we make adjustments. type num = int - type contents = Num of num | Op of (num -> num -> num) + type contents = Num of num | Op2 of (num -> num -> num) type tree = Leaf of contents | Branch of tree * tree Never mind that these types will allow us to construct silly @@ -93,9 +101,10 @@ the entire tree is replaced by a single integer (namely, 13). Now we replace the number 2 with 0: -
+
+
  ___________
  |         |
 _|__    ___|___
@@ -110,7 +119,7 @@ _|__    ___|___
 

 
 When we reduce, we get quite a ways into the computation before things
-go south:
+break down:
 
     1. Reduce head (+ 1) to itself
     2. Reduce arg ((* ((/ 6) 0)) 3)
@@ -121,14 +130,21 @@ go south:
                    2. Reduce arg 0 to itself
                    3. Reduce ((/ 6) 0) to ACKKKK
 
-This is where we replace `/` with `safe-div`.  This means changing the
-type of the arithmetic operators from `int -> int -> int` to 
-`int -> int -> int option`; and since we now have to anticipate the
-possibility that any argument might involve division by zero inside of
-it, here is the net result for our types:
+This is where we replace `/` with `safe-div`.  
+Safe-div returns not an int, but an int option.  If the division goes
+through, the result is Just n, where n is the integer result.
+But if the division attempts to divide by zero, the result is Nothing.
+
+We could try changing the type of the arithmetic operators from `int
+-> int -> int` to `int -> int -> int option`; but since we now have to
+anticipate the possibility that any argument might involve division by
+zero inside of it, it would be better to prepare for the possibility
+that any subcomputation might return here is the net result for our
+types.  The easy way to do that is to change (only) the type of num
+from int to int option, leaving everying else the same:
 
     type num = int option
-    type contents = Num of num   | Op of (num -> num -> num)
+    type contents = Num of num   | Op2 of (num -> num -> num)
     type tree = Leaf of contents | Branch of tree * tree
 
 The only difference is that instead of defining our numbers to be
@@ -151,9 +167,10 @@ is the ⇧ and the map2 function from the notes on safe division:
 Then we lift the entire computation into the monad by applying ⇧ to
 the integers, and by applying `map2` to the operators:
 
-
+
+
      ___________________
      |                 |
   ___|____         ____|_____
@@ -208,6 +225,7 @@ till it comes out of the result faucet at the top of the tree.
 
 ## Information flowing in the other direction: top to bottom
 
+We can think of this application as facilitating information flow.
 In the save-div example, a subcomputation created a message that
 propagated upwards to the larger computation:
 
@@ -252,28 +270,35 @@ embedded position.  Whatever the value of the argument that the lambda
 form combines with, that is what will be substituted in for free
 occurrences of that variable within the body of the lambda.
 
+## Binding
+
 So our next step is to add a (primitive) version of binding to our
-computation.  Rather than anticipating any number of binding
-operators, we'll allow for just one binding dependency for now.
+computation.  We'll allow for just one binding dependency for now, and
+then generalize later.
 
-This example is independent of the safe-div example, so we'll return
-to a situation in which the Maybe monad hasn't been added.  So the
-types are the ones where numbers are just integers, not int options.
-(In a couple of weeks, we'll start combining monads into a single
-system; if you're impatient, you might think about how to do that now.)
+Binding is independent of the safe division, so we'll return to a
+situation in which the Maybe monad hasn't been added.  One of the nice
+properties of programming with monads is that it is possible to add or
+subtract layers according to the needs of the moment.  Since we need
+simplicity, we'll set the Maybe monad aside for now.
+
+So we'll go back to the point where the num type is simple int, not
+int options.
 
     type num = int
 
-And the computation will be without the map2 or the ⇧ from the option
+And we'll start with the computation the map2 or the ⇧ from the option
 monad.
 
 As you might guess, the technique we'll use to arrive at binding will
 be to use the Reader monad, defined here in terms of m-identity and bind:
 
-    α --> int -> α
+    α ==> int -> α     (* The ==> is a Kleisli arrow *)
     ⇧a = \x.a
     u >>= f = \x.f(ux)x
-    map2 u v = \x.ux(vx)
+    map  f u = \x.f(ux)
+    map2 f u v = \x.f(ux)(vx)
+
 
 A boxed type in this monad will be a function from an integer to an
 object in the original type.  The unit function ⇧ lifts a value `a` to
@@ -301,9 +326,10 @@ That is, `num` is once again replaced with the type of a boxed int.
 When we were dealing with the Maybe monad, a boxed int had type `int
 option`.  In this monad, a boxed int has type `int -> int`.
 
-
+
+
      __________________
      |                |
   ___|____        ____|_____
@@ -324,7 +350,7 @@ in argument position, the code we want in order to represent the
 variable will have the type of a boxed int, namely, `int -> int`.  So
 we have the following:
 
-    x (i:int):int = i
+    x = (\fun (i:int) = i)
 
 That is, variables in this system denote the indentity function!
 
@@ -333,10 +359,12 @@ from any integer `x` to `(+ 1 (* (/ 6 x)) 4)`.
 
 Take a look at the definition of the reader monad again.  The
 midentity takes some object `a` and returns `\x.a`.  In other words,
-`⇧a = Ka`, so `⇧ = K`.  Likewise, `map2` for this monad is the `S`
-combinator.  We've seen this before as a strategy for translating a
-lambda abstract into a set of combinators.  Here is a part of the
-general scheme for translating a lambda abstract into Combinatory
+`⇧a = Ka`, so `⇧ = K`.  Likewise, the reason the `map2` function
+looked familiar is that it is essentially the `S` combinator.
+
+We've seen this before as a strategy for translating a binding
+construct into a set of combinators.  To remind you, here is a part of
+the general scheme for translating a lambda abstract into Combinatory
 Logic.  The translation function `[.]` translates a lambda term into a
 term in Combinatory Logic:
 
@@ -345,24 +373,25 @@ term in Combinatory Logic:
     [\a.M] = K[M]       (assuming a not free in M)
     [\a.(MN)] = S[\a.M][\a.N]
 
-The reason we can make do with this subset of the full function is
-that we're making the simplifying assumption that there is at most a
-single lambda involved.  So here you see the I (the translation of the
-bound variable), the K and the S.
-
+The reason we can make do with this subset of the full translation
+scheme is that we're making the simplifying assumption that there is
+at most a single lambda involved.  So once again we have the identity
+function I as the translation of the bound variable, K as the function
+governing expressions that don't contain an instance of the bound
+variable, S as the operation that manages the combination of complex
+expressions.  
 
 ## Jacobson's Variable Free Semantics as a Reader Monad
 
-We've designed the discussion so far to make the following claim as
-easy to show as possible: Jacobson's Variable Free Semantics
-(e.g., Jacobson 1999, [Towards a
-Variable-Free
+We've designed the presentation above to make it as easy as possible
+to show that Jacobson's Variable Free Semantics (e.g., Jacobson 1999,
+[Towards a Variable-Free
 Semantics](http://www.springerlink.com/content/j706674r4w217jj5/))
-is a reader monad.
+implements a reader monad.
 
 More specifically, it will turn out that Jacobson's geach combinator
 *g* is exactly our `lift` operator, and her binding combinator *z* is
-exactly our `bind` (though with the arguments reversed)!
+exactly our `bind` (though with the arguments reversed).
 
 Jacobson's system contains two main combinators, *g* and *z*.  She
 calls *g* the Geach rule, and *z* performs binding.  Here is a typical
@@ -370,9 +399,9 @@ computation.  This implementation is based closely on email from Simon
 Charlow, with beta reduction as performed by the on-line evaluator:
 
 
-; Analysis of "Everyone_i thinks he_i left"
-let g = \f g x. f (g x) in
-let z = \f g x. f (g x) x in
+; Jacobson's analysis of "Everyone_i thinks he_i left"
+let g = \f u. \x. f (u x) in
+let z = \f u. \x. f (u x) x in
 let he = \x. x in
 let everyone = \P. FORALL x (P x) in
 
@@ -381,55 +410,51 @@ everyone (z thinks (g left he))
 ~~>  FORALL x (thinks (left x) x)
 

 
-Several things to notice: First, pronouns once again denote identity functions.
-As Jeremy Kuhn has pointed out, this is related to the fact that in
-the mapping from the lambda calculus into combinatory logic that we
-discussed earlier in the course, bound variables translated to I, the
-identity combinator (see additional comments below).  We'll return to
-the idea of pronouns as identity functions in later discussions.
+Two things to notice: First, pronouns once again denote identity
+functions, just as we saw in the reader monad in the previous section.
 
 Second, *g* plays the role of transmitting a binding dependency for an
 embedded constituent to a containing constituent.
 
-Third, one of the peculiar aspects of Jacobson's system is that
-binding is accomplished not by applying *z* to the element that will
-(in some pre-theoretic sense) bind the pronoun, here, *everyone*, but
-rather by applying *z* instead to the predicate that will take
-*everyone* as an argument, here, *thinks*.  
-
-The basic recipe in Jacobson's system, then, is that you transmit the
+The basic recipe in Jacobson's system is that you transmit the
 dependence of a pronoun upwards through the tree using *g* until just
 before you are about to combine with the binder, when you finish off
-with *z*.  (There are examples with longer chains of *g*'s below.)
-
-Jacobson's *g* combinator is exactly our `lift` operator: it takes a
-functor and lifts it into the monad.  
-Furthermore, Jacobson's *z* combinator, which is what she uses to
-create binding links, is essentially identical to our reader-monad
-`bind`!  
+with *z*.  Here is an example with a longer chain of *g*'s:
 
 
-everyone (z thinks (g left he))
-
-~~> forall w (thinks (left w) w)
-
 everyone (z thinks (g (t bill) (g said (g left he))))
 
-~~> forall w (thinks (said (left w) bill) w)
+~~> FORALL x (thinks (said (left x) bill) x)
 

 
-(The `t` combinator is given by `t x = \xy.yx`; it handles situations
-in which English word order places the argument (in this case, a
-grammatical subject) before the predicate.)
+If you compare Jacobson's values for *g* and *z* to the functions in
+the reader monad given above, you'll see that Jacobson's *g*
+combinator is exactly our `map` operator.  Furthermore, Jacobson's *z*
+combinator is identital to `>>=`, except with the order of the
+arguments reversed (i.e., `(z f u) == (u >>= f)`).
 
-So *g* is exactly `lift` (a combination of `bind` and `unit`), and *z*
-is exactly `bind` with the arguments reversed.  It appears that
+(The `t` combinator in the derivations above is given by `t x =
+\xy.yx`; it handles situations in which English word order reverses
+the usual function/argument order.)
+
+In other words, 
 Jacobson's variable-free semantics is essentially a Reader monad.
 
+One of the peculiar aspects of Jacobson's system is that binding is
+accomplished not by applying *z* to the element that will (in some
+pre-theoretic sense) bind the pronoun, here, *everyone*, but rather by
+applying *z* instead to the predicate that will take *everyone* as an
+argument, here, *thinks*.
+
+
 ## The Reader monad for intensionality
 
-Now we'll look at using monads to do intensional function application.
-This is just another application of the Reader monad, not a new monad.
+[This section has not been revised since 2010, so there may be a few
+places where it doesn't follow the convetions we've adopted this time;
+nevertheless, it should be followable.]
+
+Now we'll look at using the Reader monad to do intensional function application.
+
 In Shan (2001) [Monads for natural
 language semantics](http://arxiv.org/abs/cs/0205026v1), Ken shows that
 making expressions sensitive to the world of evaluation is conceptually
diff --git a/topics/week9_using_monad_library.mdwn b/topics/week9_using_monad_library.mdwn
new file mode 100644
index 00000000..d9820acd
--- /dev/null
+++ b/topics/week9_using_monad_library.mdwn
@@ -0,0 +1,223 @@
+[[!toc levels=2]]
+
+## What functions are in the OCaml Monad modules? ##
+
+If you want to see the "signature" of some OCaml library or "module" --- that is, a list of the types it exports, and also of the types of function values (and other values) that it exports, you can do this.
+
+First, if you know that the module uses a specific *named* module type, here's what to do. An example is that modules you create using `Monad.Reader(struct type env = ... end).M` --- really you have to do that in two steps, first say `module R_E = Monad.Reader(struct type env = ... end)`, next write `R_E.M`; but for brief reading I'll just write `Monad.Reader(struct type env = ... end).M` --- these modules will all have the module type `Monad.READER`. We can see an expansion of `Monad.READER` by writing:
+
+    module type SOMETHING = sig include Monad.READER end
+
+Then OCaml will respond:
+
+    module type SOMETHING =
+      sig
+        type env
+
+        type 'a t
+        type 'a result = env -> 'a
+        val run : 'a t -> 'a result
+
+        val map : ('a -> 'b) -> 'a t -> 'b t
+        val mid : 'a -> 'a t
+        val map2 : ('a -> 'b -> 'c) -> 'a t -> 'b t -> 'c t
+        val mapply : ('a -> 'b) t -> 'a t -> 'b t
+        val ( >> ) : 'a t -> 'b t -> 'b t
+        val ( << ) : 'a t -> 'b t -> 'a t
+        val ( >>= ) : 'a t -> ('a -> 'b t) -> 'b t
+        val ( >=> ) : ('a -> 'b t) -> ('b -> 'c t) -> 'a -> 'c t
+        val ( <=< ) : ('b -> 'c t) -> ('a -> 'b t) -> 'a -> 'c t
+        val join : 'a t t -> 'a t
+        val ignore : 'a t -> unit t
+        val seq : 'a t list -> 'a list t
+        val seq_ignore : unit t list -> unit t
+        val do_when : bool -> unit t -> unit t
+        val do_unless : bool -> unit t -> unit t
+
+        val ask : env t
+        val asks : (env -> 'a) -> 'a t
+        val shift : (env -> env) -> 'a t -> 'a t
+      end
+
+Here I've reordered the elements a bit from OCaml's actual presentation to make it easier to explain them. First, there is the type of the `env` that you will supply. In this signature it's listed abstractly (no concrete definition of the type is supplied, it's just declared that it exists), but in practice this type will be unified with the envionment type that you supply. Next there is the abstract type `'a t`. This is the main type of the Reader Monad. Behind the scenes it will be the same as the type `'a result`, that is a function from `env`s to `'a`s. But OCaml keeps the type `'a t` abstract, and only exposes the actual implementation of the type when you apply the `run` function to `'a t` values. The `run` function is for most Monads just implemented as an identity function. Its effect is primarily to shift between the abstract type, whose definition OCaml treats as private, and the concrete implementation of that type, named `'a result`. Note that even though the `'a t`s and `'a result`s will usually be represented by the same structures in OCaml's memory, our library insists that you only use the `'a t` version for the monadic functions like `map` and `>>=` and so on. Also there is no translation function that lets you take an `'a result` that you've built by hand and convert it to an `'a t`. You have to build your `'a t`s using the operations that the Monad library provides for doing so.
+
+The next block of stuff in the `Monad.READER` module type are functions common to all monads. Some monads (such as List and Option) additionally have `mzero : 'a t` and some related operations. Finally, at the end are the operations specific to the Reader monad. These have mostly been given the same names as they have in Haskell's monad libraries. Here is a quick explanation:
+
+*   `ask` is a Reader monadic value that, when given an `env`, returns that very `env` as its payload. So its type is an `env t`. And it is implemented as `fun e -> e`.
+
+*   `asks` is a variant of `ask`. Haskell several times uses the convention that where `blah` is some operation that gives you some raw value, `blahs` is a variant that gives you the result of applying some *s*elector function or handler to the raw value. In this case, `asks` takes a parameter, which is a function that operates on `env`s and gives some result. `asks handler` then constitutes an `'a t`, where `'a` is the type of the handler's result. For example, if my environments are associations of some sort between `char`s and `int`s, and `lookup 'x'` is a function that takes an `env` as a further argument and returns what `int` that environment associates the char `'x'` with, then:
+
+        let getx = asks (lookup 'x')
+
+    will declare an `int t` that, when supplied with an environment, returns the `int` that that environment associates the `char` `'x'` with.
+
+*   `shift` is a function that takes two arguments, an "`env`-shifting" function and some Reader monadic value. It returns a new Reader monadic value that, when supplied with an `env`, will process the original monadic value only with the `env` shifted in the specified way. (Haskell calls the `shift` operation `local`, but I thought it would be a bit better to call it `shift` --- enough of an improvement to justify changing the name.)
+
+    For example, if `insert 'x' 1` is a function that operates on `env`s and gives a new `env` which now associates the char `'x'` with `1`, then:
+
+        let letx xint body = shift (insert 'x' xint) body
+
+    will declare an operation that takes an `int` `xint` and a monadic value `body`, and evaluates `body` in the context let x = xint in .... If we wanted instead to have a version which accepted not an `int` but rather an `int` in a Reader monad box, we could write instead:
+
+        let letx xx body = xx >>= fun xint -> shift (insert 'x' xint) body
+
+
+### Examples ###
+
+Here are some examples of using the Reader Monad modules to evaluate some simple expressions using bound variables. First, you could look at [[this Haskell code|/code/reader1.hs]]. It `import`s the `Control.Monad.Reader` library, which is where Haskell's Reader monad can be found. It declares an `Env` type that we'll implement as a simple *function* from `Char`s to `Int`s. Then it defines an "empty" environment `env0`, and a function `insert` for adding new bindings to an `env`. Next, we make a general function `getint` that can create monadic values like the `getx` illustrated above. We show how to use `getx` and `gety` to write monadic versions of `y + x` and `3 + x`. Next, we define a `letx` function as illustrated above (the second version, that takes a monadic value `xx` as its argument). We show how to use this to write a monadic version of `let x = 2 in y + x`. The final line of the file applies `runReader` to the monadic value we've built --- this is Haskell's way of doing what we do in OCaml with `run`, namely to remove the abstraction barrier and see what concrete type is really constituting our `Reader Env a`s --- and we supply it with the empty environment, which will be sufficient since the expression we're interpreting has no free variables. Haskell binds the variable `res` to the result. You can run this code inside `ghci` by typing `:load /path/to/reader1.hs`. (You could also say `:add ...` instead of `:load ...`.) Then type `res`, and Haskell will report back `5`.
+
+[[This OCaml code|/code/reader1.ml]] does exactly the same thing only using our OCaml monad libraries instead. The biggest difference from the Haskell version is in the first few lines, where we have to generate a Reader monad module parameterized on the `env` type that we intend to work with.
+
+Here's a more complicated example. This time we want to be able to bind variables to lambda abstracts as well as to `int`s. So our `env` type will need to be more complex; it will have to associate `char`s with a disjoint sum of `int`s and lambda abstracts. Now what will the type of the lambda abstracts be? Let's just restrict our attention to abstracts whose bodies return `int`s. But they might get those `int`s by performing operations on bound variables, so the body expressions need to be interpreted monadically, as `int Reader`s. We'll construe the whole lambda abstract as a  function from `int Reader`s (that is, the monadic values which are provided as arguments to the lambda abstract) to their results, so the lambda abstract will have the type `int Reader -> int Reader`. In OCaml that will be `int R.t -> int R.t`, and in Haskell `Reader Env Int -> Reader Env Int`. Since variables can be bound to either `int`s or to lambda abstracts, we declare our environments like this in OCaml:
+
+    type bound = Int of int | Fun of (int R.t -> int R.t)
+    type env = char -> bound
+
+and like this in Haskell:
+
+    data Bound = Int Int | Fun (Reader Env Int -> Reader Env Int)
+    type Env = Char -> Bound
+
+There is a tricky issue in the OCaml case, though, in that when working with OCaml, we have to *generate* our R Reader monad module, parameterized on the type of the `env`, but here we see that we need access to the *type* `'a R.t` from the generated R module in order to declare the `env`. Fortunately, it is possible to do this, by having the module that declares the `env` and the module that has our Reader monad in it be mutually recursively defined. The first few lines of [[this OCaml code|/code/reader2.ml]] do the tricky work.
+
+After that, our [[Haskell code|/code/reader2.hs]] and [[OCaml code|/code/reader2.ml]] proceed basically the same, allowing for the difference in syntax and vocabulary between Haskell and OCaml. The `getint` function works like before, except now we have to pull the int out from behind the `Int` constructor of our disjoint sum type `bound`. We have a parallel `getfun` function. Then we interpret the variable `x` using the monadic value `getint 'x'`, and we interpret the variable `f` using the monadic value `getfun 'f'`. The `letx` operation is similarly adjusted, and we also have a parallel `letf`.
+
+The really new thing in this code, compared to the previous example, is our definition of a monadic value to interpret the lambda abstract `\y -> y + x`, that `f` gets bound to. And also our interpretation of the expression `f 3`, which looks up a function that the variable `f` is bound to, and then applies it to (a monadically-lifted version of) `3`. (We have the argument be monadically lifted so that we could also say, for example, `f y`.)
+
+
+## OK, what else is in the OCaml Monad modules? ##
+
+I won't give an exhaustive list here. But here is the output of `module type SOMETHING = sig include Monad.BLAH end` for some of the `BLAH`s:
+
+
+    module type STATE =
+      sig
+        type store
+        type 'a t
+        type 'a result = store -> 'a * store
+        (* plus the other usual monadic stuff, and: *)
+        val get : store t
+        val gets : (store -> 'a) -> 'a t
+        val modify : (store -> store) -> unit t
+        val put : store -> unit t
+      end
+
+The `store` type has to be provided by you, when you generate the module, similarly to as in the Reader monad. The `'a result` type shows the real definition of an `'a State` type, otherwise kept abstract as `'a t`. Instead of the special operations `ask` and so on that the Reader monad has, State has the operations `get`, `gets`, `modify`, and `put`. The first two work just like `ask` and `asks` did for the Reader monad. The third one works *similarly* to `shift` for the Reader monad, with the crucial difference that the rebinding that `shift` introduces is in effect only for the `body` argument of the `shift` operation. Outside of that `body`, we revert to the originally supplied `env`. But notice that `modify` doesn't take any `body` argument. `modify` introduces changes to the supplied `store` that once introduced *stay in place*, until we manually change them again. Thus with the Reader monad you'd do things like this:
+
+    R.(xx >>= fun x -> ... shift (insert ...) body >>= fun y -> (* now we're using the unshifted env *) ...)
+
+With the State monad you'd instead do things like this:
+
+    S.(xx >>= fun x -> ... modify (fun old_store -> new_store) >>= fun () -> (* we continue using the modified store, until it's modified once again *) ...)
+
+Since the pattern `... >>= fun () -> ...` or `... >>= fun variable_you_never_use -> ...` occurs often when working with monads, there's a shorthand: you can instead say `... >> ...`, with `>>` in place of `>>= fun pattern ->`.
+
+Here's another monad module signature:
+
+    module type WRITER =
+      sig
+        type log
+        type 'a t
+        type 'a result = 'a * log
+        (* plus the other usual monadic stuff, and: *)
+        val listen : 'a t -> ('a * log) t
+        val listens : (log -> 'b) -> 'a t -> ('a * 'b) t
+        val tell : log -> unit t
+        val censor : (log -> log) -> 'a t -> 'a t
+      end
+
+Writer is very similar to Reader: first, it is parameterized on something like an `env`, here called a `log`. (A typical implementation for `log` would be the `string` type.) Second, the Writer operations `listen`, `listens`, and `censor` parallel the Reader operations `ask`, `asks`, and `shift`. But one difference is that with Writer, you cannot choose what initial `env` (`log`) to supply. You always begin with the `empty` `log` (such as `""` for `string`s). A second difference is that the types differ. Compare:
+
+    module type READER =
+      sig
+        ...
+        val ask : env t
+        val asks : (env -> 'a) -> 'a t
+        val shift : (env -> env) -> 'a t -> 'a t
+      end
+
+Whereas Writer's `sensor` and Reader's `shift` have isomorphic types, there is some extra complextity to Writer's `listen` and `listens`, compared to `ask` and `asks`. What this extra complexity means is that for `Writer`, listening happens only in a local context. You can't `listen` to what got written to the log before you installed your `listen`ing tap. But you can return payloads that are dependent on what you've heard in the local context.
+
+Unlike Reader, Writer also has a `tell` operation, which is akin to the `put` operation in the State monad. The difference is that the `tell` function takes a `log` as argument and *appends* that to the existing `log`. You can't erase or overwrite elements already in the `log`; you can only append to it. However, if you like, you can `censor` the log in arbitrary ways and use that when interpreting other monadic values locally. After that local context, though, we return to the original log (
+
+Here's a complex example that illustrates this. First we will use the helper function `String.upper` (from "juli8.ml") and a second helper function that we define like this:
+
+    let bracket log = "{" ^ log ^ "}"
+
+Next, we construct some monadic values and reveal them at the end using `run`:
+
+    module W_L = Monad.Writer(struct
+      type log = string
+      let empty = ""
+      let append s1 s2 = if s1 = "" then s2 else if s2 = "" then s1 else s1 ^ " " ^ s2
+    end)
+    module W = Writer1.M;;
+    W.(let xx = tell "one" >> listens bracket (tell "two" >> mid 10) in
+       let yy = censor String.upper (tell "zero" >> listens bracket xx) in
+       let zz = tell "before" >> yy >>= fun y -> tell "after" >> mid y in
+       ...);;
+
+The monadic value `xx` writes "one" to the log, then discards the resulting `()` payload (it continues `>> ...` rather than `>>= fun var -> ...`). Then we have a use of `listens`. This will evaluate its body `tell "two" >> mid 10` and return as payload a pair of the body's original payload and a bracketed copy of the local log. Thus the payload of `listens bracket (tell "two" >> mid 10)` will be `(10, "{two}")`. The `"one"` that got written to the log earlier isn't accessible to `listens`; however it does stay in the log. Hence the result of `run xx`, showing first the payload and then the log, would be:
+
+    - : (int * string) W.result = ((10, "{two}"), "one two")
+
+Now `yy` uses that `xx` monadic value to illustrate the use of `censor`. Here we have `censor` apply `String.upper` to the log generated in the local context it's applied to, hence the result of  `run yy` would be:
+
+    - : ((int * string) * string) W.result = (((10, "{two}"), "{one two}"), "ZERO ONE TWO three")
+
+The final value `zz` shows what happens to entries written to the log before and after the `censor`ing that occurs in `yy`, namely nothing. That is, `run zz` is:
+
+- : ((int * string) * string) W.result = (((10, "{two}"), "{one two}"), "before ZERO ONE TWO after")
+
+Let's look at some more familiar monad signatures. Here is one:
+
+    module type OPTION =
+      sig
+        type 'a t
+        type 'a result = 'a option
+        (* plus the other usual monadic stuff, and: *)
+        val mzero : 'a t
+        val guard : bool -> unit t
+        val test : ('a option -> bool) -> 'a t -> 'a t
+      end
+
+This is what's exposed in the `Monad.Option.M` module (with `Option` and `List`, you can also leave off the initial `Monad.`). In the parent `Monad.Option` module itself, there are many more operations. Similarly, `Monad.List` (aka just `List`) exposes many more operations than `Monad.List.M` does. The `.M` modules restrict us to just the monadic interface. Unlike Reader and State and Writer, the Option and List monads don't need to be parameterized on environments or anything else of that sort. The Option monad has three additional monadic operations, analogues of which are also all present in List. First, there is the `mzero` monadic value, implemented as `None` and satisfying the Monad Laws for `mzero` we explained elsewhere. The key one to remember is that `mzero` aborts a chain of composed Kleisli functions. That is, `mzero >>= anything` is always `mzero`. `guard` takes a boolean argument and if its false, gives `mzero`. If the argument is true, it just gives the uninteresting `mid ()`, hence the typical way to use `guard` is as:
+
+    module O = Option.M;;    
+    O.(guard some_bool_expr >> more_monadic_stuff)
+
+If `some_bool_expr` is true, then this will ignore its payload and go on to compute `more_monadic_stuff`; if it's false, then the whole chain gets ignored because of the distinctive behavior of `mzero`.
+
+The third special operation in the Option monad is `test`. This lets you supply a function that takes an ordinary `'a option` type (that is, one where the "abstraction curtain" imposed by the `'a O.t` type is not in place) and returns a bool. Then you take an Option monadic value (one where the "abstraction curtain" *is* in place). OCaml will temporarily remove the abstraction curtain on the second argument and see how the function you supplied assesses it. If the result is `true`, then the result is identical to that Option monadic value, unaltered. If the result is `false`, then the result is `mzero`. (For those of you who know Frank Veltman's work on dynamic semantics for epistemic modals, this is a key component.)
+
+Here is the List monadic interface:
+
+    module type LIST =
+      sig
+        type 'a t
+        type 'a result = 'a list
+        (* plus the other usual monadic stuff, and: *)
+        val mzero : 'a t
+        val guard : bool -> unit t
+        val test : ('a list -> bool) -> 'a t -> 'a t
+        val ( ++ ) : 'a t -> 'a t -> 'a t
+        val pick : 'a t -> ('a * 'a t) t
+      end
+
+The `mzero` and `guard` and `test` operations work analogously to the ones in the Option monad. The `++` (infix) operation is like `List.append` (OCaml also uses `@` for that), with the difference that `++` is defined on the abstract List monadic values of type `'a List.M.t`, not the OCaml native lists (with the "abstraction curtain" removed). In Haskell, `++` works on either native lists or elements of the List monad, because Haskell doesn't distinguish them. Haskell doesn't impose an abstraction curtain in the case of its List and Maybe monads. `pick` is an operation that transforms (the abstract version of) `[1; 2; 3]` to (the abstract version of) `[(1, [2; 3]); (2, [1; 3]); (3, [1; 2])]`.
+
+Here is another monadic interface:
+
+    module type TREE =
+      sig
+        type 'a tree
+        type 'a t
+        type 'a result = 'a tree
+        (* plus the other usual monadic stuff, and: *)
+        val ( ++ ) : 'a t -> 'a t -> 'a t
+      end
+
+This is the signature/module type for the Monad.LTree module. ("LTree" for *leaf-labeled* trees.)
+
+You can create leaf-only trees using the monadic function `mid`. You can join two trees together using the function `++`, paralleling the one in List. Note that in the Tree case, unlike the List case, `++` is not associative: `xx ++ (yy ++ zz)` is not the same as `(xx + yy) ++ zz`. Nor is there any `mzero` for trees as implemented by this module.
+