X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=blobdiff_plain;f=code%2Fintensionality-monad.ml;h=b5dc9f52cd90c64b893f882ac3fc3ba8982d8168;hp=eebe5ee1f1334839c3ddce63b886282900325cb5;hb=f747612ad27e9facc7c92c04e4c6981b40a561ad;hpb=183aeafe5566607c8768b7c978907a15b6c29c4c diff --git a/code/intensionality-monad.ml b/code/intensionality-monad.ml index eebe5ee1..b5dc9f52 100644 --- a/code/intensionality-monad.ml +++ b/code/intensionality-monad.ml @@ -1,4 +1,4 @@ -(* This is the intensionality monad discussed in the lecture notes for week 7. *) +(* This is the intensionality monad discussed in the lecture notes for week 8. *) type s = int;; (* integers model possible worlds *) type e = char;; (* chars model individuals *) @@ -8,38 +8,40 @@ let ann = 'a';; let bill = 'b';; let cam = 'c';; -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 left1 (x : e) = true;; (* Everyone left *) +let saw1 (y : e) (x : e) = x < y;; (* Ann saw Bill and Cam, and Bill saw Cam *) -left1 ann;; -saw1 bill ann;; -saw1 ann bill;; +left1 ann;; (* true *) +saw1 bill ann;; (* true *) +saw1 ann bill;; (* false *) (* 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;; +let left (x : e) (w : s) = match (x, w) with ('c', 2) -> false | _ -> true;; left ann 1;; (* Ann left in world 1 *) left cam 2;; (* Cam didn't leave in world 2 *) -let saw x y w = (w < 2) && (y < x);; +let saw (y : e) (x : e) (w : s) = (w < 2) && (x < y);; saw bill ann 1;; (* Ann saw Bill in world 1 *) saw bill ann 2;; (* Ann didn't see Bill in world 2 *) -(* The intensionality reader-monad: *) +(* 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));; +let mid x (w : s) = x;; +let (>>=) xx k (w : s) = k (xx w) w;; +let map2' f xx yy = xx >>= (fun x -> yy >>= (fun y -> f x y));; -bind (unit ann) left 1;; -bind (unit cam) left 2;; +(mid ann >>= left) 1;; (* true *) +(mid cam >>= left) 2;; (* false *) -lift2' saw (unit bill) (unit ann) 1;; -lift2' saw (unit bill) (unit ann) 2;; +map2' saw (mid bill) (mid ann) 1;; (* true *) +map2' saw (mid bill) (mid ann) 2;; (* false *) -let thinks (p:s->t) (x:e) (w:s) = +let thinks (p : s->t) (x : e) (w : s) = match (x, p 2) with ('a', false) -> false | _ -> p w;; -bind (unit ann) (thinks (bind (unit bill) left)) 1;; -bind (unit ann) (thinks (bind (unit cam) left)) 1;; +(mid bill >>= left) 1;; (* true *) +(mid cam >>= left) 1;; (* true *) +(mid ann >>= thinks (mid bill >>= left)) 1;; (* true *) +(mid ann >>= thinks (mid cam >>= left)) 1;; (* false *)