X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=blobdiff_plain;f=week7.mdwn;h=ba845b2960f4a1540d3a7991c9d1b9f1e90711aa;hp=62ef89f0ab8b7a2faa8fecf83aa141963d523a54;hb=966f3179a2866846d6b0e347b32ebe56da8cdd5e;hpb=7834e35d4a2de390ce6a1e9113186dcbb9c07a6f

diff --git a/week7.mdwn b/week7.mdwn
index 62ef89f0..ba845b29 100644
--- a/week7.mdwn
+++ b/week7.mdwn
@@ -48,22 +48,24 @@ that provides at least the following three elements:
   use a container metaphor: if `x` has type `int option`, then `x` is
   a box that (may) contain an integer.
 
-    type 'a option = None | Some of 'a;;
+    `type 'a option = None | Some of 'a;;`
 
 * A way to turn an ordinary value into a monadic value.  In Ocaml, we
   did this for any integer n by mapping an arbitrary integer `n` to
   the option `Some n`.  To be official, we can define a function
   called unit:
 
-    let unit x = Some x;;
-    val unit : 'a -> 'a option = <fun>
+    `let unit x = Some x;;`
+
+    `val unit : 'a -> 'a option = <fun>`
 
     So `unit` is a way to put something inside of a box.
 
 * A bind operation (note the type):
 
-     let bind m f = match m with None -> None | Some n -> f n;;
-     val bind : 'a option -> ('a -> 'b option) -> 'b option = <fun>
+     `let bind m f = match m with None -> None | Some n -> f n;;`
+
+     `val bind : 'a option -> ('a -> 'b option) -> 'b option = <fun>`
 
      `bind` takes two arguments (a monadic object and a function from
      ordinary objects to monadic objects), and returns a monadic
@@ -75,7 +77,7 @@ that provides at least the following three elements:
      Then the second argument uses `x` to compute a new monadic
      value.  Conceptually, then, we have
 
-    let bind m f = (let x = unwrap m in f x);;
+    `let bind m f = (let x = unwrap m in f x);;`
 
     The guts of the definition of the `bind` operation amount to
     specifying how to unwrap the monadic object `m`.  In the bind
@@ -112,17 +114,17 @@ val unit : 'a -> 'a option = <fun>
 - : int option = Some 2
 </pre>
 
-	The parentheses is the magic for telling Ocaml that the
-	function to be defined (in this case, the name of the function
-	is `*`, pronounced "bind") is an infix operator, so we write
-	`m * f` or `( * ) m f` instead of `* m f`.
+The parentheses is the magic for telling Ocaml that the
+function to be defined (in this case, the name of the function
+is `*`, pronounced "bind") is an infix operator, so we write
+`m * f` or `( * ) m f` instead of `* m f`.
 
 *    Associativity: bind obeys a kind of associativity, like this:
 
-    (m * f) * g == m * (fun x -> f x * g)
+    `(m * f) * g == m * (fun x -> f x * g)`
 
-    If you don't understand why the lambda form is necessary, you need
-    to look again at the type of bind.  This is important.  
+    If you don't understand why the lambda form is necessary (the "fun
+    x" part), you need to look again at the type of bind.
 
     For an illustration of associativity in the option monad:
 
@@ -133,15 +135,15 @@ Some 3 * (fun x -> unit x * unit);;
 - : int option = Some 3
 </pre>
 
-	Of course, associativity must hold for arbitrary functions of
-	type `'a -> M 'a`, where `M` is the monad type.  It's easy to
-	convince yourself that the bind operation for the option monad
-	obeys associativity by dividing the inputs into cases: if `m`
-	matches `None`, both computations will result in `None`; if
-	`m` matches `Some n`, and `f n` evalutes to `None`, then both
-	computations will again result in `None`; and if the value of
-	`f n` matches `Some r`, then both computations will evaluate
-	to `g r`.
+Of course, associativity must hold for arbitrary functions of
+type `'a -> M 'a`, where `M` is the monad type.  It's easy to
+convince yourself that the bind operation for the option monad
+obeys associativity by dividing the inputs into cases: if `m`
+matches `None`, both computations will result in `None`; if
+`m` matches `Some n`, and `f n` evalutes to `None`, then both
+computations will again result in `None`; and if the value of
+`f n` matches `Some r`, then both computations will evaluate
+to `g r`.
 
 *    Right identity: unit is a right identity for bind.  That is, 
      `m * unit == m` for all monad objects `m`.  For instance,
@@ -162,7 +164,7 @@ arguments of a monoid operation) the two arguments of the bind are of
 different types.  But if we generalize bind so that both arguments are
 of type `'a -> M 'a`, then we get plain identity laws and
 associativity laws, and the monad laws are exactly like the monoid
-laws (see <http://www.haskell.org/haskellwiki/Monad_Laws>).
+laws (see <http://www.haskell.org/haskellwiki/Monad_Laws>, near the bottom).
 
 
 Monad outlook
@@ -189,8 +191,11 @@ intensionality](http://parles.upf.es/glif/pub/sub11/individual/bena_wint.pdf),
 though without explicitly using monads.
 
 All of the code in the discussion below can be found here: [[intensionality-monad.ml]].
-To run it, download the file, start Ocaml, and say `# #use
-"intensionality-monad.ml";;`. 
+To run it, download the file, start Ocaml, and say 
+
+    # #use "intensionality-monad.ml";;
+
+Note the extra `#` attached to the directive `use`.
 
 Here's the idea: since people can have different attitudes towards
 different propositions that happen to have the same truth value, we