X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=blobdiff_plain;f=intensionality-monad.ml;fp=intensionality-monad.ml;h=2f30f8b73f3a4d66620296fd58d57561fb8cb12a;hp=0000000000000000000000000000000000000000;hb=5eb5b091a62e66068007e326cc97ea1faaad2960;hpb=f3dfba595f7e893633f572694d184245f23ce3bc

diff --git a/intensionality-monad.ml b/intensionality-monad.ml
new file mode 100644
index 00000000..2f30f8b7
--- /dev/null
+++ b/intensionality-monad.ml
@@ -0,0 +1,57 @@
+(* 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 *)