(* 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 *)