update gsv2.ml

diff --git a/code/gsv2.ml b/code/gsv2.ml
index abd305f..c8f039f 100644 (file)
--- a/code/gsv2.ml
+++ b/code/gsv2.ml
@@ -1,8 +1,6 @@
 (* GSV monadically 13 April 2015 *)
 
 type identifier = char
 (* GSV monadically 13 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 *)
 
 module type SEMANTICS = sig
   type noun (* this is whatever monadic type the semantics assigns to noun-sized contents *)


@@ -39,8 +37,8 @@ module type SEMANTICS = sig
   val maybe : sent -> sent
 end
 
   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]
 
 type entity = Ann | Bill | Carol | Dave | Ella | Frank
 let domain = [Ann; Bill; Carol; Dave; Ella; Frank]


@@ -53,12 +51,22 @@ let string_of_entity = function
   | Frank -> "Frank"
 let print_entity ent = print_string (string_of_entity ent)
 
   | 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.
 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
 *)
 
   let is_male = function Bill | Dave | Frank -> true | _ -> false


@@ -206,25 +214,14 @@ module Test(S : SEMANTICS) : sig end = struct
 
 end
 
 
 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 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)
 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 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)
 
 module RY = struct
   include R.T(Y)


@@ -385,6 +382,43 @@ module YS'L = struct
 end
 
 
 end
 
 

+(*
+   A variety of semantics are provided. Here is the naming scheme:
+   
+   Sem1* is classic semantics with support for variable binding/anaphora.
+   Sem4* would be the dynamic alternative of 1*. (not here provided)
+   You shouldn't be able to implement quantification in these,
+   without bringing in some of the mechanisms of a list/set component.
+   However, Haskell provides those 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* adds a List component to the stack to do quantification.
+   Sem5* is the dynamic counterpart.
+
+   Sem3* adds an (additional) Reader monad for intensionality.
+   Sem6* 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).
+   SemBb 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) uses "topics" or sequences of entities being
+   discussed as payloads, so sent types use box(topic). It also incorporates
+   elements of SemNb/d, so that sent types are really topic -> box(topic).
+   SemNf (not yet provided) would remove the List component from the monad
+   stack, in order to properly implement Veltman's "might". Now sent
+   types would be [topic] -> box([topic]).
+*)
+ 
+

 module Sem1a = struct
   let dynamic = false
   let extensional = true
 module Sem1a = struct
   let dynamic = false
   let extensional = true


@@ -485,7 +519,7 @@ module Sem2a = struct
 
   (* We could use either monad RL or LR, with type env = var -> entity.
      Their box type is the same: env -> ['a]
 
   (* 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
      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


@@ -603,9 +637,9 @@ module Sem3a = struct
   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 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 *)
   (* 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 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 *)
 


@@ -656,9 +690,9 @@ module Sem3c = struct
   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 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 *)
   (* 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 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


@@ -719,16 +753,13 @@ module Sem5c = struct
   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 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 : 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
 
 (*
     This would propagate effects out of the disjuncts, so that for example after


@@ -783,9 +814,9 @@ module Sem6c = struct
   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 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 *)
   (* 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 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


@@ -799,7 +830,7 @@ module Sem6c = struct
 
   let (&&&) xx yy = X.(xx >> yy)
   let (|||) xx yy = ~~~ (~~~ xx &&& ~~~ yy)
 
   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 some c (body : sent) = X.(let_ c (mids domain) body)
   let every c (body : sent) = ~~~ (some c (~~~ body))


@@ -823,10 +854,10 @@ module Sem6c = struct
     Obj.magic yy
 end (* Sem6c *)
 
     Obj.magic yy
 end (* Sem6c *)
 

-(* 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.
+(* Sem6c seems adequate for much of 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.

    Next we develop some semantics that are closer to their actual presentation. *)
 
    Next we develop some semantics that are closer to their actual presentation. *)
 

-(* This develops Sem5c using in part the strategies from Sem1b. *)
+(* This develops Sem5c using in part the Kleisli strategy from Sem1b. *)

 module Sem5e = struct
   let dynamic = true
   let extensional = true
 module Sem5e = struct
   let dynamic = true
   let extensional = true


@@ -838,6 +869,16 @@ module Sem5e = struct
      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.
      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 Sem6e doesn't yet properly handle Veltman's "might"; see remarks below.

   *)
   type topic = entity list
   let topic0 = []
   *)
   type topic = entity list
   let topic0 = []


@@ -852,19 +893,19 @@ module Sem5e = struct
   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 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 : 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))
 
   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 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


@@ -873,11 +914,6 @@ module Sem5e = struct
 
   let every c (body : sent) = ~~~ (some c (~~~ body))
 
 
   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))
   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))


@@ -897,7 +933,7 @@ module Sem5e = struct
   let maybe pp = fun top -> failwith "Unimplemented"
 end (* Sem5e *)
 
   let maybe pp = fun top -> failwith "Unimplemented"
 end (* Sem5e *)
 

-(* Add intensionality to Sem5e *)
+(* Add intensionality to Sem5e. See comments there. *)

 module Sem6e = struct
   let dynamic = true
   let extensional = false
 module Sem6e = struct
   let dynamic = true
   let extensional = false


@@ -916,12 +952,27 @@ module Sem6e = struct
   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 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 *)
   (* 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 *)
 
   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 (~~~) (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 *)


@@ -958,6 +1009,17 @@ module Sem6e = struct
       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
       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

+  (* 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([]).
+  *)
+

 end (* Sem6e *)
 
 module TestAll = struct
 end (* Sem6e *)
 
 module TestAll = struct


@@ -997,5 +1059,16 @@ end
     that the referent be either woman. But it doesn't put me in a position to assert (ii),
     since that implies I was kissed by Carol. So far as truth-value goes,
     if Carol kissed me both sentences are true, and if Ann did then both sentences are false.
     that the referent be either woman. But it doesn't put me in a position to assert (ii),
     since that implies I was kissed by Carol. So far as truth-value goes,
     if Carol kissed me both sentences are true, and if Ann did then both sentences are false.

-*)

 
 

+# let module S = Sem6e in let wife xx = S.(female xx &&& ~~~ (single xx)) in let may_stay xx = S.(maybe (~~~ (left xx))) in ...
+# let xx = S.(wife getx) in S.(run_ xx [[Ann];[Carol];[Ella]]);;
+- : entity list list * S'Y.store = ([[Ann]; [Carol]], <fun>)
+# let xx = S.(may_stay getx) in S.(run_ xx [[Ann];[Carol];[Ella]]);;
+- : entity list list * S'Y.store = ([[Carol]; [Ella]], <fun>)
+# let xx = S.(some 'y' (gety === getx)) in S.(run_ xx [[Ann];[Carol];[Ella]]);;
+- : entity list list * S'Y.store = ([[Ann; Ann]; [Carol; Carol]; [Ella; Ella]], <fun>)
+# let xx = S.(some 'y' (gety === getx &&& may_stay gety)) in S.(run_ xx [[Ann];[Carol];[Ella]]);;
+- : entity list list * S'Y.store = ([[Carol; Carol]; [Ella; Ella]], <fun>)
+# let xx = S.(some 'y' (gety === getx) &&& may_stay gety) in S.(run_ xx [[Ann];[Carol];[Ella]]);;
+- : entity list list * S'Y.store = ([[Carol; Carol]; [Ella; Ella]], <fun>)
+*)