+# let divide num den = if den = 0 then None else Some (num/den);; +val divide : int -> int -> int option =+ +as basically a function from two integers to an integer, except with +this little bit of option frill, or option plumbing, on the side. + +A note on notation: Haskell uses the infix operator `>>=` to stand for `bind`. I really hate that symbol. Following Wadler, I prefer to infix five-pointed star, or on a keyboard, `*`. @@ -100,57 +109,82 @@ The Monad laws Just like good robots, monads must obey three laws designed to prevent them from hurting the people that use them or themselves. -* Left identity: unit is a left identity for the bind operation. - That is, for all `f:'a -> 'a M`, where `'a M` is a monadic - object, we have `(unit x) * f == f x`. For instance, `unit` is a - function of type `'a -> 'a option`, so we have +* **Left identity: unit is a left identity for the bind operation.** + That is, for all `f:'a -> 'a m`, where `'a m` is a monadic + object, we have `(unit x) * f == f x`. For instance, `unit` is a + function of type `'a -> 'a option`, so we have+

# let ( * ) m f = match m with None -> None | Some n -> f n;; val ( * ) : 'a option -> ('a -> 'b option) -> 'b option =- 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: +* **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: + Some examples of associativity in the option monad:# let unit x = Some x;; val unit : 'a -> 'a option = + +# unit 2;; +- : int option = Some 2 # unit 2 * unit;; - : int option = Some 2 + +# divide 6 2;; +- : int option = Some 3 +# unit 2 * divide 6;; +- : int option = Some 3 + +# divide 6 0;; +- : int option = None +# unit 0 * divide 6;; +- : int option = None

-Some 3 * unit * unit;; +# Some 3 * unit * unit;; - : int option = Some 3 -Some 3 * (fun x -> unit x * unit);; +# Some 3 * (fun x -> unit x * unit);; - : int option = Some 3 + +# Some 3 * divide 6 * divide 2;; +- : int option = Some 1 +# Some 3 * (fun x -> divide 6 x * divide 2);; +- : int option = Some 1 + +# Some 3 * divide 2 * divide 6;; +- : int option = None +# Some 3 * (fun x -> divide 2 x * divide 6);; +- : int option = None- 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 -> '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 +`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, +* **Right identity: unit is a right identity for bind.** That is, + `m * unit == m` for all monad objects `m`. For instance,

# Some 3 * unit;; - : int option = Some 3 +# None * unit;; +- : 'a option = NoneNow, if you studied algebra, you'll remember that a *monoid* is an @@ -162,9 +196,9 @@ 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

type 'a intension = s -> 'a;; @@ -286,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`). @@ -310,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.