• GS&V's semantics involves elements from several different monads we've been looking at. First, they're working with (epistemic) modalities, so there are worlds playing a role like they did in Reader Monad for Intensionality. But we're going to ignore the modal element for this exercise. There's also variable binding, which calls for another Reader monad. Next, there is a notion of a store, which some operations add new reference cells to. We implement this with a State monad (and so too, in effect, do they---though they don't conceive of what they're doing in those terms). So we'll be working with a combination of both a Reader monad for the variable binding and a State monad to keep track of the new "pegs" or reference cells.

    There are systematic ways to layer different monads together. If you want to read about these, a keyword is "monad transformers." Ken Shan discusses them in his paper that we recommended earlier.

    However, since we haven't studied these, we will just combine the Reader monad and the State monad in an ad hoc way. The easiest way to do this is to think of the assignment function and the store of reference cells as a combined state, which gets threaded through the computations in the same way that simple states did in your earlier homeworks.

    We'll call these "discourse possibility monads," or dpms, and type them as follows:

    type entity = Bob | Carol | Ted | Alice;;
    let domain = [Bob; Carol; Ted; Alice];;
    type assignment = char -> int;; (* variables are bound to indexes into the store *)
    type store = entity list;;
    type 'a dpm = 
        (* we ignore worlds *)
        assignment * store -> 'a * assignment * store

    Although we're leaving worlds out of the picture, each of these monadic values still represents a different discourse possibility: which entities might be being talked about, using which variables.

    Since dpms are to be a monad, we have to define a unit and a bind. These are just modeled on the unit and bind for the State monad:

    let dpm_unit (value : 'a) : 'a dpm = fun (r, h) -> (value, r, h);;
    let dpm_bind (u : 'a dpm) (f : 'a -> 'b dpm) : 'b dpm =
        fun (r, h) ->
            let (a, r', h') = u (r, h)
            in let u' = f a
            in u' (r', h')
  • A possibility for GS&V is a triple of an assignment function r, a store h, and a world w. We're dropping worlds so we'll call pairs (r, h) discourse possibilities. dpms are monads that represent computations that may mutate---or in GS&V's terminology "extend"---discourse possibilities. An 'a dpm is a function that takes a starting (r, h) and returns an 'a and a possibly mutated r' and h'.

  • Is that enough? If not, here are some more hints. But try to get as far as you can on your own.