intensionality-monad.ml

   1 (* This is the intensionality monad discussed in the lecture notes for week 7. *)
   2
   3 type s = int;;
   4 type e = char;;
   5 type t = bool;;
   6
   7 type 'a intension = s -> 'a;;
   8 let unit x (w:s) = x;;
   9
  10 let ann = unit 'a';;
  11 let bill = unit 'b';;
  12 let cam = unit 'c';;
  13
  14 let bind m f (w:s) = f (m w) w;;
  15 bind (unit 'a') unit 1;;
  16
  17 let left w x = match (w,x) with (2,'c') -> false | _ -> true;;
  18
  19 let extapp fn arg w = fn w (arg w);;
  20
  21 extapp left ann 1;;
  22
  23 extapp left cam 2;;
  24
  25 let saw w x y = (w < 2) && (y < x);;
  26 extapp (extapp saw bill) ann 1;; (* true *)
  27 extapp (extapp saw bill) ann 2;; (* false *)
  28
  29 let intapp fn arg w = fn w arg;;
  30
  31 let lift pred w arg = bind arg (fun x w -> pred w x) w;;
  32
  33 intapp (lift left) ann 1;; (* true: Ann still left in world 1 *)
  34 intapp (lift left) cam 2;; (* false: Cam still didn't leave in world 2 *)
  35
  36 let lift2 pred w arg1 arg2 =
  37   bind arg1 (fun x -> bind arg2 (fun y w -> pred w x y)) w;;
  38 intapp (intapp (lift2 saw) bill) ann 1;;  (* true: Ann saw Bill in world 1 *)
  39 intapp (intapp (lift2 saw) bill) ann 2;;  (* false: No one saw anyone in world 2 *)
  40
  41 let think (w:s) (p:s->t) (x:e) =
  42   match (x, p 2) with ('a', false) -> false | _ -> p w;;
  43
  44 intapp (lift (intapp think
  45                      (intapp (lift left)
  46                              (unit 'b'))))
  47        (unit 'a')
  48 1;; (* true *)
  49
  50 intapp (lift (intapp think
  51                      (intapp (lift left)
  52                              (unit 'c'))))
  53        (unit 'a')
  54 1;; (* false *)
  55
  56 let swap f x y = f y x;;
  57 bind cam (swap left) 2;; (* false *)