(* This is the intensionality monad discussed in the lecture notes for week 7. *) type s = int;; type e = char;; type t = bool;; 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 left w x = match (w,x) with (2,'c') -> false | _ -> true;; let extapp fn arg w = fn w (arg w);; extapp left ann 1;; extapp left cam 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 intapp fn arg w = fn w arg;; let lift pred w arg = bind arg (fun x w -> pred w x) w;; 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 *) 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 *) let think (w:s) (p:s->t) (x:e) = 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 *) let swap f x y = f y x;; bind cam (swap left) 2;; (* false *)