(* This is the intensionality monad discussed in the lecture notes for week 8. *) type s = int;; (* integers model possible worlds *) type e = char;; (* chars model individuals *) type t = bool;; (* booleans model truth values *) let ann = 'a';; let bill = 'b';; let cam = 'c';; let left1 (x : e) = true;; (* Everyone left *) let saw1 (y : e) (x : e) = x < y;; (* Ann saw Bill and Cam, and Bill saw Cam *) left1 ann;; (* true *) saw1 bill ann;; (* true *) saw1 ann bill;; (* false *) (* 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;; left ann 1;; (* Ann left in world 1 *) left cam 2;; (* Cam didn't leave in world 2 *) let saw (y : e) (x : e) (w : s) = (w < 2) && (x < y);; saw bill ann 1;; (* Ann saw Bill in world 1 *) saw bill ann 2;; (* Ann didn't see Bill in world 2 *) (* The intensionality reader-monad *) type 'a intension = s -> 'a;; let mid x (w : s) = x;; let (>>=) xx k (w : s) = k (xx w) w;; let map2' f xx yy = xx >>= (fun x -> yy >>= (fun y -> f x y));; (mid ann >>= left) 1;; (* true *) (mid cam >>= left) 2;; (* false *) map2' saw (mid bill) (mid ann) 1;; (* true *) map2' saw (mid bill) (mid ann) 2;; (* false *) let thinks (p : s->t) (x : e) (w : s) = match (x, p 2) with ('a', false) -> false | _ -> p w;; (mid bill >>= left) 1;; (* true *) (mid cam >>= left) 1;; (* true *) (mid ann >>= thinks (mid bill >>= left)) 1;; (* true *) (mid ann >>= thinks (mid cam >>= left)) 1;; (* false *)