X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=blobdiff_plain;f=week7.mdwn;h=ba845b2960f4a1540d3a7991c9d1b9f1e90711aa;hp=a78a77e291a6d71883a8acadd5bdc3fa9f2769c4;hb=966f3179a2866846d6b0e347b32ebe56da8cdd5e;hpb=ef954bbcb3b568413e2dd48374dbeb7201ccd4bb diff --git a/week7.mdwn b/week7.mdwn index a78a77e2..ba845b29 100644 --- a/week7.mdwn +++ b/week7.mdwn @@ -105,26 +105,26 @@ them from hurting the people that use them or themselves. 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 = 
-    # let unit x = Some x;;
-    val unit : 'a -> 'a option = 
-    # unit 2 * unit;;
-    - : int option = Some 2
-    
- - 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`. +
+# let ( * ) m f = match m with None -> None | Some n -> f n;;
+val ( * ) : 'a option -> ('a -> 'b option) -> 'b option = 
+# let unit x = Some x;;
+val unit : 'a -> 'a option = 
+# unit 2 * unit;;
+- : int option = Some 2
+
+ +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: @@ -135,15 +135,15 @@ Some 3 * (fun x -> unit x * unit);; - : int option = Some 3 - 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, @@ -164,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 ). +laws (see , near the bottom). Monad outlook @@ -191,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