X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=blobdiff_plain;f=week6.mdwn;h=b97a09f3ff51f7655a30f486060afcd833ea3a50;hp=5898788187b1c1cf4fb5e53631f024aaee09103e;hb=48f733f96a60560cc42360cbfc890f6f9c529d91;hpb=177c81322f3487ac795fbcb58e8fb765bbc1f86d

diff --git a/week6.mdwn b/week6.mdwn
index 58987881..b97a09f3 100644
--- a/week6.mdwn
+++ b/week6.mdwn
@@ -200,7 +200,7 @@ let div (x:int) (y:int) =
                _ -> Some (x / y);;
 
 (*
-val div : int -> int -> int option = \<fun\>
+val div : int -> int -> int option = fun
 # div 12 3;;
 - : int option = Some 4
 # div 12 0;;
@@ -216,7 +216,7 @@ Error: This expression has type int option
 
 This starts off well: dividing 12 by 3, no problem; dividing 12 by 0,
 just the behavior we were hoping for.  But we want to be able to use
-the output of the safe division function as input for further division
+the output of the safe-division function as input for further division
 operations.  So we have to jack up the types of the inputs:
 
 <pre>
@@ -271,7 +271,7 @@ val add : int option -> int option -> int option = <fun>
 *)
 </pre>
 
-This works, but is somewhat disappointing: the `add` prediction
+This works, but is somewhat disappointing: the `add` operation
 doesn't trigger any presupposition of its own, so it is a shame that
 it needs to be adjusted because someone else might make trouble.
 
@@ -281,7 +281,8 @@ well chosen to resonate with linguists, but what can you do):
 
 <pre>
 let bind (x: int option) (f: int -> (int option)) = 
-  match x with None -> None | Some n -> f n;;
+  match x with None -> None | 
+               Some n -> f n;;
 
 let add (x: int option) (y: int option)  =
   bind x (fun x -> bind y (fun y -> Some (x + y)));;
@@ -301,7 +302,13 @@ let div (x: int option) (y: int option) =
 
 Compare the new definitions of `add` and `div` closely: the definition
 for `add` shows what it looks like to equip an ordinary operation to
-survive in a presupposition-filled world, and the definition of `div`
-shows exactly what extra needs to be added in order to trigger the
-no-division-by-zero presupposition.
+survive in dangerous presupposition-filled world.  Note that the new
+definition of `add` does not need to test whether its arguments are
+None objects or real numbers---those details are hidden inside of the
+`bind` function.
 
+The definition of `div` shows exactly what extra needs to be said in
+order to trigger the no-division-by-zero presupposition.
+
+For linguists: this is a complete theory of a particularly simply form
+of presupposition projection (every predicate is a hole).