projects
/
lambda.git
/ commitdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
| commitdiff |
tree
raw
|
patch
|
inline
| side by side (parent:
a0bd769
)
update intensionality.ml
author
Jim
<jim.pryor@nyu.edu>
Mon, 6 Apr 2015 13:41:19 +0000
(09:41 -0400)
committer
Jim
<jim.pryor@nyu.edu>
Mon, 6 Apr 2015 13:41:19 +0000
(09:41 -0400)
code/intensionality-monad.ml
patch
|
blob
|
history
diff --git
a/code/intensionality-monad.ml
b/code/intensionality-monad.ml
index
eebe5ee
..
b05d3fe
100644
(file)
--- a/
code/intensionality-monad.ml
+++ b/
code/intensionality-monad.ml
@@
-8,38
+8,38
@@
let ann = 'a';;
let bill = 'b';;
let cam = 'c';;
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;;
(* Now we make the extension of "leave" sensitive to the world of evaluation *)
left1 ann;;
saw1 bill ann;;
saw1 ann bill;;
(* 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 *)
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 *)
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;;
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;;
+
(mid cam >>= left)
2;;
-
lift2' saw (unit bill) (unit
ann) 1;;
-
lift2' saw (unit bill) (unit
ann) 2;;
+
map2' saw (mid bill) (mid
ann) 1;;
+
map2' saw (mid bill) (mid
ann) 2;;
-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;;
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 ann >>= thinks (mid bill >>=
left)) 1;;
+
(mid ann >>= thinks (mid cam >>=
left)) 1;;