X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=blobdiff_plain;f=intensionality-monad.ml;h=eebe5ee1f1334839c3ddce63b886282900325cb5;hp=2f30f8b73f3a4d66620296fd58d57561fb8cb12a;hb=2d5df0441175013c782ebee648a17043405ca251;hpb=5eb5b091a62e66068007e326cc97ea1faaad2960

diff --git a/intensionality-monad.ml b/intensionality-monad.ml
index 2f30f8b7..eebe5ee1 100644
--- a/intensionality-monad.ml
+++ b/intensionality-monad.ml
@@ -1,57 +1,45 @@
 (* This is the intensionality monad discussed in the lecture notes for week 7. *)
 
-type s = int;;
-type e = char;;
-type t = bool;;
+type s = int;; (* integers model possible worlds *)
+type e = char;; (* chars model individuals *)
+type t = bool;; (* booleans model truth values *)
 
-type 'a intension = s -> 'a;;
-let unit x (w:s) = x;;
-
-let ann = unit 'a';;
-let bill = unit 'b';;
-let cam = unit 'c';;
-
-let bind m f (w:s) = f (m w) w;;
-bind (unit 'a') unit 1;;
+let ann = 'a';;
+let bill = 'b';;
+let cam = 'c';;
 
-let left w x = match (w,x) with (2,'c') -> false | _ -> true;;
+let left1 (x:e) = true;; (* Everyone left *)
+let saw1 (x:e) (y:e) = y < x;; (* Ann saw Bill and Cam, and Bill saw Cam *)
 
-let extapp fn arg w = fn w (arg w);;
+left1 ann;;
+saw1 bill ann;;
+saw1 ann bill;;
 
-extapp left ann 1;;
+(* Now we make the extension of "leave" sensitive to the world of evaluation *)
+let left (x:e) (w:s) = match (x, w) with ('c', 2) -> false | _ -> true;;
 
-extapp left cam 2;;
+left ann 1;; (* Ann left in world 1 *)
+left cam 2;; (* Cam didn't leave in world 2 *)
 
-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 x y w = (w < 2) && (y < x);;
+saw bill ann 1;; (* Ann saw Bill in world 1 *)
+saw bill ann 2;; (* Ann didn't see Bill in world 2 *)
 
-let intapp fn arg w = fn w arg;;
-
-let lift pred w arg = bind arg (fun x w -> pred w x) w;;
+(* The intensionality reader-monad: *)
+type 'a intension = s -> 'a;;
+let unit x (w:s) = x;;
+let bind m f (w:s) = f (m w) w;;
+let lift2' f u v = bind u (fun x -> bind v (fun y -> f x y));;
 
-intapp (lift left) ann 1;; (* true: Ann still left in world 1 *)
-intapp (lift left) cam 2;; (* false: Cam still didn't leave in world 2 *)
+bind (unit ann) left 1;;
+bind (unit cam) left 2;;
 
-let lift2 pred w arg1 arg2 = 
-  bind arg1 (fun x -> bind arg2 (fun y w -> pred w x y)) w;;
-intapp (intapp (lift2 saw) bill) ann 1;;  (* true: Ann saw Bill in world 1 *)
-intapp (intapp (lift2 saw) bill) ann 2;;  (* false: No one saw anyone in world 2 *)
+lift2' saw (unit bill) (unit ann) 1;; 
+lift2' saw (unit bill) (unit ann) 2;;
 
-let think (w:s) (p:s->t) (x:e) = 
+let thinks (p:s->t) (x:e) (w:s) = 
   match (x, p 2) with ('a', false) -> false | _ -> p w;;
 
-intapp (lift (intapp think
-                     (intapp (lift left)
-                             (unit 'b'))))
-       (unit 'a') 
-1;; (* true *)
-
-intapp (lift (intapp think
-                     (intapp (lift left)
-                             (unit 'c'))))
-       (unit 'a') 
-1;; (* false *)
+bind (unit ann) (thinks (bind (unit bill) left)) 1;;
+bind (unit ann) (thinks (bind (unit cam) left)) 1;;
 
-let swap f x y = f y x;;
-bind cam (swap left) 2;; (* false *)