code/gsv2.ml

   1 (* GSV monadically 15 April 2015 *)
   2
   3 type identifier = char
   4
   5 module type SEMANTICS = sig
   6   type noun (* this is whatever monadic type the semantics assigns to noun-sized contents *)
   7   type sent (* this is whatever monadic type the semantics assigns to sentence-sized contents *)
   8   val run : sent -> bool
   9   val dynamic : bool
  10   val extensional : bool
  11
  12   val getx : noun  val gety : noun  val getz : noun
  13   (* OCaml will parse ~~~ as a prefix operator, but unfortunately won't let you say
  14      `~~~ predicate subject`; you have to say `~~~ (predicate subject)`. *)
  15   val ( ~~~ ) : sent -> sent
  16   (* OCaml will parse these three as infix operators (yay), but makes them all
  17      left-associative (ehh for >>>) and have the same precedence (boo). *)
  18   val ( &&& ) : sent -> sent -> sent
  19   val ( ||| ) : sent -> sent -> sent
  20   val ( >>> ) : sent -> sent -> sent
  21   (* OCaml parses this with same associativity and precedence as the preceding (boo). *)
  22   val (===) : noun -> noun -> sent
  23   val ann : noun  val bill : noun  val carol : noun  val dave : noun  val ella : noun  val frank : noun
  24   val male : noun -> sent  val female : noun -> sent
  25   val left : noun -> sent
  26   val single : noun -> sent
  27   (* Transitive verbs apply to their direct objs first, subjects second. *)
  28   val marriedto : noun -> noun -> sent
  29   val saw : noun -> noun -> sent
  30   val kisses : noun -> noun -> sent
  31   val loves : noun -> noun -> sent   (* here construed extensionally *)
  32   (* Quantifiers may be unimplemented. *)
  33   val some : identifier -> sent -> sent
  34   val every : identifier -> sent -> sent
  35   (* Intensional verbs and operators may be unimplemented. *)
  36   val thinks : sent -> noun -> sent
  37   val maybe : sent -> sent
  38 end
  39
  40 type world = Actual | Second | Third
  41 let modal_domain = [Actual; Second; Third]
  42
  43 type entity = Ann | Bill | Carol | Dave | Ella | Frank
  44 let domain = [Ann; Bill; Carol; Dave; Ella; Frank]
  45 let string_of_entity = function
  46   | Ann -> "Ann"
  47   | Bill -> "Bill"
  48   | Carol -> "Carol"
  49   | Dave -> "Dave"
  50   | Ella -> "Ella"
  51   | Frank -> "Frank"
  52 let print_entity ent = print_string (string_of_entity ent)
  53
  54 let env0 = fun _ -> raise Not_found
  55 let lookup (sought : identifier) env = env sought
  56 let lookup_string (sought : identifier) env = try string_of_entity (env sought) with Not_found -> "*"
  57 let print_lookup c env = print_string (lookup_string c env)
  58 let insert (var : identifier) who env = fun sought -> if sought = var then who else env sought
  59
  60 let any_truths (xs : 'a list) : bool = List.exists ident xs
  61 let all_truths (xs : 'a list) : bool = List.for_all ident xs
  62
  63 module Facts(X : Monad.MONAD) = struct
  64 (* Here are the atomic facts: Ann and Bill are married, also Carol and Dave.
  65    Genders and marital statuses are epistemically necessary.
  66    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.
  67    In w2, all but Carol left; no one sees anything; all spouses kiss; all men love only Carol and Ella loves the wives.
  68    In w3, only Ann and Bill left; no one sees anything; nobody kisses; Frank loves everyone else.
  69    So: everyone is either essentially married or essentially single. And Ann and Bill essentially left; others left only contingently.
  70 *)
  71
  72   let is_male = function Bill | Dave | Frank -> true | _ -> false
  73   let are_married = function (Ann, Bill) | (Bill, Ann) | (Carol, Dave) | (Dave, Carol) -> true | _ -> false
  74   let is_a_wife = function Ann | Carol -> true | _ -> false
  75
  76   let male xx = X.(map is_male xx)
  77   let female xx = X.(map (not % is_male) xx)
  78
  79 (* Ella and Frank are single *)
  80   let single xx = X.(map (fun x -> x > Dave) xx)
  81
  82 (* Actually (in w1), everybody left. In w2, everybody but Carol left. In w3, only Ann and Bill left. *)
  83   let left1 xx = X.(map (fun _ -> true) xx)
  84   let left2 xx = X.(map (fun x -> x <> Carol) xx)
  85   let left3 xx = X.(map (fun x -> x = Ann || x = Bill) xx)
  86
  87 (* In the sentences, order of application is: TransitiveVerb + Object + Subject.
  88    But we convert to logical order for our operations. *)
  89
  90 (* Actually, each person saw the people alphabetically before them. In w2 and w3, no one saw anyone. *)
  91   let saw1 yy xx = X.(map2 (fun x y -> x < y) xx yy)
  92   let saw2 yy xx = X.(map2 (fun _ _ -> false) xx yy)
  93   let saw3 = saw2
  94
  95 (* Necessarily, Ann and Bill are married to each other; also Carol to Dave. *)
  96   let marriedto yy xx = X.(map2 (curry are_married) xx yy)
  97
  98 (* Actually, only Carol and Dave kiss. In w2, spouses kiss. In w3, there is no kissing. *)
  99   let kisses1 yy xx = X.(map2 (fun x y -> (x = Carol && y = Dave) || (x = Dave && y = Carol)) xx yy)
 100   let kisses2 yy xx = marriedto xx yy
 101   let kisses3 yy xx = X.(map2 (fun x y -> false) xx yy)
 102
 103 (* Actually, each husband loves only his wife and Frank also loves the women.
 104    In w2, all the men love Carol and Ella loves the wives.
 105    In w3, Frank loves everyone else. *)
 106   let loves1 yy xx = X.(map2 (fun x y -> (is_male x && are_married(x,y)) || (x = Frank && not (is_male y))) xx yy)
 107   let loves2 yy xx = X.(map2 (fun x y -> (is_male x && y = Carol) || (x = Ella && is_a_wife y)) xx yy)
 108   let loves3 yy xx = X.(map2 (fun x y -> x = Frank && x <> y) xx yy)
 109 end
 110
 111 module Test(S : SEMANTICS) : sig end = struct
 112   type result = True | False | Fail
 113   let print_result res = match res with True -> print_string "true" | False -> print_string "false" | Fail -> print_string "failure"
 114
 115   let check name expected expr =
 116     (match (try Some (S.run expr) with Not_found -> None) with
 117       | Some true -> if expected = True then true else begin print_string "Sentence \""; print_string name; print_string "\" failed: got true but expected "; print_result expected; print_newline (); false end
 118       | Some false -> if expected = False then true else begin print_string "Sentence \""; print_string name; print_string "\" failed: got false but expected "; print_result expected; print_newline (); false end
 119       | None -> if expected = Fail then true else begin print_string "Sentence \""; print_string name; print_string "\" failed: got failure but expected "; print_result expected; print_newline (); false end)
 120 (*
 121     with List.Short_list -> begin print_string "Sentence \""; print_string name; print_string "\" failed: got Short_list but expected "; print_result expected; print_newline (); false end
 122     with Failure "Unimplemented" -> begin print_string "Sentence \""; print_string name; print_endline "\" unimplemented."; true end
 123 *)
 124
 125   let dynamic res = if S.dynamic then res else Fail
 126
 127   let truth = S.(male bill)
 128   let falsehood = S.(female bill)
 129   let bool_results =
 130   [ check "true" True truth
 131   ; check "false" False falsehood
 132   ; check "true and true" True S.(truth &&& truth)
 133   ; check "true and false" False S.(truth &&& falsehood)
 134   ; check "false and true" False S.(falsehood &&& truth)
 135   ; check "false and false" False S.(falsehood &&& falsehood)
 136   ; check "true or true" True S.(truth ||| truth)
 137   ; check "true or false" True S.(truth ||| falsehood)
 138   ; check "false or true" True S.(falsehood ||| truth)
 139   ; check "false or false" False S.(falsehood ||| falsehood)
 140   ; check "true >>> true" True S.(truth >>> truth)
 141   ; check "true >>> false" False S.(truth >>> falsehood)
 142   ; check "false >>> true" True S.(falsehood >>> truth)
 143   ; check "false >>> false" True S.(falsehood >>> falsehood)
 144   ]
 145   let () = print_newline(); print_int (List.count not bool_results); print_endline " boolean test(s) failed."
 146
 147   let results =
 148   [ check "1. Bill is male" True S.(male bill)
 149   ; check "2. Bill is female" False S.(female bill)
 150   ; check "3. Bill isn't female" True S.(~~~ (female bill))
 151   ; check "4. Carol didn't leave" False S.(~~~ (left carol))
 152   ; S.extensional || check "5. Maybe Carol didn't leave" True S.(maybe (~~~ (left carol)))
 153   ; S.extensional || check "6. Maybe Ann didn't leave" False S.(maybe (~~~ (left ann)))
 154
 155   ; check "7. Some x. x is male" True S.(some 'x' (male getx))
 156   ; check "8. Some x. x isn't female" True S.(some 'x' (~~~ (female getx)))
 157   ; check "9. Some x. x left" True S.(some 'x' (left getx))
 158   ; check "10. Some x. x didn't leave" False S.(some 'x' (~~~ (left getx)))
 159   ; check "11. Every x. x left" True S.(every 'x' (left getx))
 160   ; check "12. Every x. x is female" False S.(every 'x' (female getx))
 161   ; check "13. Every x. x isn't male" False S.(every 'x' (~~~ (male getx)))
 162   ; check "14. (Some x. x is male) and Ann is female" True S.(some 'x' (male getx) &&& female ann)
 163   ; check "15. Some x. (x is male and Ann is female)" True S.(some 'x' (male getx &&& female ann))
 164
 165   ; check "16. Some x. (x is male and x is female)" False S.(some 'x' (male getx &&& female getx))
 166   ; check "17. Some x. (x is male) and Some x. x is female" True S.(some 'x' (male getx) &&& some 'x' (female getx))
 167
 168   ; check "18. Some x. (x is male and Some y. y is male)" True S.(some 'x' (male getx &&& some 'y' (male gety)))
 169   ; check "19. Some x. (x is male and Some y. y is female)" True S.(some 'x' (male getx &&& some 'y' (female gety)))
 170   ; check "20. Some x. (x is male and Some y. x is male)" True S.(some 'x' (male getx &&& some 'y' (male getx)))
 171   ; check "21. Some x. (x is male and Some y. x is female)" False S.(some 'x' (male getx &&& some 'y' (female getx)))
 172   ; check "22. Some x. (x is male and Some y. x isn't female)" True S.(some 'x' (male getx &&& some 'y' (~~~ (female getx))))
 173   ; check "23. Some x. (x is male and Some x. x is female)" True S.(some 'x' (male getx &&& some 'x' (female getx)))
 174
 175   ; check "24. Some x. (x is male) and Some y. (y is female and Bill is male)" True S.(some 'x' (male getx) &&& some 'y' (male gety &&& male bill))
 176   ; check "25. Some x. (x is male and Some y. (y is female and Bill is male))" True S.(some 'x' (male getx &&& some 'y' (female gety &&& male bill)))
 177   ; check "26. Some x. (x is male and Some y. (y is male and Bill is male))" True S.(some 'x' (male getx &&& some 'y' (male gety &&& male bill)))
 178   ; check "27. Some x. (x is male and Some y. (x is female and Bill is male))" False S.(some 'x' (male getx &&& some 'y' (female getx &&& male bill)))
 179   ; check "28. Some x. (x is male and Some y. (x isn't female and Bill is male))" True S.(some 'x' (male getx &&& some 'y' (~~~ (female getx) &&& male bill)))
 180   ; check "29. Some x. (x is male and Some y. (x is male and Bill is male))" True S.(some 'x' (male getx &&& some 'y' (male getx &&& male bill)))
 181
 182   ; check "30. Some x. (x is male and Some y. (y is female and x isn't female))" True S.(some 'x' (male getx &&& some 'y' (female gety &&& ~~~ (female getx))))
 183   ; check "31. Some x. (x is male and Some y. (y is female and x is single))" True S.(some 'x' (male getx &&& some 'y' (female gety &&& single getx)))
 184   ; check "32. Some x. (x is male and Some y. (y is female and x isn't single))" True S.(some 'x' (male getx &&& some 'y' (female gety &&& ~~~ (single getx))))
 185   ; check "33. Some x. (x is male and Some y. (y is male and x is single))" True S.(some 'x' (male getx &&& some 'y' (male gety &&& single getx)))
 186   ; check "34. Some x. (x is male and Some y. (y is male and x isn't single))" True S.(some 'x' (male getx &&& some 'y' (male gety &&& ~~~ (single getx))))
 187
 188   ; check "35. Some x. (x is male and Some y. (x is female and x is single))" False S.(some 'x' (male getx &&& some 'y' (female getx &&& single getx)))
 189   ; check "36. Some x. (x is male and Some y. (x is female and x isn't single))" False S.(some 'x' (male getx &&& some 'y' (female getx &&& ~~~ (single getx))))
 190   ; check "37. Some x. (x is male and Some y. (x is male and x is single))" True S.(some 'x' (male getx &&& some 'y' (male getx &&& single getx)))
 191   ; check "38. Some x. (x is male and Some y. (x is male and x isn't single))" True S.(some 'x' (male getx &&& some 'y' (male getx &&& ~~~ (single getx))))
 192
 193   ; check "39. (Some x. male x) and x left" (dynamic True) S.(some 'x' (male getx) &&& left getx)
 194   ; check "40. (Some x. male x) and female x" (dynamic False) S.(some 'x' (male getx) &&& female getx)
 195   ; check "41. (Some x. male x) and Some y. female x" (dynamic False) S.(some 'x' (male getx) &&& some 'y' (female getx))
 196   ; check "42. (Some x. male x) and Some y. male x" (dynamic True) S.(some 'x' (male getx) &&& some 'y' (male getx))
 197   ; check "43. (Some x. male x) and Some y. (female x and male Bill)" (dynamic False) S.(some 'x' (male getx) &&& some 'y' (female getx &&& male bill))
 198   ; check "44. (Some x. male x) and Some y. (male x and male Bill)" (dynamic True) S.(some 'x' (male getx) &&& some 'y' (male getx &&& male bill))
 199   ; check "45. (Some x. male x) and Some y. (female y and x isn't single)" (dynamic True) S.(some 'x' (male getx) &&& some 'y' (female gety &&& ~~~ (single getx)))
 200   ; check "46. (Some x. male x) and Some y. (female x and x isn't single)" (dynamic False) S.(some 'x' (male getx) &&& some 'y' (female getx &&& ~~~ (single getx)))
 201   ; check "47. (Some x. male x) and Some y. (male x and x isn't single)" (dynamic True) S.(some 'x' (male getx) &&& some 'y' (male getx &&& ~~~ (single getx)))
 202
 203   ; check "48. Every x. (male x and (Some y. married y x) -> loves y x)" (dynamic True) S.(every 'x' (male getx &&& some 'y' (marriedto gety getx) >>> loves gety getx))
 204   ; check "49. Every x. (male x and (Some y. married y x) -> kisses y x)" (dynamic False) S.(every 'x' (male getx &&& some 'y' (marriedto gety getx) >>> kisses gety getx))
 205   ; check "50. (Some x. (male x and Some y. married y x)) -> loves y x" (dynamic True) S.(some 'x' (male getx &&& some 'y' (marriedto gety getx)) >>> loves gety getx)
 206   ; check "51. (Some x. (male x and Some y. married y x)) -> kisses y x" (dynamic False) S.(some 'x' (male getx &&& some 'y' (marriedto gety getx)) >>> kisses gety getx)
 207
 208   ; check "52. Every x. (male x and Some y. (female y and (x = frank or married y x)) -> loves y x)" (dynamic True) S.(every 'x' (male getx &&& some 'y' (female gety &&& (getx === frank ||| marriedto gety getx)) >>> loves gety getx))
 209   ; check "53. Every x. (male x and (x = frank or Some y. married y x) -> loves y x)" (dynamic Fail) S.(every 'x' (male getx &&& (getx === frank ||| some 'y' (marriedto gety getx)) >>> loves gety getx))
 210   ; check "54. Every x. (male x and (Some y. (x = frank and female y) or Some y. married y x) -> loves y x)" (dynamic Fail) S.(every 'x' (male getx &&& (some 'y' (getx === frank &&& female gety) ||| some 'y' (marriedto gety getx)) >>> loves gety getx))
 211   ; check "55. Every x. (male x and ((x = frank and Some y. female y) or Some y. married y x) -> loves y x)" (dynamic Fail) S.(every 'x' (male getx &&& ((getx === frank &&& some 'y' (female gety)) ||| some 'y' (marriedto gety getx)) >>> loves gety getx))
 212   ]
 213   let () = print_newline(); print_int (List.count not results); print_endline " test(s) failed."
 214
 215 end
 216
 217 (* create lots of monads, so that we have them if we need them *)
 218
 219 module L = Monad.List
 220 module R = Monad.Reader(struct type env = identifier -> entity end)
 221 module R' = Monad.Reader(struct type env = identifier -> int end)
 222 module Y = Monad.Reader(struct type env = world end)
 223 module S = Monad.State(struct type store = identifier -> entity end)
 224 module S' = Monad.State(struct type store = identifier -> int end)
 225
 226 module RY = struct
 227   include R.T(Y)
 228   include Monad.Derive.Reader_dbl(Y)(R.T(Y))
 229 end
 230 module YR = struct
 231   include Y.T(R)
 232   include Monad.Derive.Reader_dbl(R)(Y.T(R))
 233 end
 234 module LR = struct
 235   include L.T(R)
 236   include Monad.Derive.Reader(R)(L.T(R))
 237 end
 238 module LY = struct
 239   include L.T(Y)
 240   include Monad.Derive.Reader(Y)(L.T(Y))
 241 end
 242 module RL = struct
 243   include R.M(L)
 244   include Monad.Derive.List(L)(R.M(L))
 245 end
 246 module YL = struct
 247   include Y.M(L)
 248   include Monad.Derive.List(L)(Y.M(L))
 249 end
 250
 251 module SY = struct
 252   include S.T(Y)
 253   include Monad.Derive.Reader(Y)(S.T(Y))
 254 end
 255 module YS = struct
 256   include Y.T(S)
 257   include Monad.Derive.State(S)(Y.T(S))
 258 end
 259 module LS = struct
 260   include L.T(S)
 261   include Monad.Derive.State(S)(L.T(S))
 262 end
 263 module LY = struct
 264   include L.T(Y)
 265   include Monad.Derive.Reader(Y)(L.T(Y))
 266 end
 267 module SL = struct
 268   include S.M(L)
 269   include Monad.Derive.List(L)(S.M(L))
 270 end
 271 module YL = struct
 272   include Y.M(L)
 273   include Monad.Derive.List(L)(Y.M(L))
 274 end
 275
 276 module S'Y = struct
 277   include S'.T(Y)
 278   include Monad.Derive.Reader(Y)(S'.T(Y))
 279 end
 280 module YS' = struct
 281   include Y.T(S')
 282   include Monad.Derive.State(S')(Y.T(S'))
 283 end
 284 module LS' = struct
 285   include L.T(S')
 286   include Monad.Derive.State(S')(L.T(S'))
 287 end
 288 module S'L = struct
 289   include S'.M(L)
 290   include Monad.Derive.List(L)(S'.M(L))
 291 end
 292
 293 module LRY = struct
 294   include L.T(RY)
 295   include Monad.Derive.Reader2(RY)(L.T(RY))
 296 end
 297 module LYR = struct
 298   include L.T(YR)
 299   include Monad.Derive.Reader2(YR)(L.T(YR))
 300 end
 301 module RLY = struct
 302   include R.M(LY)
 303   include Monad.Derive.List(LY)(R.M(LY))
 304   include Monad.Derive.Reader_dbl(LY)(R.M(LY))
 305 end
 306 module RYL = struct
 307   include R.M(YL)
 308   include Monad.Derive.List(YL)(R.M(YL))
 309   include Monad.Derive.Reader_dbl(YL)(R.M(YL))
 310 end
 311 module YLR = struct
 312   include Y.M(LR)
 313   include Monad.Derive.List(LR)(Y.M(LR))
 314   include Monad.Derive.Reader_dbl(LR)(Y.M(LR))
 315 end
 316 module YRL = struct
 317   include Y.M(RL)
 318   include Monad.Derive.List(RL)(Y.M(RL))
 319   include Monad.Derive.Reader_dbl(RL)(Y.M(RL))
 320 end
 321
 322 module LSY = struct
 323   include L.T(SY)
 324   include Monad.Derive.Reader(SY)(L.T(SY))
 325   include Monad.Derive.State(SY)(L.T(SY))
 326 end
 327 module LYS = struct
 328   include L.T(YS)
 329   include Monad.Derive.Reader(YS)(L.T(YS))
 330   include Monad.Derive.State(YS)(L.T(YS))
 331 end
 332 module SLY = struct
 333   include S.M(LY)
 334   include Monad.Derive.List(LY)(S.M(LY))
 335   include Monad.Derive.Reader(LY)(S.M(LY))
 336 end
 337 module SYL = struct
 338   include S.M(YL)
 339   include Monad.Derive.List(YL)(S.M(YL))
 340   include Monad.Derive.Reader(YL)(S.M(YL))
 341 end
 342 module YLS = struct
 343   include Y.M(LS)
 344   include Monad.Derive.List(LS)(Y.M(LS))
 345   include Monad.Derive.State(LS)(Y.M(LS))
 346 end
 347 module YSL = struct
 348   include Y.M(SL)
 349   include Monad.Derive.List(SL)(Y.M(SL))
 350   include Monad.Derive.State(SL)(Y.M(SL))
 351 end
 352
 353 module LS'Y = struct
 354   include L.T(S'Y)
 355   include Monad.Derive.Reader(S'Y)(L.T(S'Y))
 356   include Monad.Derive.State(S'Y)(L.T(S'Y))
 357 end
 358 module LYS' = struct
 359   include L.T(YS')
 360   include Monad.Derive.Reader(YS')(L.T(YS'))
 361   include Monad.Derive.State(YS')(L.T(YS'))
 362 end
 363 module S'LY = struct
 364   include S'.M(LY)
 365   include Monad.Derive.List(LY)(S'.M(LY))
 366   include Monad.Derive.Reader(LY)(S'.M(LY))
 367 end
 368 module S'YL = struct
 369   include S'.M(YL)
 370   include Monad.Derive.List(YL)(S'.M(YL))
 371   include Monad.Derive.Reader(YL)(S'.M(YL))
 372 end
 373 module YLS' = struct
 374   include Y.M(LS')
 375   include Monad.Derive.List(LS')(Y.M(LS'))
 376   include Monad.Derive.State(LS')(Y.M(LS'))
 377 end
 378 module YS'L = struct
 379   include Y.M(S'L)
 380   include Monad.Derive.List(S'L)(Y.M(S'L))
 381   include Monad.Derive.State(S'L)(Y.M(S'L))
 382 end
 383
 384
 385 (*
 386    A variety of semantics are provided. Here is the naming scheme:
 387
 388    Sem1* is classic semantics with support for variable binding/anaphora.
 389    Sem5* would be the dynamic alternative of 1*. (not here provided, but
 390    discussed in comments.)
 391    You can't implement quantification in these,
 392    except by bringing in some of the mechanisms of a list/set component.
 393    (You'll create a box([entity]) and convert it to a box([bool]),
 394    then convert the latter to box(bool).)
 395    However, Haskell already provides the needed mechanisms in the basic Monad API (as the
 396    function Juli8 names `seq`), so we can do quantification without _explicitly
 397    invoking_ a ListT in our monadic stack.
 398
 399    Sem2* and Sem 6* would be the intensionalized versions of those.
 400    (Not here provided, but Sem6* is discussed in comments.)
 401
 402    Sem3* adds a List component to the stack to do quantification.
 403    Sem7* is the dynamic counterpart.
 404
 405    Sem4* adds an (additional) Reader monad for intensionality.
 406    Sem8* is the dynamic counterpart.
 407
 408    Within that broad organization, here are the sub-patterns:
 409
 410    SemNa uses just a bool payload, so sent types are box(bool).
 411    SemNb makes sent types the Klesli variant of Na, so sent types are
 412    bool -> box(bool).
 413    SemNc uses instead a unit payload, which we can do when the monadic
 414    stack has a List or Option component; then false will be the monad's
 415    mzero, whereas truth will be instances of type box(unit) that aren't
 416    mzero.
 417    SemNd would be the Kleisli variant of Nc, as Nb is the Kleisli variant
 418    of Na.
 419    SemNe (only for dynamic) would use "topics" or sequences of entities being discussed
 420    as payloads, so sent types are box(topic). What we really provide
 421    here is the Kleisli variation of this (SemNf), so sent types = topic -> box(topic).
 422 *)
 423
 424
 425 module Sem1a = struct
 426   let dynamic = false
 427   let extensional = true
 428
 429   (* We use monad R, with env = var -> entity.
 430      Types of sentences are env -> bool. *)
 431   module X = R
 432   type noun = entity X.t
 433   type sent = bool X.t
 434   let run (xx : sent) : bool = X.(run xx env0 = true)
 435   let getx = X.(asks (lookup 'x'))
 436   let gety = X.(asks (lookup 'y'))
 437   let getz = X.(asks (lookup 'z'))
 438   let let_ c (xx : noun) (body : sent) = X.(xx >>= fun x -> shift (insert c x) body)
 439
 440   let (~~~) xx = X.(map not xx)
 441   let (&&&) xx yy = X.(xx >>= fun b' -> if not b' then mid false else yy)
 442   let (|||) xx yy = X.(xx >>= fun b' -> if b' then mid true else yy)
 443   let (>>>) xx yy = X.(xx >>= fun b' -> if not b' then mid true else yy)
 444
 445   let some c (body : sent) =
 446     let (bbs : bool X.t list) = List.map (fun x -> let_ c X.(mid x) body) domain in
 447     let (bsb : bool list X.t) = X.seq bbs in
 448     let (bb : bool X.t) = X.map (exists ident) bsb in
 449     bb
 450   let every c (body : sent) =
 451     let (bbs : bool X.t list) = List.map (fun x -> let_ c X.(mid x) body) domain in
 452     let (bsb : bool list X.t) = X.seq bbs in
 453     let (bb : bool X.t) = X.map (for_all ident) bsb in
 454     bb
 455
 456   module F = Facts(X)
 457   let ann = X.(mid Ann) let bill = X.(mid Bill) let carol = X.(mid Carol) let dave = X.(mid Dave) let ella = X.(mid Ella) let frank = X.(mid Frank)
 458   let (===) xx yy = X.(map2 (=) xx yy)
 459   let male = F.male let female = F.female let single = F.single let left = F.left1
 460   let marriedto = F.marriedto let saw = F.saw1 let kisses = F.kisses1 let loves = F.loves1
 461   let thinks pp xx = failwith "Unimplemented"
 462   let maybe pp = failwith "Unimplemented"
 463 end (* Sem1a *)
 464
 465 module Sem1b = struct
 466   let dynamic = false
 467   let extensional = true
 468
 469   (* We again use monad R, with env = var -> entity.
 470      This variant defines sentence meanings as Kleisli arrows, that is:
 471        type sent = bool -> bool X.t
 472      or equivalently, bool -> (env -> bool). A true sentence takes any bool
 473      input to a boxed version of that input (so truth = mid), and a false
 474      sentence takes any input to mid false.
 475      This more closely parallels the dynamic semantics (though it should not,
 476      just on account of that structural similarity, be itself counted as dynamic).
 477      It also brings the boolean operations closer to monadic primitives.
 478   *)
 479   module X = R
 480   type noun = entity X.t
 481   type sent = bool -> bool X.t
 482   let run (k : sent) : bool = X.(run (k true) env0 = true)
 483   let getx = X.(asks (lookup 'x'))
 484   let gety = X.(asks (lookup 'y'))
 485   let getz = X.(asks (lookup 'z'))
 486   let let_ c (xx : noun) (body : sent) = fun b -> X.(xx >>= fun x -> shift (insert c x) (body b))
 487
 488   let (~~~) k = fun b -> X.(if b then map not (k true) else mid false)
 489   let (&&&) k j = X.(k >=> j)
 490   let (|||) k j = ~~~ (~~~ k &&& ~~~ j)
 491   let (>>>) k j = ~~~ k ||| j
 492 (* or
 493   let (|||) xx yy = fun b -> X.(xx b >>= fun b' -> if b' then mid true else yy b)
 494   let (>>>) xx yy = fun b -> X.(xx b >>= fun b' -> if not b' then mid true else yy b)
 495   let (>>>) k j = ~~~ (k &&& ~~~ j)
 496 *)
 497
 498   let some c (body : sent) = fun b ->
 499     let (bbs : bool X.t list) = List.map (fun x -> let_ c X.(mid x) body b) domain in
 500     let (bsb : bool list X.t) = X.seq bbs in
 501     let (bb : bool X.t) = X.map (exists ident) bsb in
 502     bb
 503   let every c (body : sent) = fun b ->
 504     let (bbs : bool X.t list) = List.map (fun x -> let_ c X.(mid x) body b) domain in
 505     let (bsb : bool list X.t) = X.seq bbs in
 506     let (bb : bool X.t) = X.map (for_all ident) bsb in
 507     bb
 508
 509   module F = Facts(X)
 510   let to_kleisli xx = fun b -> X.(xx >>= fun b' -> mid (b && b'))
 511   let ann = X.(mid Ann) let bill = X.(mid Bill) let carol = X.(mid Carol) let dave = X.(mid Dave) let ella = X.(mid Ella) let frank = X.(mid Frank)
 512   let (===) xx yy = to_kleisli X.(map2 (=) xx yy)
 513   let male = to_kleisli % F.male let female = to_kleisli % F.female let single = to_kleisli % F.single let left = to_kleisli % F.left1
 514   let marriedto yy xx = to_kleisli (F.marriedto yy xx) let saw yy xx = to_kleisli (F.saw1 yy xx) let kisses yy xx = to_kleisli (F.kisses1 yy xx) let loves yy xx = to_kleisli (F.loves1 yy xx)
 515   let thinks pp xx = fun b -> failwith "Unimplemented"
 516   let maybe pp = fun b -> failwith "Unimplemented"
 517 end (* Sem1b *)
 518
 519 module Sem3a = struct
 520   let dynamic = false
 521   let extensional = true
 522
 523   (* We could use either monad RL or LR, with type env = var -> entity.
 524      Their box type is the same: env -> ['a]
 525      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.
 526      We use the box type in two ways: first, we use a box(entity) to compute whether a matrix
 527      clause is satisfied by a bound pronoun, where entity ranges over the whole domain.
 528      Second, it is convenient and more consonant with later strategies
 529      to re-use the same monad for sentence types (rather than using a simpler monad
 530      that lacks a List component). Here we will let the types of sentences
 531      be box(bool), that is: env -> [bool]. We will understand the sentence to be true
 532      if there are ANY truths in the resulting list. A list of all falses is treated
 533      the same as an empty list. Sem3c, below, eliminates this artifact by changing
 534      the sentence type to box(unit). Then truths (rel to an env) are [();...] and
 535      falsehoods are [].
 536 *)
 537   module X = LR
 538   type noun = entity X.t
 539   type sent = bool X.t
 540   let run (xx : sent) : bool = X.(any_truths (run xx env0))
 541   (* lift an 'a list to a single 'a X.t *)
 542   let mids (xs : 'a list) : 'a X.t = let rec aux xx = function [] -> xx | x::xs -> aux X.(xx ++ mid x) xs in aux X.mzero xs
 543   let getx = X.(asks (lookup 'x'))
 544   let gety = X.(asks (lookup 'y'))
 545   let getz = X.(asks (lookup 'z'))
 546   let let_ c (xx : noun) (body : sent) = X.(xx >>= fun x -> shift (insert c x) body)
 547
 548   let (~~~) xx = X.(map not xx)
 549   let (&&&) xx yy = X.(xx >>= fun b' -> if not b' then mid false else yy)
 550   let (|||) xx yy = X.(xx >>= fun b' -> if b' then mid true else yy)
 551   let (>>>) xx yy = X.(xx >>= fun b' -> if not b' then mid true else yy)
 552
 553   (* On this semantics, `some c body` is a list of the boolean outcomes for body for each assignment to c.
 554      That matches our convention for sentence types, where any truth in the list means the sentence is true.
 555      However, we can't then define `every c body === ~~~ (some c (~~~ body))`, because it's only when the rhs is entirely true that the lhs should be true.
 556      In later semantics, the duality of `some` and `every` will be restored.
 557   *)
 558   let some c (body : sent) = X.(let_ c (mids domain) body)
 559   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) (* could alternatively return [true] instead of xs *)
 560
 561   module F = Facts(X)
 562   let ann = X.(mid Ann) let bill = X.(mid Bill) let carol = X.(mid Carol) let dave = X.(mid Dave) let ella = X.(mid Ella) let frank = X.(mid Frank)
 563   let (===) xx yy = X.(map2 (=) xx yy)
 564   let male = F.male let female = F.female let single = F.single let left = F.left1
 565   let marriedto = F.marriedto let saw = F.saw1 let kisses = F.kisses1 let loves = F.loves1
 566   let thinks pp xx = failwith "Unimplemented"
 567   let maybe pp = failwith "Unimplemented"
 568 end (* Sem3a *)
 569
 570 (* Sem3b would convert Sem3a into having sentence meanings be Kleisli arrows, as Sem1b did.
 571    Not here implemented. *)
 572
 573 (* Variant of Sem3a, which uses [();...] vs [] instead of [true;...] vs (list of all false OR []). *)
 574 module Sem3c = struct
 575   let dynamic = false
 576   let extensional = true
 577
 578   (* We use monad LR as above, with same env = var -> entity and box type = env -> ['a].
 579      We again use box(entity) to compute whether matrix clauses are satisfied by
 580      bound pronouns; but now we use box(unit) for the types of sentences.
 581      Truths (rel to an env) are [();...] and falsehood is [].
 582   *)
 583   module X = LR
 584   type noun = entity X.t
 585   type sent = unit X.t
 586   let run (xx : sent) : bool = X.(not (List.is_null (run xx env0)))
 587   (* lift an 'a list to a single 'a X.t *)
 588   let mids (xs : 'a list) : 'a X.t = let rec aux xx = function [] -> xx | x::xs -> aux X.(xx ++ mid x) xs in aux X.mzero xs
 589   let getx = X.(asks (lookup 'x'))
 590   let gety = X.(asks (lookup 'y'))
 591   let getz = X.(asks (lookup 'z'))
 592   let let_ c (xx : noun) (body : sent) = X.(xx >>= fun x -> shift (insert c x) body)
 593   let to_unit (x : bool) : unit X.t = X.guard x
 594
 595   let (~~~) xx = X.(list_map (fun xs -> if is_null xs then [()] else []) xx)
 596   let (&&&) xx yy = X.(xx >> yy)
 597   let (|||) xx yy = X.(xx ++ (* ~~~ xx >> *) yy)
 598   let (>>>) xx yy = X.(~~~ xx ++ yy)
 599 (* or
 600   let (>>>) xx yy = X.(~~~ (xx >> ~~~ yy))
 601 *)
 602
 603   let some c (body : sent) = X.(let_ c (mids domain) body)
 604   let every c (body : sent) = ~~~ (some c (~~~ body))
 605
 606   module F = Facts(X)
 607   let ann = X.(mid Ann) let bill = X.(mid Bill) let carol = X.(mid Carol) let dave = X.(mid Dave) let ella = X.(mid Ella) let frank = X.(mid Frank)
 608   let (===) xx yy = X.(map2 (=) xx yy >>= to_unit)
 609   let male xx = X.(F.male xx >>= to_unit)
 610   let female xx = X.(F.female xx >>= to_unit)
 611   let single xx = X.(F.single xx >>= to_unit)
 612   let left xx = X.(F.left1 xx >>= to_unit)
 613   let marriedto yy xx = X.(F.marriedto yy xx >>= to_unit)
 614   let saw yy xx = X.(F.saw1 yy xx >>= to_unit)
 615   let kisses yy xx = X.(F.kisses1 yy xx >>= to_unit)
 616   let loves yy xx = X.(F.loves1 yy xx >>= to_unit)
 617   let thinks pp xx = failwith "Unimplemented"
 618   let maybe pp = failwith "Unimplemented"
 619 end (* Sem3c *)
 620
 621 (* Sem3d would convert Sem3c into having sentence meanings be Kleisli arrows, as Sem1b did.
 622    Not here implemented. *)
 623
 624 (* Add intensionality to 2a *)
 625 module Sem4a = struct
 626   let dynamic = false
 627   let extensional = false
 628
 629   (* Using monad LRY, with type env = var -> entity.
 630      Box type is env -> world -> ['a]
 631      Types of sentences are env -> world -> [bool]. *)
 632   module X = LRY
 633   type noun = entity X.t
 634   type sent = bool X.t
 635   let run xx = X.(any_truths (run xx env0 Actual))
 636   (* lift an 'a list to a single 'a X.t *)
 637   let mids (xs : 'a list) : 'a X.t = let rec aux xx = function [] -> xx | x::xs -> aux X.(xx ++ mid x) xs in aux X.mzero xs
 638   let getx = X.(asks (lookup 'x'))
 639   let gety = X.(asks (lookup 'y'))
 640   let getz = X.(asks (lookup 'z'))
 641   let getw = X.(uask) (* get world from the underlying Y monad *)
 642   (* select an intranstive verb based on the world *)
 643   let select1 f1 f2 f3 xx = X.(getw >>= fun w -> (if w = Actual then f1 else if w = Second then f2 else f3) xx)
 644   (* select a transitive verb based on the world *)
 645   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)
 646   let let_ c (xx : noun) (body : sent) = X.(xx >>= fun x -> shift (insert c x) body)
 647   let letw world (body : sent) = X.(ushift (fun _ -> world) body) (* shift the "env" of the underlying Y monad *)
 648
 649   let (~~~) xx = X.(map not xx)
 650   let (&&&) xx yy = X.(xx >>= fun b' -> if not b' then mid false else yy)
 651   let (|||) xx yy = X.(xx >>= fun b' -> if b' then mid true else yy)
 652   let (>>>) xx yy = X.(xx >>= fun b' -> if not b' then mid true else yy)
 653
 654   let some c (body : sent) = X.(let_ c (mids domain) body)
 655   let every c (body : sent) = X.(let xx = let_ c (mids domain) body in list_map (fun xs -> if all_truths xs then xs else []) xx)
 656
 657   module F = Facts(X)
 658   let ann = X.(mid Ann) let bill = X.(mid Bill) let carol = X.(mid Carol) let dave = X.(mid Dave) let ella = X.(mid Ella) let frank = X.(mid Frank)
 659   let (===) xx yy = X.(map2 (=) xx yy)
 660   let male = F.male let female = F.female let single = F.single
 661   let left xx = select1 F.left1 F.left2 F.left3 xx
 662   let saw yy xx = select2 F.saw1 F.saw2 F.saw3 yy xx
 663   let marriedto = F.marriedto
 664   let kisses yy xx = select2 F.kisses1 F.kisses2 F.kisses3 yy xx
 665   let loves yy xx = select2 F.loves1 F.loves2 F.loves3 yy xx
 666   let thinks pp xx = failwith "Unimplemented"
 667   let maybe (body : sent) : sent =
 668     let (yy : R.env -> Y.env -> bool list) = fun e w ->
 669       let body_int = List.map (fun w' -> any_truths (X.run (letw w' body) e w)) modal_domain in
 670       body_int (* can just use body's intension as the result of `maybe body` *) in
 671     Obj.magic yy
 672 end (* Sem4a *)
 673
 674 (* Sem4b would convert Sem4a into having sentence meanings be Kleisli arrows, as Sem1b did.
 675    Not here implemented. *)
 676
 677 (* Add intensionality to 2c *)
 678 module Sem4c = struct
 679   let dynamic = false
 680   let extensional = false
 681
 682   (* Using monad LRY, with type env = var -> entity.
 683      Box type is env -> world -> ['a]
 684      Types of sentences are env -> world -> [unit]. *)
 685   module X = LRY
 686   type noun = entity X.t
 687   type sent = unit X.t
 688   let run xx = X.(not (List.is_null (run xx env0 Actual)))
 689   (* lift an 'a list to a single 'a X.t *)
 690   let mids (xs : 'a list) : 'a X.t = let rec aux xx = function [] -> xx | x::xs -> aux X.(xx ++ mid x) xs in aux X.mzero xs
 691   let getx = X.(asks (lookup 'x'))
 692   let gety = X.(asks (lookup 'y'))
 693   let getz = X.(asks (lookup 'z'))
 694   let getw = X.(uask) (* get world from the underlying Y monad *)
 695   (* select an intranstive verb based on the world *)
 696   let select1 f1 f2 f3 xx = X.(getw >>= fun w -> (if w = Actual then f1 else if w = Second then f2 else f3) xx)
 697   (* select a transitive verb based on the world *)
 698   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)
 699   let let_ c (xx : noun) (body : sent) = X.(xx >>= fun x -> shift (insert c x) body)
 700   let letw world (body : sent) = X.(ushift (fun _ -> world) body) (* shift the "env" of the underlying Y monad *)
 701   let to_unit (x : bool) : unit X.t = X.guard x
 702
 703   let (~~~) xx = X.(list_map (fun xs -> if is_null xs then [()] else []) xx)
 704   let (&&&) xx yy = X.(xx >> yy)
 705   let (|||) xx yy = X.(xx ++ (* ~~~ xx >> *) yy)
 706   let (>>>) xx yy = X.(~~~ xx ++ yy)
 707 (* or
 708   let (>>>) xx yy = X.(~~~ (xx >> ~~~ yy))
 709 *)
 710
 711   let some c (body : sent) = X.(let_ c (mids domain) body)
 712   let every c (body : sent) = ~~~ (some c (~~~ body))
 713
 714   module F = Facts(X)
 715   let ann = X.(mid Ann) let bill = X.(mid Bill) let carol = X.(mid Carol) let dave = X.(mid Dave) let ella = X.(mid Ella) let frank = X.(mid Frank)
 716   let (===) xx yy = X.(map2 (=) xx yy >>= to_unit)
 717   let male xx = X.(F.male xx >>= to_unit)
 718   let female xx = X.(F.female xx >>= to_unit)
 719   let single xx = X.(F.single xx >>= to_unit)
 720   let left xx = X.(select1 F.left1 F.left2 F.left3 xx >>= to_unit)
 721   let saw yy xx = X.(select2 F.saw1 F.saw2 F.saw3 yy xx >>= to_unit)
 722   let marriedto yy xx = X.(F.marriedto yy xx >>= to_unit)
 723   let kisses yy xx = X.(select2 F.kisses1 F.kisses2 F.kisses3 yy xx >>= to_unit)
 724   let loves yy xx = X.(select2 F.loves1 F.loves2 F.loves3 yy xx >>= to_unit)
 725   let thinks pp xx = failwith "Unimplemented"
 726   let maybe (body : sent) : sent =
 727     let (yy : R.env -> Y.env -> unit list) = fun e w ->
 728       let body_int = List.map (fun w' -> not @@ List.is_null @@ X.run (letw w' body) e w) modal_domain in
 729       if any_truths body_int then [()] else [] in
 730     Obj.magic yy
 731 end (* Sem4c *)
 732
 733 (* Sem4d would convert Sem4c into having sentence meanings be Kleisli arrows, as Sem1b did.
 734    Not here implemented. *)
 735
 736
 737 (* Dynamic version of Sem3c *)
 738 module Sem7c = struct
 739   let dynamic = true
 740   let extensional = true
 741
 742   (* This needs to use monad SL, with store = var -> entity
 743      and box type = store -> ['a,store]
 744      Sentence meaning is box(unit).
 745      Later strategies with more complex sentence meanings and stores
 746      may be able to use monad LS, with box type store -> ['a],store
 747   *)
 748   module X = SL
 749   type noun = entity X.t
 750   type sent = unit X.t
 751   let run (xx : sent) : bool = X.(not (List.is_null (run xx env0)))
 752   (* lift an 'a list to a single 'a X.t *)
 753   let mids (xs : 'a list) : 'a X.t = let rec aux xx = function [] -> xx | x::xs -> aux X.(xx ++ mid x) xs in aux X.mzero xs
 754   let getx = X.(gets (lookup 'x'))
 755   let gety = X.(gets (lookup 'y'))
 756   let getz = X.(gets (lookup 'z'))
 757   let let_ c (xx : noun) (body : sent) = X.(xx >>= fun x -> modify (insert c x) >> body)
 758   let to_unit (x : bool) : unit X.t = X.guard x
 759
 760   let (~~~) (xx : sent) : sent =
 761     let yy : S.store -> (unit * S.store) list = fun s -> if List.is_null (X.run xx s) then [(),s] else [] in
 762     Obj.magic yy  (* this is an identity function that changes the type of yy to a unit X.t *)
 763   let (&&&) xx yy = X.(xx >> yy)
 764   let (|||) xx yy = ~~~ (~~~ xx &&& ~~~ yy)
 765   let (>>>) xx yy = X.(~~~ (xx &&& ~~~ yy))
 766
 767 (*
 768     This would propagate effects out of the disjuncts, so that for example after
 769       "Some y. (x = frank and female y) or Some y. married y x"
 770     "y" would be available for anaphor:
 771       let (|||) xx yy = X.(xx ++ (~~~ xx >> yy))
 772
 773     This wouldn't propagate effects from antecedent to consequent, so that for example
 774       "(Some y. marriedto y bill) >>> female gety"
 775     has a failed lookup on "y":
 776       let (>>>) xx yy = X.(~~~ xx ++ yy)
 777 *)
 778
 779   let some c (body : sent) = X.(let_ c (mids domain) body)
 780   let every c (body : sent) = ~~~ (some c (~~~ body))
 781
 782   module F = Facts(X)
 783   let ann = X.(mid Ann) let bill = X.(mid Bill) let carol = X.(mid Carol) let dave = X.(mid Dave) let ella = X.(mid Ella) let frank = X.(mid Frank)
 784   let (===) xx yy = X.(map2 (=) xx yy >>= to_unit)
 785   let male xx = X.(F.male xx >>= to_unit)
 786   let female xx = X.(F.female xx >>= to_unit)
 787   let single xx = X.(F.single xx >>= to_unit)
 788   let left xx = X.(F.left1 xx >>= to_unit)
 789   let marriedto yy xx = X.(F.marriedto yy xx >>= to_unit)
 790   let saw yy xx = X.(F.saw1 yy xx >>= to_unit)
 791   let kisses yy xx = X.(F.kisses1 yy xx >>= to_unit)
 792   let loves yy xx = X.(F.loves1 yy xx >>= to_unit)
 793   let thinks pp xx = failwith "Unimplemented"
 794   let maybe pp = failwith "Unimplemented"
 795 end (* Sem7c *)
 796
 797
 798 (* Dynamic version of Sem4c / Add intensionality to Sem7c *)
 799 module Sem8c = struct
 800   let dynamic = true
 801   let extensional = false
 802
 803   (* This needs to use monad SLY, with store = var -> entity
 804      and box type = store -> world -> ['a,store]
 805      Sentence meaning is box(unit).
 806      Later strategies with more complex sentence meanings and stores
 807      may be able to use monad LSY, with box type store -> world -> ['a],store
 808   *)
 809   module X = SLY
 810   type noun = entity X.t
 811   type sent = unit X.t
 812   let run (xx : sent) : bool = X.(not (List.is_null (run xx env0 Actual)))
 813   (* lift an 'a list to a single 'a X.t *)
 814   let mids (xs : 'a list) : 'a X.t = let rec aux xx = function [] -> xx | x::xs -> aux X.(xx ++ mid x) xs in aux X.mzero xs
 815   let getx = X.(gets (lookup 'x'))
 816   let gety = X.(gets (lookup 'y'))
 817   let getz = X.(gets (lookup 'z'))
 818   let getw = X.(ask) (* get world from the underlying Y monad *)
 819   (* select an intranstive verb based on the world *)
 820   let select1 f1 f2 f3 xx = X.(getw >>= fun w -> (if w = Actual then f1 else if w = Second then f2 else f3) xx)
 821   (* select a transitive verb based on the world *)
 822   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)
 823   let let_ c (xx : noun) (body : sent) = X.(xx >>= fun x -> modify (insert c x) >> body)
 824   let letw world (body : sent) = X.(shift (fun _ -> world) body) (* shift the "env" of the underlying Y monad *)
 825   let to_unit (x : bool) : unit X.t = X.guard x
 826 (*
 827   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)
 828 *)
 829
 830   let (~~~) (xx : sent) : sent =
 831     let yy : S.store -> Y.env -> (unit * S.store) list = fun s w -> if List.is_null (X.run xx s w) then [(),s] else [] in
 832     Obj.magic yy  (* this is an identity function that changes the type of yy to a unit X.t *)
 833
 834   let (&&&) xx yy = X.(xx >> yy)
 835   let (|||) xx yy = ~~~ (~~~ xx &&& ~~~ yy)
 836   let (>>>) xx yy = X.(~~~ (xx &&& ~~~ yy))
 837
 838   let some c (body : sent) = X.(let_ c (mids domain) body)
 839   let every c (body : sent) = ~~~ (some c (~~~ body))
 840
 841   module F = Facts(X)
 842   let ann = X.(mid Ann) let bill = X.(mid Bill) let carol = X.(mid Carol) let dave = X.(mid Dave) let ella = X.(mid Ella) let frank = X.(mid Frank)
 843   let (===) xx yy = X.(map2 (=) xx yy >>= to_unit)
 844   let male xx = X.(F.male xx >>= to_unit)
 845   let female xx = X.(F.female xx >>= to_unit)
 846   let single xx = X.(F.single xx >>= to_unit)
 847   let left xx = X.(select1 F.left1 F.left2 F.left3 xx >>= to_unit)
 848   let saw yy xx = X.(select2 F.saw1 F.saw2 F.saw3 yy xx >>= to_unit)
 849   let marriedto yy xx = X.(F.marriedto yy xx >>= to_unit)
 850   let kisses yy xx = X.(select2 F.kisses1 F.kisses2 F.kisses3 yy xx >>= to_unit)
 851   let loves yy xx = X.(select2 F.loves1 F.loves2 F.loves3 yy xx >>= to_unit)
 852   let thinks pp xx = failwith "Unimplemented"
 853   let maybe (body : sent) : sent =
 854     let (yy : S.store -> Y.env -> (unit * S.store) list) = fun s w ->
 855       let body_int = List.map (fun w' -> not @@ List.is_null @@ X.run (letw w' body) s w) modal_domain in
 856       if any_truths body_int then [(),s] else [] in
 857     Obj.magic yy
 858 end (* Sem8c *)
 859
 860 (* 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.
 861    Next we develop some semantics that are closer to their actual presentation. *)
 862
 863 (* This develops Sem7c using in part the Kleisli strategy from Sem1b. *)
 864 module Sem7f = struct
 865   let dynamic = true
 866   let extensional = true
 867
 868   (* Let a topic be sequence of entities introduced into conversation (GSV's pegs -> entities, with pegs construed as positions in the sequence).
 869      Then let store = var -> int (that is, position in the topic)
 870      Then we can use monad LS', with box type = store -> ['a],store
 871      And sentence meanings are Kleisli arrows: topic -> box(topic). The list component
 872      in the type captures indeterminacy in what objects are being discussed (introduced
 873      by quantifiers). Truths (relative to a initial store and topic) result in
 874      non-empty topic lists; falsehoods in empty ones.
 875      Our stores/envs are GSV's refsys r; our topics are their g.
 876      Notice that GSV make their "information states" homogenous wrt r; this corresponds
 877      to our result type having stores _outside_ the list.
 878      GSV's meaning types are [store * topic * world] -> [store * topic * world], but
 879      as noted the homogeneity wrt store would permit also:
 880        store * [topic * world] -> store * [topic * world].
 881      Our meaning types (once we add worlds in 6e, below) will be:
 882        topic -> (store -> world -> ([topic] * store))
 883      We count a world as eliminated when it results in an empty list of topics.
 884      Note that our Sem8f doesn't yet properly handle Veltman's "might"; see remarks below.
 885   *)
 886   type topic = entity list
 887   let topic0 = []
 888   module X = LS'
 889   type noun = (topic -> entity) X.t
 890   type sent = topic -> topic X.t
 891   let run (k : sent) : bool = X.(not (List.is_null (fst (run (k topic0) env0))))
 892   (* lift an 'a list to a single 'a X.t *)
 893   let mids (xs : 'a list) : 'a X.t = let rec aux xx = function [] -> xx | x::xs -> aux X.(xx ++ mid x) xs in aux X.mzero xs
 894   let get_nth n topic = try List.nth topic n with List.Short_list -> failwith ("can't get item "^string_of_int n^" of "^List.string_of_list string_of_entity topic)
 895   let getx : noun = X.(gets (lookup 'x') >>= fun n -> mid (get_nth n))
 896   let gety : noun = X.(gets (lookup 'y') >>= fun n -> mid (get_nth n))
 897   let getz : noun = X.(gets (lookup 'z') >>= fun n -> mid (get_nth n))
 898   let let_ c (n : int) (body : sent) : sent = fun top -> X.(modify (insert c n) >> (body top))
 899
 900   (* All logical operations except &&& and some are "effect islands", with the exception that effects of the antecedent
 901      of a conditional are visible in that conditional's consequent. *)
 902
 903   let (~~~) (k : sent) : sent = fun top ->
 904     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
 905     Obj.magic yy  (* this is an identity function that changes the type of yy to a topic X.t *)
 906   let (&&&) k j = X.(k >=> j)
 907   let (|||) k j = ~~~ (~~~ k &&& ~~~ j)
 908   let (>>>) k j = X.(~~~ (k >=> ~~~ j))
 909
 910   (* This properly handles `some` as GSV do, by only joining the results
 911      _after_ updating them on body(extended topic). See GSV pp. 28-9. *)
 912   let some c (body : sent) : sent = fun top ->
 913     let n = length top in
 914     let aux ent = X.(let_ c n body) (List.snoc top ent) in
 915     let domain' = List.map aux domain in
 916     X.join (mids domain')
 917
 918   let every c (body : sent) = ~~~ (some c (~~~ body))
 919
 920   module F = Facts(X)
 921   let mapply' (ff : noun) (top : topic) : entity X.t = X.(map (fun f -> f top) ff)
 922   let wrap name = X.(mid (const name))
 923   let wrap1 f xx = fun top -> X.(f (mapply' xx top) >>= fun b -> if b then mid top else mzero)
 924   let wrap2 f xx yy = fun top -> X.(f (mapply' xx top) (mapply' yy top) >>= fun b -> if b then mid top else mzero)
 925   let ann = wrap Ann let bill = wrap Bill let carol = wrap Carol let dave = wrap Dave let ella = wrap Ella let frank = wrap Frank
 926   let (===) (xx : noun) (yy : noun) : sent = wrap2 X.(map2 (=)) xx yy
 927   let male (xx : noun) : sent = wrap1 F.male xx
 928   let female xx = wrap1 F.female xx
 929   let single xx = wrap1 F.single xx
 930   let left xx = wrap1 F.left1 xx
 931   let marriedto yy xx = wrap2 F.marriedto yy xx
 932   let saw yy xx = wrap2 F.saw1 yy xx
 933   let kisses yy xx = wrap2 F.kisses1 yy xx
 934   let loves yy xx = wrap2 F.loves1 yy xx
 935   let thinks pp xx = fun top -> failwith "Unimplemented"
 936   let maybe pp = fun top -> failwith "Unimplemented"
 937 end (* Sem7f *)
 938
 939 (* Add intensionality to Sem7f. See comments there. *)
 940 module Sem8f = struct
 941   let dynamic = true
 942   let extensional = false
 943
 944   type topic = entity list
 945   let topic0 = []
 946   module X = LS'Y
 947   type noun = (topic -> entity) X.t
 948   type sent = topic -> topic X.t
 949   let run (k : sent) : bool = X.(not (List.is_null (fst (run (k topic0) env0 Actual))))
 950   (* lift an 'a list to a single 'a X.t *)
 951   let mids (xs : 'a list) : 'a X.t = let rec aux xx = function [] -> xx | x::xs -> aux X.(xx ++ mid x) xs in aux X.mzero xs
 952   let get_nth n topic = try List.nth topic n with List.Short_list -> failwith ("can't get item "^string_of_int n^" of "^List.string_of_list string_of_entity topic)
 953   let getx : noun = X.(gets (lookup 'x') >>= fun n -> mid (get_nth n))
 954   let gety : noun = X.(gets (lookup 'y') >>= fun n -> mid (get_nth n))
 955   let getz : noun = X.(gets (lookup 'z') >>= fun n -> mid (get_nth n))
 956   let getw = X.(ask) (* get world from the underlying Y monad *)
 957   (* select an intranstive verb based on the world *)
 958   let select1 f1 f2 f3 xx = X.(getw >>= fun w -> (if w = Actual then f1 else if w = Second then f2 else f3) xx)
 959   (* select a transitive verb based on the world *)
 960   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)
 961   let let_ c (n : int) (body : sent) : sent = fun top -> X.(modify (insert c n) >> (body top))
 962   let letw world (body : sent) : sent = fun top -> X.(shift (fun _ -> world) (body top)) (* shift the "env" of the underlying Y monad *)
 963
 964   (* debugging *)
 965   let lookup_string sought env top = try string_of_entity (List.nth top (env sought)) with Not_found -> "*" | List.Short_list -> "#"
 966   let print_lookup sought env top = print_string (lookup_string sought env top)
 967   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)
 968   (* variant of run that uses a non-empty initial topic list, and displays entire result, not just whether it's true *)
 969   let run' (k : sent) ?(w=Actual) (tops : topic list) =
 970     let n = List.length (List.head tops) in
 971     let env = match n with
 972     | 1 -> insert 'x' 0 env0
 973     | 2 -> insert 'x' 0 (insert 'y' 1 env0)
 974     | 3 -> insert 'x' 0 (insert 'y' 1 (insert 'z' 2 env0))
 975     | _ -> failwith ("can't run' topics of length " ^ string_of_int n) in
 976     assert(for_all (fun top -> List.length top = n) tops);
 977     X.(run (mids tops >>= k) env w)
 978
 979   let (~~~) (k : sent) : sent = fun top ->
 980     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
 981     Obj.magic yy  (* this is an identity function that changes the type of yy to a topic X.t *)
 982   let (&&&) k j = X.(k >=> j)
 983   let (|||) k j = ~~~ (~~~ k &&& ~~~ j)
 984   let (>>>) k j = X.(~~~ (k >=> ~~~ j))
 985
 986   let some c (body : sent) : sent = fun top ->
 987     let n = length top in
 988     let aux ent = X.(let_ c n body) (List.snoc top ent) in
 989     let domain' = List.map aux domain in
 990     X.join (mids domain')
 991
 992   let every c (body : sent) = ~~~ (some c (~~~ body))
 993
 994   module F = Facts(X)
 995   let mapply' (ff : noun) (top : topic) : entity X.t = X.(map (fun f -> f top) ff)
 996   let wrap name = X.(mid (const name))
 997   let wrap1 f xx = fun top -> X.(f (mapply' xx top) >>= fun b -> if b then mid top else mzero)
 998   let wrap2 f xx yy = fun top -> X.(f (mapply' xx top) (mapply' yy top) >>= fun b -> if b then mid top else mzero)
 999   let ann = wrap Ann let bill = wrap Bill let carol = wrap Carol let dave = wrap Dave let ella = wrap Ella let frank = wrap Frank
1000   let (===) (xx : noun) (yy : noun) : sent = wrap2 X.(map2 (=)) xx yy
1001   let male (xx : noun) : sent = wrap1 F.male xx
1002   let female xx = wrap1 F.female xx
1003   let single xx = wrap1 F.single xx
1004   let left xx = wrap1 (select1 F.left1 F.left2 F.left3) xx
1005   let marriedto yy xx = wrap2 F.marriedto yy xx
1006   let saw yy xx = wrap2 (select2 F.saw1 F.saw2 F.saw3) yy xx
1007   let kisses yy xx = wrap2 (select2 F.kisses1 F.kisses2 F.kisses3) yy xx
1008   let loves yy xx = wrap2 (select2 F.loves1 F.loves2 F.loves3) yy xx
1009   let thinks pp xx = failwith "Unimplemented"
1010   let maybe (body : sent) : sent = fun top ->
1011     let (yy : S'.store -> Y.env -> topic list * S'.store) = fun s w ->
1012       let body_int = List.map (fun w' -> not @@ List.is_null @@ fst @@ X.run (letw w' body top) s w) modal_domain in
1013       if any_truths body_int then [top],s else [],s in
1014     Obj.magic yy
1015   (* This implementation of `maybe` doesn't yet exactly capture Veltman's "might". It isn't a holistic filter:
1016      it examines topics one-by-one and will eliminate any where they (considered in isolation) make body impossible.
1017      Hence, if some of the possible referents for x are essentially not-body, and others are possibly-body, after
1018      updating on _this_ implementation of `maybe body`, we'll be left with only the latter. On Veltman's semantics,
1019      otoh, we'd be left with the whole original information state.
1020      To capture Veltman's semantics properly, we'd need to remove the List component from our monad stack, and use
1021      [topic] as our payloads, so that sent types would then be: [topic] -> S'Y([topic]). All of the operations except
1022      for `maybe` would then have to emulate the operations of the List monad by hand (manually performing catmap etc).
1023      But `maybe` could examine the [topic] as a whole and decide whether to return box(it) or box([]).
1024      This would be to go back to the Sem5/Sem6 choices of monads (without list), and to implement the handling of lists
1025      by hand, as we did in the Sem1/Sem2 strategies.
1026
1027      Additionally, we haven't tried here to handle non-rigid noun-types. That's why we can have sent types be:
1028          topic (or [topic]) -> store -> world -> ([topic], store)
1029      the input topic doesn't depend on what the world is. GSV's types are suited to handle non-rigid noun types,
1030      since they are instead using an analogue of (world * topic) -> store -> ([world,topic], store). We could follow suit,
1031      removing the Reader monad implementing Intensionality from our stack and implementing that by hand, too. Another
1032      strategy would be to continue using a Reader monad but not by merging it into our main monad stack, instead using
1033      values of _that_ box type as _payloads for_ our main box type. This echoes a question raised by Dylan in seminar:
1034      why must we combine the monads only by way of "stacking them" into a single monad? As Jim said in seminar, it's not
1035      obvious one must do so, it just seems most natural. The strategy being evisaged now would at least in part follow
1036      Dylan's suggestion. We'd let our sentence types then be:
1037          intensionality_box([topic]) -> state_plus_intensionality_box(intensionality_box([topic]))
1038        = intensionality_box([topic]) -> store -> world -> (intensionality_box([topic]) * store)
1039      In that case, I think we could once again merge the list component into the intensionality_box type, getting:
1040          intens_list_box(topic) -> state_intens_box(intens_list_box(topic))
1041        = intens_list_box(topic) -> store -> world -> (intens_list_box(topic) * store)
1042        = (world -> [topic]) -> store -> world -> ((world -> [topic]) * store)
1043      That looks like a pretty complicated type, and might not seem an improvement over GSV's own system. But its advantage is that
1044      the implementation of its operations would so closely parallel the other semantic strategies illustrated above.
1045      Testifying to the "modularity" of monads, which we have been recommending as one of their prominent virtues.
1046   *)
1047
1048 end (* Sem8f *)
1049
1050 module TestAll = struct
1051   print_endline "\nTesting Sem1a";;
1052   module T1a = Test(Sem1a);;
1053   print_endline "\nTesting Sem1b";;
1054   module T1b = Test(Sem1b);;
1055   print_endline "\nTesting Sem3a";;
1056   module T3a = Test(Sem3a);;
1057   print_endline "\nTesting Sem3c";;
1058   module T3c = Test(Sem3c);;
1059   print_endline "\nTesting Sem4a";;
1060   module T4a = Test(Sem4a);;
1061   print_endline "\nTesting Sem4c";;
1062   module T4c = Test(Sem4c);;
1063   print_endline "\nTesting Sem7c";;
1064   module T7c = Test(Sem7c);;
1065   print_endline "\nTesting Sem7f";;
1066   module T7f = Test(Sem7f);;
1067   print_endline "\nTesting Sem8c";;
1068   module T8c = Test(Sem8c);;
1069   print_endline "\nTesting Sem8f";;
1070   module T8f = Test(Sem8f);;
1071   print_newline ()
1072 end
1073
1074 (*
1075     One can't test the broken vase case by comparing the _truth_ of any sentences.
1076     The difference is in whether the sentences have meanings that are "supported by"
1077     the same informtation states. Compare in our model:
1078       (i) Someone kissed me. She might have stayed.
1079     and:
1080       (ii) Someone who might have stayed kissed me.
1081     Recall that in our model Ann leaves in every world, but Carol stays in some (non-actual)
1082     world. If my background information settles that I was kissed by either Ann or Carol,
1083     then I'm in a position to assert (i), since after the first clause it's left open
1084     that the referent be either woman. But it doesn't put me in a position to assert (ii),
1085     since that implies I was kissed by Carol. So far as truth-value goes,
1086     if Carol kissed me both sentences are true, and if Ann did then both sentences are false.
1087 *)
1088