-(* GSV monadically 13 April 2015 *)
+(* GSV monadically 15 April 2015 *)
type identifier = char
-let any_truths (xs : 'a list) : bool = List.exists ident xs
-let all_truths (xs : 'a list) : bool = List.for_all ident xs
module type SEMANTICS = sig
type noun (* this is whatever monadic type the semantics assigns to noun-sized contents *)
val maybe : sent -> sent
end
-type world = Actual | Other | Another
-let modal_domain = [Actual; Other; Another]
+type world = Actual | Second | Third
+let modal_domain = [Actual; Second; Third]
type entity = Ann | Bill | Carol | Dave | Ella | Frank
let domain = [Ann; Bill; Carol; Dave; Ella; Frank]
| Frank -> "Frank"
let print_entity ent = print_string (string_of_entity ent)
+let env0 = fun _ -> raise Not_found
+let lookup (sought : identifier) env = env sought
+let lookup_string (sought : identifier) env = try string_of_entity (env sought) with Not_found -> "*"
+let print_lookup c env = print_string (lookup_string c env)
+let insert (var : identifier) who env = fun sought -> if sought = var then who else env sought
+
+let any_truths (xs : 'a list) : bool = List.exists ident xs
+let all_truths (xs : 'a list) : bool = List.for_all ident xs
+
module Facts(X : Monad.MONAD) = struct
(* Here are the atomic facts: Ann and Bill are married, also Carol and Dave.
Genders and marital statuses are epistemically necessary.
In the actual world (w1), everyone left; people look leftwards (Carol sees Bill and Ann, etc.); Carol and Dave kiss; husbands love only their wives and Frank loves all the women.
In w2, all but Carol left; no one sees anything; all spouses kiss; all men love only Carol and Ella loves the wives.
In w3, only Ann and Bill left; no one sees anything; nobody kisses; Frank loves everyone else.
+ So: everyone is either essentially married or essentially single. And Ann and Bill essentially left; others left only contingently.
*)
let is_male = function Bill | Dave | Frank -> true | _ -> false
end
+(* create lots of monads, so that we have them if we need them *)
-
-
-
-
+module L = Monad.List
module R = Monad.Reader(struct type env = identifier -> entity end)
-module S = Monad.State(struct type store = identifier -> entity end)
-module S' = Monad.State(struct type store = identifier -> int end)
module R' = Monad.Reader(struct type env = identifier -> int end)
-
-let env0 = fun _ -> raise Not_found
-let lookup (sought : identifier) env = env sought
-let lookup_string (sought : identifier) env = try string_of_entity (env sought) with Not_found -> "*"
-let print_lookup c env = print_string (lookup_string c env)
-let insert (var : identifier) who env = fun sought -> if sought = var then who else env sought
-
module Y = Monad.Reader(struct type env = world end)
-
-module L = Monad.List
+module S = Monad.State(struct type store = identifier -> entity end)
+module S' = Monad.State(struct type store = identifier -> int end)
module RY = struct
include R.T(Y)
end
+(*
+ A variety of semantics are provided. Here is the naming scheme:
+
+ Sem1* is classic semantics with support for variable binding/anaphora.
+ Sem5* would be the dynamic alternative of 1*. (not here provided, but
+ discussed in comments.)
+ You can't implement quantification in these,
+ except by bringing in some of the mechanisms of a list/set component.
+ (You'll create a box([entity]) and convert it to a box([bool]),
+ then convert the latter to box(bool).)
+ However, Haskell already provides the needed mechanisms in the basic Monad API (as the
+ function Juli8 names `seq`), so we can do quantification without _explicitly
+ invoking_ a ListT in our monadic stack.
+
+ Sem2* and Sem 6* would be the intensionalized versions of those.
+ (Not here provided, but Sem6* is discussed in comments.)
+
+ Sem3* adds a List component to the stack to do quantification.
+ Sem7* is the dynamic counterpart.
+
+ Sem4* adds an (additional) Reader monad for intensionality.
+ Sem8* is the dynamic counterpart.
+
+ Within that broad organization, here are the sub-patterns:
+
+ SemNa uses just a bool payload, so sent types are box(bool).
+ SemNb makes sent types the Klesli variant of Na, so sent types are
+ bool -> box(bool).
+ SemNc uses instead a unit payload, which we can do when the monadic
+ stack has a List or Option component; then false will be the monad's
+ mzero, whereas truth will be instances of type box(unit) that aren't
+ mzero.
+ SemNd would be the Kleisli variant of Nc, as Nb is the Kleisli variant
+ of Na.
+ SemNe (only for dynamic) would use "topics" or sequences of entities being discussed
+ as payloads, so sent types are box(topic). What we really provide
+ here is the Kleisli variation of this (SemNf), so sent types = topic -> box(topic).
+*)
+
+
module Sem1a = struct
let dynamic = false
let extensional = true
let maybe pp = fun b -> failwith "Unimplemented"
end (* Sem1b *)
-module Sem2a = struct
+module Sem3a = struct
let dynamic = false
let extensional = true
(* We could use either monad RL or LR, with type env = var -> entity.
Their box type is the same: env -> ['a]
- However, the types of SL and LS differ, and the latter is more suitable for the dynamic version. So to keep things maximally parallel, we'll use LR here.
+ However, the types of SL and LS differ, and the latter is more suitable for (some of) the dynamic version(s). So to keep things maximally parallel, we'll use LR here.
We use the box type in two ways: first, we use a box(entity) to compute whether a matrix
clause is satisfied by a bound pronoun, where entity ranges over the whole domain.
Second, it is convenient and more consonant with later strategies
that lacks a List component). Here we will let the types of sentences
be box(bool), that is: env -> [bool]. We will understand the sentence to be true
if there are ANY truths in the resulting list. A list of all falses is treated
- the same as an empty list. Sem2c, below, eliminates this artifact by changing
+ the same as an empty list. Sem3c, below, eliminates this artifact by changing
the sentence type to box(unit). Then truths (rel to an env) are [();...] and
falsehoods are [].
*)
let marriedto = F.marriedto let saw = F.saw1 let kisses = F.kisses1 let loves = F.loves1
let thinks pp xx = failwith "Unimplemented"
let maybe pp = failwith "Unimplemented"
-end (* Sem2a *)
+end (* Sem3a *)
-(* Sem2b would convert Sem2a into having sentence meanings be Kleisli arrows, as Sem1b did.
+(* Sem3b would convert Sem3a into having sentence meanings be Kleisli arrows, as Sem1b did.
Not here implemented. *)
-(* Variant of Sem2a, which uses [();...] vs [] instead of [true;...] vs (list of all false OR []). *)
-module Sem2c = struct
+(* Variant of Sem3a, which uses [();...] vs [] instead of [true;...] vs (list of all false OR []). *)
+module Sem3c = struct
let dynamic = false
let extensional = true
let loves yy xx = X.(F.loves1 yy xx >>= to_unit)
let thinks pp xx = failwith "Unimplemented"
let maybe pp = failwith "Unimplemented"
-end (* Sem2c *)
+end (* Sem3c *)
-(* Sem2d would convert Sem2c into having sentence meanings be Kleisli arrows, as Sem1b did.
+(* Sem3d would convert Sem3c into having sentence meanings be Kleisli arrows, as Sem1b did.
Not here implemented. *)
(* Add intensionality to 2a *)
-module Sem3a = struct
+module Sem4a = struct
let dynamic = false
let extensional = false
let getz = X.(asks (lookup 'z'))
let getw = X.(uask) (* get world from the underlying Y monad *)
(* select an intranstive verb based on the world *)
- let select1 f1 f2 f3 xx = X.(getw >>= fun w -> (if w = Actual then f1 else if w = Other then f2 else f3) xx)
+ let select1 f1 f2 f3 xx = X.(getw >>= fun w -> (if w = Actual then f1 else if w = Second then f2 else f3) xx)
(* select a transitive verb based on the world *)
- let select2 f1 f2 f3 yy xx = X.(getw >>= fun w -> (if w = Actual then f1 else if w = Other then f2 else f3) yy xx)
+ let select2 f1 f2 f3 yy xx = X.(getw >>= fun w -> (if w = Actual then f1 else if w = Second then f2 else f3) yy xx)
let let_ c (xx : noun) (body : sent) = X.(xx >>= fun x -> shift (insert c x) body)
let letw world (body : sent) = X.(ushift (fun _ -> world) body) (* shift the "env" of the underlying Y monad *)
let body_int = List.map (fun w' -> any_truths (X.run (letw w' body) e w)) modal_domain in
body_int (* can just use body's intension as the result of `maybe body` *) in
Obj.magic yy
-end (* Sem3a *)
+end (* Sem4a *)
-(* Sem3b would convert Sem3a into having sentence meanings be Kleisli arrows, as Sem1b did.
+(* Sem4b would convert Sem4a into having sentence meanings be Kleisli arrows, as Sem1b did.
Not here implemented. *)
(* Add intensionality to 2c *)
-module Sem3c = struct
+module Sem4c = struct
let dynamic = false
let extensional = false
let getz = X.(asks (lookup 'z'))
let getw = X.(uask) (* get world from the underlying Y monad *)
(* select an intranstive verb based on the world *)
- let select1 f1 f2 f3 xx = X.(getw >>= fun w -> (if w = Actual then f1 else if w = Other then f2 else f3) xx)
+ let select1 f1 f2 f3 xx = X.(getw >>= fun w -> (if w = Actual then f1 else if w = Second then f2 else f3) xx)
(* select a transitive verb based on the world *)
- let select2 f1 f2 f3 yy xx = X.(getw >>= fun w -> (if w = Actual then f1 else if w = Other then f2 else f3) yy xx)
+ let select2 f1 f2 f3 yy xx = X.(getw >>= fun w -> (if w = Actual then f1 else if w = Second then f2 else f3) yy xx)
let let_ c (xx : noun) (body : sent) = X.(xx >>= fun x -> shift (insert c x) body)
let letw world (body : sent) = X.(ushift (fun _ -> world) body) (* shift the "env" of the underlying Y monad *)
let to_unit (x : bool) : unit X.t = X.guard x
let body_int = List.map (fun w' -> not @@ List.is_null @@ X.run (letw w' body) e w) modal_domain in
if any_truths body_int then [()] else [] in
Obj.magic yy
-end (* Sem3c *)
+end (* Sem4c *)
-(* Sem3d would convert Sem3c into having sentence meanings be Kleisli arrows, as Sem1b did.
+(* Sem4d would convert Sem4c into having sentence meanings be Kleisli arrows, as Sem1b did.
Not here implemented. *)
-(* Dynamic version of Sem2c *)
-module Sem5c = struct
+(* Dynamic version of Sem3c *)
+module Sem7c = struct
let dynamic = true
let extensional = true
let getz = X.(gets (lookup 'z'))
let let_ c (xx : noun) (body : sent) = X.(xx >>= fun x -> modify (insert c x) >> body)
let to_unit (x : bool) : unit X.t = X.guard x
-(*
- let peek msg () = X.(get >>= fun s -> begin print_string msg; print_string ": x="; print_lookup 'x' s; print_string ", y="; print_lookup 'y' s; print_string ", z="; print_lookup 'z' s; print_newline (); mid () end)
-*)
let (~~~) (xx : sent) : sent =
let yy : S.store -> (unit * S.store) list = fun s -> if List.is_null (X.run xx s) then [(),s] else [] in
Obj.magic yy (* this is an identity function that changes the type of yy to a unit X.t *)
let (&&&) xx yy = X.(xx >> yy)
let (|||) xx yy = ~~~ (~~~ xx &&& ~~~ yy)
- let (>>>) xx yy = X.(~~~ (xx >> ~~~ yy))
+ let (>>>) xx yy = X.(~~~ (xx &&& ~~~ yy))
(*
This would propagate effects out of the disjuncts, so that for example after
let loves yy xx = X.(F.loves1 yy xx >>= to_unit)
let thinks pp xx = failwith "Unimplemented"
let maybe pp = failwith "Unimplemented"
-end (* Sem5c *)
+end (* Sem7c *)
-(* Dynamic version of Sem3c / Add intensionality to Sem5c *)
-module Sem6c = struct
+(* Dynamic version of Sem4c / Add intensionality to Sem7c *)
+module Sem8c = struct
let dynamic = true
let extensional = false
let getz = X.(gets (lookup 'z'))
let getw = X.(ask) (* get world from the underlying Y monad *)
(* select an intranstive verb based on the world *)
- let select1 f1 f2 f3 xx = X.(getw >>= fun w -> (if w = Actual then f1 else if w = Other then f2 else f3) xx)
+ let select1 f1 f2 f3 xx = X.(getw >>= fun w -> (if w = Actual then f1 else if w = Second then f2 else f3) xx)
(* select a transitive verb based on the world *)
- let select2 f1 f2 f3 yy xx = X.(getw >>= fun w -> (if w = Actual then f1 else if w = Other then f2 else f3) yy xx)
+ let select2 f1 f2 f3 yy xx = X.(getw >>= fun w -> (if w = Actual then f1 else if w = Second then f2 else f3) yy xx)
let let_ c (xx : noun) (body : sent) = X.(xx >>= fun x -> modify (insert c x) >> body)
let letw world (body : sent) = X.(shift (fun _ -> world) body) (* shift the "env" of the underlying Y monad *)
let to_unit (x : bool) : unit X.t = X.guard x
let (&&&) xx yy = X.(xx >> yy)
let (|||) xx yy = ~~~ (~~~ xx &&& ~~~ yy)
- let (>>>) xx yy = X.(~~~ (xx >> ~~~ yy))
+ let (>>>) xx yy = X.(~~~ (xx &&& ~~~ yy))
let some c (body : sent) = X.(let_ c (mids domain) body)
let every c (body : sent) = ~~~ (some c (~~~ body))
let body_int = List.map (fun w' -> not @@ List.is_null @@ X.run (letw w' body) s w) modal_domain in
if any_truths body_int then [(),s] else [] in
Obj.magic yy
-end (* Sem6c *)
+end (* Sem8c *)
-(* Sem6c seems adequate for the phenomena GSV are examining, and is substantially simpler than their own semantics. Sem6c doesn't have their "pegs" and complex two-stage function from vars to referents.
+(* Sem8c seems adequate for much of the phenomena GSV are examining, and is substantially simpler than their own semantics. Sem8c doesn't have their "pegs" and complex two-stage function from vars to referents.
Next we develop some semantics that are closer to their actual presentation. *)
-(* This develops Sem5c using in part the strategies from Sem1b. *)
-module Sem5e = struct
+(* This develops Sem7c using in part the Kleisli strategy from Sem1b. *)
+module Sem7f = struct
let dynamic = true
let extensional = true
in the type captures indeterminacy in what objects are being discussed (introduced
by quantifiers). Truths (relative to a initial store and topic) result in
non-empty topic lists; falsehoods in empty ones.
+ Our stores/envs are GSV's refsys r; our topics are their g.
+ Notice that GSV make their "information states" homogenous wrt r; this corresponds
+ to our result type having stores _outside_ the list.
+ GSV's meaning types are [store * topic * world] -> [store * topic * world], but
+ as noted the homogeneity wrt store would permit also:
+ store * [topic * world] -> store * [topic * world].
+ Our meaning types (once we add worlds in 6e, below) will be:
+ topic -> (store -> world -> ([topic] * store))
+ We count a world as eliminated when it results in an empty list of topics.
+ Note that our Sem8f doesn't yet properly handle Veltman's "might"; see remarks below.
*)
type topic = entity list
let topic0 = []
let gety : noun = X.(gets (lookup 'y') >>= fun n -> mid (get_nth n))
let getz : noun = X.(gets (lookup 'z') >>= fun n -> mid (get_nth n))
let let_ c (n : int) (body : sent) : sent = fun top -> X.(modify (insert c n) >> (body top))
-(*
- let lookup_string sought env top = try string_of_entity (List.nth top (env sought)) with Not_found -> "*" | List.Short_list -> "#"
- let print_lookup sought env top = print_string (lookup_string sought env top)
- let peek msg top = X.(get >>= fun s -> begin print_string msg; print_string ": x="; print_lookup 'x' s top; print_string ", y="; print_lookup 'y' s top; print_string ", z="; print_lookup 'z' s top; print_newline (); mid top end)
-*)
+
+ (* All logical operations except &&& and some are "effect islands", with the exception that effects of the antecedent
+ of a conditional are visible in that conditional's consequent. *)
let (~~~) (k : sent) : sent = fun top ->
let yy : S'.store -> topic list * S'.store = fun s -> if List.is_null (fst (X.run (k top) s)) then ([top],s) else ([],s) in
Obj.magic yy (* this is an identity function that changes the type of yy to a topic X.t *)
let (&&&) k j = X.(k >=> j)
- let (|||) k j = ~~~ (~~~ k &&& ~~~ j) (* TODO how about (k >>> j) >>> j *)
+ let (|||) k j = ~~~ (~~~ k &&& ~~~ j)
let (>>>) k j = X.(~~~ (k >=> ~~~ j))
+ (* This properly handles `some` as GSV do, by only joining the results
+ _after_ updating them on body(extended topic). See GSV pp. 28-9. *)
let some c (body : sent) : sent = fun top ->
let n = length top in
let aux ent = X.(let_ c n body) (List.snoc top ent) in
let every c (body : sent) = ~~~ (some c (~~~ body))
-(* TODO
- let some c body = X.(mids domain >>= fun x -> modify (insert c x) body >>= guard >> mid x)
- let every c body = X.(let xx = let_ c (mids domain) body in list_map (fun xs -> if all_truths xs then xs else []) xx)
-*)
-
module F = Facts(X)
let mapply' (ff : noun) (top : topic) : entity X.t = X.(map (fun f -> f top) ff)
let wrap name = X.(mid (const name))
let loves yy xx = wrap2 F.loves1 yy xx
let thinks pp xx = fun top -> failwith "Unimplemented"
let maybe pp = fun top -> failwith "Unimplemented"
-end (* Sem5e *)
+end (* Sem7f *)
-(* Add intensionality to Sem5e *)
-module Sem6e = struct
+(* Add intensionality to Sem7f. See comments there. *)
+module Sem8f = struct
let dynamic = true
let extensional = false
let getz : noun = X.(gets (lookup 'z') >>= fun n -> mid (get_nth n))
let getw = X.(ask) (* get world from the underlying Y monad *)
(* select an intranstive verb based on the world *)
- let select1 f1 f2 f3 xx = X.(getw >>= fun w -> (if w = Actual then f1 else if w = Other then f2 else f3) xx)
+ let select1 f1 f2 f3 xx = X.(getw >>= fun w -> (if w = Actual then f1 else if w = Second then f2 else f3) xx)
(* select a transitive verb based on the world *)
- let select2 f1 f2 f3 yy xx = X.(getw >>= fun w -> (if w = Actual then f1 else if w = Other then f2 else f3) yy xx)
+ let select2 f1 f2 f3 yy xx = X.(getw >>= fun w -> (if w = Actual then f1 else if w = Second then f2 else f3) yy xx)
let let_ c (n : int) (body : sent) : sent = fun top -> X.(modify (insert c n) >> (body top))
let letw world (body : sent) : sent = fun top -> X.(shift (fun _ -> world) (body top)) (* shift the "env" of the underlying Y monad *)
+ (* debugging *)
+ let lookup_string sought env top = try string_of_entity (List.nth top (env sought)) with Not_found -> "*" | List.Short_list -> "#"
+ let print_lookup sought env top = print_string (lookup_string sought env top)
+ let peek msg top = X.(get >>= fun s -> begin print_string msg; print_string ": x="; print_lookup 'x' s top; print_string ", y="; print_lookup 'y' s top; print_string ", z="; print_lookup 'z' s top; print_newline (); mid top end)
+ (* variant of run that uses a non-empty initial topic list, and displays entire result, not just whether it's true *)
+ let run' (k : sent) ?(w=Actual) (tops : topic list) =
+ let n = List.length (List.head tops) in
+ let env = match n with
+ | 1 -> insert 'x' 0 env0
+ | 2 -> insert 'x' 0 (insert 'y' 1 env0)
+ | 3 -> insert 'x' 0 (insert 'y' 1 (insert 'z' 2 env0))
+ | _ -> failwith ("can't run' topics of length " ^ string_of_int n) in
+ assert(for_all (fun top -> List.length top = n) tops);
+ X.(run (mids tops >>= k) env w)
+
let (~~~) (k : sent) : sent = fun top ->
let yy : S'.store -> Y.env -> topic list * S'.store = fun s w -> if List.is_null (fst (X.run (k top) s w)) then ([top],s) else ([],s) in
Obj.magic yy (* this is an identity function that changes the type of yy to a topic X.t *)
let body_int = List.map (fun w' -> not @@ List.is_null @@ fst @@ X.run (letw w' body top) s w) modal_domain in
if any_truths body_int then [top],s else [],s in
Obj.magic yy
-end (* Sem6e *)
+ (* This implementation of `maybe` doesn't yet exactly capture Veltman's "might". It isn't a holistic filter:
+ it examines topics one-by-one and will eliminate any where they (considered in isolation) make body impossible.
+ Hence, if some of the possible referents for x are essentially not-body, and others are possibly-body, after
+ updating on _this_ implementation of `maybe body`, we'll be left with only the latter. On Veltman's semantics,
+ otoh, we'd be left with the whole original information state.
+ To capture Veltman's semantics properly, we'd need to remove the List component from our monad stack, and use
+ [topic] as our payloads, so that sent types would then be: [topic] -> S'Y([topic]). All of the operations except
+ for `maybe` would then have to emulate the operations of the List monad by hand (manually performing catmap etc).
+ But `maybe` could examine the [topic] as a whole and decide whether to return box(it) or box([]).
+ This would be to go back to the Sem5/Sem6 choices of monads (without list), and to implement the handling of lists
+ by hand, as we did in the Sem1/Sem2 strategies.
+
+ Additionally, we haven't tried here to handle non-rigid noun-types. That's why we can have sent types be:
+ topic (or [topic]) -> store -> world -> ([topic], store)
+ the input topic doesn't depend on what the world is. GSV's types are suited to handle non-rigid noun types,
+ since they are instead using an analogue of (world * topic) -> store -> ([world,topic], store). We could follow suit,
+ removing the Reader monad implementing Intensionality from our stack and implementing that by hand, too. Another
+ strategy would be to continue using a Reader monad but not by merging it into our main monad stack, instead using
+ values of _that_ box type as _payloads for_ our main box type. This echoes a question raised by Dylan in seminar:
+ why must we combine the monads only by way of "stacking them" into a single monad? As Jim said in seminar, it's not
+ obvious one must do so, it just seems most natural. The strategy being evisaged now would at least in part follow
+ Dylan's suggestion. We'd let our sentence types then be:
+ intensionality_box([topic]) -> state_plus_intensionality_box(intensionality_box([topic]))
+ = intensionality_box([topic]) -> store -> world -> (intensionality_box([topic]) * store)
+ In that case, I think we could once again merge the list component into the intensionality_box type, getting:
+ intens_list_box(topic) -> state_intens_box(intens_list_box(topic))
+ = intens_list_box(topic) -> store -> world -> (intens_list_box(topic) * store)
+ = (world -> [topic]) -> store -> world -> ((world -> [topic]) * store)
+ That looks like a pretty complicated type, and might not seem an improvement over GSV's own system. But its advantage is that
+ the implementation of its operations would so closely parallel the other semantic strategies illustrated above.
+ Testifying to the "modularity" of monads, which we have been recommending as one of their prominent virtues.
+ *)
+
+end (* Sem8f *)
module TestAll = struct
print_endline "\nTesting Sem1a";;
module T1a = Test(Sem1a);;
print_endline "\nTesting Sem1b";;
module T1b = Test(Sem1b);;
- print_endline "\nTesting Sem2a";;
- module T2a = Test(Sem2a);;
- print_endline "\nTesting Sem2c";;
- module T2c = Test(Sem2c);;
print_endline "\nTesting Sem3a";;
module T3a = Test(Sem3a);;
print_endline "\nTesting Sem3c";;
module T3c = Test(Sem3c);;
- print_endline "\nTesting Sem5c";;
- module T5c = Test(Sem5c);;
- print_endline "\nTesting Sem5e";;
- module T5e = Test(Sem5e);;
- print_endline "\nTesting Sem6c";;
- module T6c = Test(Sem6c);;
- print_endline "\nTesting Sem6e";;
- module T6e = Test(Sem6e);;
+ print_endline "\nTesting Sem4a";;
+ module T4a = Test(Sem4a);;
+ print_endline "\nTesting Sem4c";;
+ module T4c = Test(Sem4c);;
+ print_endline "\nTesting Sem7c";;
+ module T7c = Test(Sem7c);;
+ print_endline "\nTesting Sem7f";;
+ module T7f = Test(Sem7f);;
+ print_endline "\nTesting Sem8c";;
+ module T8c = Test(Sem8c);;
+ print_endline "\nTesting Sem8f";;
+ module T8f = Test(Sem8f);;
print_newline ()
end