code/intensionality-monad.ml

   1 (* This is the intensionality monad discussed in the lecture notes for week 8. *)
   2
   3 type s = int;; (* integers model possible worlds *)
   4 type e = char;; (* chars model individuals *)
   5 type t = bool;; (* booleans model truth values *)
   6
   7 let ann = 'a';;
   8 let bill = 'b';;
   9 let cam = 'c';;
  10
  11 let left1 (x : e) = true;; (* Everyone left *)
  12 let saw1 (y : e) (x : e) = x < y;; (* Ann saw Bill and Cam, and Bill saw Cam *)
  13
  14 left1 ann;;      (* true *)
  15 saw1 bill ann;;  (* true *)
  16 saw1 ann bill;;  (* false *)
  17
  18 (* Now we make the extension of "leave" sensitive to the world of evaluation *)
  19 let left (x : e) (w : s) = match (x, w) with ('c', 2) -> false | _ -> true;;
  20
  21 left ann 1;; (* Ann left in world 1 *)
  22 left cam 2;; (* Cam didn't leave in world 2 *)
  23
  24 let saw (y : e) (x : e) (w : s) = (w < 2) && (x < y);;
  25 saw bill ann 1;; (* Ann saw Bill in world 1 *)
  26 saw bill ann 2;; (* Ann didn't see Bill in world 2 *)
  27
  28 (* The intensionality reader-monad *)
  29 type 'a intension = s -> 'a;;
  30 let mid x (w : s) = x;;
  31 let (>>=) xx k (w : s) = k (xx w) w;;
  32 let map2' f xx yy = xx >>= (fun x -> yy >>= (fun y -> f x y));;
  33
  34 (mid ann >>= left) 1;;              (* true *)
  35 (mid cam >>= left) 2;;              (* false *)
  36
  37 map2' saw (mid bill) (mid ann) 1;;  (* true *)
  38 map2' saw (mid bill) (mid ann) 2;;  (* false *)
  39
  40 let thinks (p : s->t) (x : e) (w : s) =
  41   match (x, p 2) with ('a', false) -> false | _ -> p w;;
  42
  43 (mid bill >>= left) 1;; (* true *)
  44 (mid cam >>= left) 1;;  (* true *)
  45 (mid ann >>= thinks (mid bill >>= left)) 1;; (* true *)
  46 (mid ann >>= thinks (mid cam >>= left)) 1;;  (* false *)
  47