X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=blobdiff_plain;f=intensionality-monad.ml;h=eebe5ee1f1334839c3ddce63b886282900325cb5;hp=2f30f8b73f3a4d66620296fd58d57561fb8cb12a;hb=8fa88810958724fdd34b39f978adfd733c58ca44;hpb=5eb5b091a62e66068007e326cc97ea1faaad2960 diff --git a/intensionality-monad.ml b/intensionality-monad.ml index 2f30f8b7..eebe5ee1 100644 --- a/intensionality-monad.ml +++ b/intensionality-monad.ml @@ -1,57 +1,45 @@ (* This is the intensionality monad discussed in the lecture notes for week 7. *) -type s = int;; -type e = char;; -type t = bool;; +type s = int;; (* integers model possible worlds *) +type e = char;; (* chars model individuals *) +type t = bool;; (* booleans model truth values *) -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 ann = 'a';; +let bill = 'b';; +let cam = 'c';; -let left w x = match (w,x) with (2,'c') -> false | _ -> true;; +let left1 (x:e) = true;; (* Everyone left *) +let saw1 (x:e) (y:e) = y < x;; (* Ann saw Bill and Cam, and Bill saw Cam *) -let extapp fn arg w = fn w (arg w);; +left1 ann;; +saw1 bill ann;; +saw1 ann bill;; -extapp left ann 1;; +(* Now we make the extension of "leave" sensitive to the world of evaluation *) +let left (x:e) (w:s) = match (x, w) with ('c', 2) -> false | _ -> true;; -extapp left cam 2;; +left ann 1;; (* Ann left in world 1 *) +left cam 2;; (* Cam didn't leave in world 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 saw x y w = (w < 2) && (y < x);; +saw bill ann 1;; (* Ann saw Bill in world 1 *) +saw bill ann 2;; (* Ann didn't see Bill in world 2 *) -let intapp fn arg w = fn w arg;; - -let lift pred w arg = bind arg (fun x w -> pred w x) w;; +(* The intensionality reader-monad: *) +type 'a intension = s -> 'a;; +let unit x (w:s) = x;; +let bind m f (w:s) = f (m w) w;; +let lift2' f u v = bind u (fun x -> bind v (fun y -> f x y));; -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 *) +bind (unit ann) left 1;; +bind (unit cam) left 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 *) +lift2' saw (unit bill) (unit ann) 1;; +lift2' saw (unit bill) (unit ann) 2;; -let think (w:s) (p:s->t) (x:e) = +let thinks (p:s->t) (x:e) (w:s) = 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 *) +bind (unit ann) (thinks (bind (unit bill) left)) 1;; +bind (unit ann) (thinks (bind (unit cam) left)) 1;; -let swap f x y = f y x;; -bind cam (swap left) 2;; (* false *)