``` # let ( * ) m f = match m with None -> None | Some n -> f n;;
@@ -136,19 +136,19 @@ val unit : 'a -> 'a option =
- : int option = None
```
-The parentheses is the magic for telling Ocaml that the +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: +* **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 (the "fun - x" part), you need to look again at the type of bind. + 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. - Some examples of associativity in the option monad: + Some examples of associativity in the option monad:
``` # Some 3 * unit * unit;;
@@ -168,7 +168,7 @@ is `*`, pronounced "bind") is an infix operator, so we write
```
Of course, associativity must hold for arbitrary functions of -type `'a -> M 'a`, where `M` is the monad type. It's easy to +type `'a -> 'a m`, 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 @@ -177,8 +177,8 @@ 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, +* **Right identity: unit is a right identity for bind.** That is, + `m * unit == m` for all monad objects `m`. For instance,
``` # Some 3 * unit;;
@@ -196,7 +196,7 @@ serving as the left and right identity.  That is, temporarily using
presented here, a monad is not exactly a monoid, because (unlike the
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
+of type `'a -> 'a m`, then we get plain identity laws and
associativity laws, and the monad laws are exactly like the monoid
laws (see , near the bottom).

@@ -225,9 +225,9 @@ intensionality](http://parles.upf.es/glif/pub/sub11/individual/bena_wint.pdf),

All of the code in the discussion below can be found here: [[intensionality-monad.ml]].

Note the extra `#` attached to the directive `use`.

@@ -283,15 +283,15 @@ as possible.

So here's what we do:

-In Ocaml, we'll use integers to model possible worlds:
+In OCaml, we'll use integers to model possible worlds:

-    type s = int;;
-    type e = char;;
-    type t = bool;;
+	type s = int;;
+	type e = char;;
+	type t = bool;;

Characters (characters in the computational sense, i.e., letters like
`'a'` and `'b'`, not Kaplanian characters) will model individuals, and
-Ocaml booleans will serve for truth values.
+OCaml booleans will serve for truth values.

type 'a intension = s -> 'a;;
@@ -324,7 +324,7 @@ We'll assume that this and the other laws always hold.

We now build up some extensional meanings:

-    let left w x = match (w,x) with (2,'c') -> false | _ -> true;;
+	let left w x = match (w,x) with (2,'c') -> false | _ -> true;;

This function says that everyone always left, except for Cam in world
2 (i.e., `left 2 'c' == false`).
@@ -348,16 +348,16 @@ So Ann left in world 1, but Cam didn't leave in world 2.

A transitive predicate:

-    let saw w x y = (w < 2) && (y < x);;
-    extapp (extapp saw bill) ann 1;; (* true *)
-    extapp (extapp saw bill) ann 2;; (* false *)
+	let saw w x y = (w < 2) && (y < x);;
+	extapp (extapp saw bill) ann 1;; (* true *)
+	extapp (extapp saw bill) ann 2;; (* false *)

In world 1, Ann saw Bill and Cam, and Bill saw Cam.  No one saw anyone
in world two.

Good.  Now for intensions:

-    let intapp fn arg w = fn w arg;;
+	let intapp fn arg w = fn w arg;;

The only difference between intensional application and extensional
application is that we don't feed the evaluation world to the argument.
--
2.11.0

```