added proto-monad

diff --git a/week6.mdwn b/week6.mdwn
index ac94b79..b97a09f 100644 (file)
--- a/week6.mdwn
+++ b/week6.mdwn
@@ -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
 
 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>
 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>
 
 *)
 </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.
 
 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)) = 
 
 <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)));;
 
 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
 
 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).