changed my unit_M to Chris' convention of M_unit, for consistency
[lambda.git] / intensionality-monad.ml
1 (* This is the intensionality monad discussed in the lecture notes for week 7. *)
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 (x:e) (y:e) = y < x;; (* Ann saw Bill and Cam, and Bill saw Cam *)
13
14 left1 ann;;
15 saw1 bill ann;;
16 saw1 ann bill;;
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 x y w = (w < 2) && (y < x);;
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 unit x (w:s) = x;;
31 let bind m f (w:s) = f (m w) w;;
32 let lift2' f u v = bind u (fun x -> bind v (fun y -> f x y));;
33
34 bind (unit ann) left 1;;
35 bind (unit cam) left 2;;
36
37 lift2' saw (unit bill) (unit ann) 1;; 
38 lift2' saw (unit bill) (unit ann) 2;;
39
40 let thinks (p:s->t) (x:e) (w:s) = 
41   match (x, p 2) with ('a', false) -> false | _ -> p w;;
42
43 bind (unit ann) (thinks (bind (unit bill) left)) 1;;
44 bind (unit ann) (thinks (bind (unit cam) left)) 1;;
45