type env = int -> int;;
type 'a reader = env -> 'a;;
-let unit_reader a : 'a reader = fun e -> a;;
-let bind_reader (u : 'a reader) (f : 'a -> 'b reader) : 'b reader =
+let reader_unit a : 'a reader = fun e -> a;;
+let reader_bind (u : 'a reader) (f : 'a -> 'b reader) : 'b reader =
fun e -> f (u e) e;;
(* Now we supply the Reader monad as a parameter to Tree_monadizer.
* the monadize function specialized to the Reader monad *)
module TreeReader = Tree_monadizer(struct
type 'a m = 'a reader
- let unit = unit_reader
- let bind = bind_reader
+ let unit = reader_unit
+ let bind = reader_bind
end);;
type store = int;;
type 'a state = store -> 'a * store;;
-let unit_state a : 'a state = fun s -> (a, s);;
-let bind_state (u : 'a state) (f : 'a -> 'b state) : 'b state =
+let state_unit a : 'a state = fun s -> (a, s);;
+let state_bind (u : 'a state) (f : 'a -> 'b state) : 'b state =
fun s -> (let (a, s') = u s in (f a) s');;
(* Make a TreeState module containing monadize specialized to the State monad *)
module TreeState = Tree_monadizer(struct
type 'a m = 'a state
- let unit = unit_state
- let bind = bind_state
+ let unit = state_unit
+ let bind = state_bind
end);;
-let unit_list a = [a];;
-let bind_list (u: 'a list) (f : 'a -> 'b list) : 'b list =
+let list_unit a = [a];;
+let list_bind (u: 'a list) (f : 'a -> 'b list) : 'b list =
List.concat(List.map f u);;
(* Make a TreeList module containing monadize specialized to the List monad *)
module TreeList = Tree_monadizer(struct
type 'a m = 'a list
- let unit = unit_list
- let bind = bind_list
+ let unit = list_unit
+ let bind = list_bind
end);;
end;;
type ('a,'r) cont = ('a -> 'r) -> 'r;;
-let unit_cont a : ('a,'r) cont = fun k -> k a;;
-let bind_cont (u: ('a,'r) cont) (f: 'a -> ('b,'r) cont) : ('b,'r) cont =
+let cont_unit a : ('a,'r) cont = fun k -> k a;;
+let cont_bind (u: ('a,'r) cont) (f: 'a -> ('b,'r) cont) : ('b,'r) cont =
fun k -> u (fun a -> f a k);;
(* Make a TreeCont module containing monadize specialized to the Cont monad *)
module TreeCont = Tree_monadizer2(struct
type ('a,'r) m = ('a,'r) cont
- let unit = unit_cont
- let bind = bind_cont
+ let unit = cont_unit
+ let bind = cont_bind
end);;
(* do nothing *)
let initial_continuation = fun t -> t in
-TreeCont.monadize unit_cont t1 initial_continuation;;
+TreeCont.monadize cont_unit t1 initial_continuation;;
(* convert tree to list of leaves *)
let initial_continuation = fun t -> [] in
TreeCont.monadize (fun a k -> 1 + k a) t1 initial_continuation;;
+
+
+(* Tree monad *)
+
+(* type 'a tree defined above *)
+let tree_unit (a: 'a) : 'a tree = Leaf a;;
+let rec tree_bind (u : 'a tree) (f : 'a -> 'b tree) : 'b tree =
+ match u with
+ | Leaf a -> f a
+ | Node (l, r) -> Node (tree_bind l f, tree_bind r f);;
+
+type 'a, treeTC_reader =
+ 'a tree reader;;
+
+ let unit (a: 'a) : 'a tree reader =
+ M.unit (Leaf a);;
+
+ let rec bind (u : ('a, M) tree) (f : 'a -> ('b, M) tree) : ('b, M) tree =
+ match u with
+ | Leaf a -> M.bind (f a) (fun b -> M.unit (Leaf b))
+ | Node (l, r) -> M.bind (bind l f) (fun l' ->
+ M.bind (bind r f) (fun r' ->
+ M.unit (Node (l', r'));;
Since `dpm`s 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 unit_dpm (value : 'a) : 'a dpm = fun (r, h) -> (value, r, h);;
+ let dpm_unit (value : 'a) : 'a dpm = fun (r, h) -> (value, r, h);;
- let bind_dpm (u : 'a dpm) (f : 'a -> 'b dpm) : 'b dpm =
+ 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
As I said, for simplicity, we'll represent sets using lists:
type 'a set = 'a list;;
- let empty_set : 'a set = [];;
- let unit_set (value: 'a) : 'a set = [value];;
- let bind_set (u: 'a set) (f: 'a -> 'b set) : 'b set =
+ let set_empty : 'a set = [];;
+ let set_unit (value: 'a) : 'a set = [value];;
+ let set_bind (u: 'a set) (f: 'a -> 'b set) : 'b set =
List.concat (List.map f u);;
then let obj = List.nth h (r 'x') in q obj
else false
in (truth_value', r, h)
- in bind_set u (fun one_dpm -> unit_set (bind_dpm one_dpm eliminator))
+ in set_bind u (fun one_dpm -> set_unit (dpm_bind one_dpm eliminator))
- The first seven lines here just perfom the operation we described: return a `bool dpm` computation that only yields `true` when its input `(r, h)` associates variable `x` with the right sort of entity. The last line performs the `bind_set` operation. This works by taking each `dpm` in the set and returning a `unit_set` of a filtered `dpm`. The definition of `bind_set` takes care of collecting together all of the `unit_set`s that result for each different set element we started with.
+ The first seven lines here just perfom the operation we described: return a `bool dpm` computation that only yields `true` when its input `(r, h)` associates variable `x` with the right sort of entity. The last line performs the `set_bind` operation. This works by taking each `dpm` in the set and returning a `set_unit` of a filtered `dpm`. The definition of `set_bind` takes care of collecting together all of the `set_unit`s that result for each different set element we started with.
We can call the `(fun one_dpm -> ...)` part \[[Qx]] and then updating `u` with \[[Qx]] will be:
- bind_set u \[[Qx]]
+ set_bind u \[[Qx]]
or as it's written using Haskell's infix notation for bind:
* Now what do we do with predicates? As before, we suppose we have a function `q` that maps entities to `bool`s. We want to turn it into a function that maps `entity dpm`s to `bool dpm`s. Eventually we'll need to operate not just on single `dpm`s but on sets of them, but first things first. We'll begin by lifting `q` into a function that takes `entity dpm`s as arguments and returns `bool dpm`s:
- fun entity_dpm -> bind_dpm entity_dpm (fun e -> unit_dpm (q e))
+ fun entity_dpm -> dpm_bind entity_dpm (fun e -> dpm_unit (q e))
- Now we have to transform this into a function that again takes single `entity dpm`s as arguments, but now returns a `bool dpm set`. This is easily done with `unit_set`:
+ Now we have to transform this into a function that again takes single `entity dpm`s as arguments, but now returns a `bool dpm set`. This is easily done with `set_unit`:
- fun entity_dpm -> unit_set (bind_dpm entity_dpm (fun e -> unit_dpm (q e)))
+ fun entity_dpm -> set_unit (dpm_bind entity_dpm (fun e -> dpm_unit (q e)))
Finally, we realize that we're going to have a set of `bool dpm`s to start with, and we need to monadically bind \[[Qx]] to them. We don't want any of the monadic values in the set that wrap `false` to become `true`; instead, we want to apply a filter that checks whether values that formerly wrapped `true` should still continue to do so.
let eliminator : bool -> bool dpm =
fun truth_value ->
if truth_value = false
- then unit_dpm false
- else bind_dpm entity_dpm (fun e -> unit_dpm (q e))
- in fun one_dpm -> unit_set (bind_dpm one_dpm eliminator)
+ then dpm_unit false
+ else dpm_bind entity_dpm (fun e -> dpm_unit (q e))
+ in fun one_dpm -> set_unit (dpm_bind one_dpm eliminator)
Applied to an `entity_dpm`, that yields a function that we can bind to a `bool dpm set` and that will transform the doubly-wrapped `bool` into a new `bool dpm set`.
in let entity_dpm = getx
in let eliminator = fun truth_value ->
if truth_value = false
- then unit_dpm false
- else bind_dpm entity_dpm (fun e -> unit_dpm (q e))
- in fun one_dpm -> unit_set (bind_dpm one_dpm eliminator)
+ then dpm_unit false
+ else dpm_bind entity_dpm (fun e -> dpm_unit (q e))
+ in fun one_dpm -> set_unit (dpm_bind one_dpm eliminator)
<!--
or, simplifying:
in (obj, r, h)
in let eliminator = fun truth_value ->
if truth_value
- then bind_dpm getx (fun e -> unit_dpm (q e))
- else unit_dpm false
- in fun one_dpm -> unit_set (bind_dpm one_dpm eliminator)
+ then dpm_bind getx (fun e -> dpm_unit (q e))
+ else dpm_unit false
+ in fun one_dpm -> set_unit (dpm_bind one_dpm eliminator)
-->
- If we simplify and unpack the definition of `bind_dpm`, that's equivalent to:
+ If we simplify and unpack the definition of `dpm_bind`, that's equivalent to:
let getx = fun (r, h) ->
let obj = List.nth h (r 'x')
if truth_value
then (fun (r, h) ->
let (a, r', h') = getx (r, h)
- in let u' = (fun e -> unit_dpm (q e)) a
+ in let u' = (fun e -> dpm_unit (q e)) a
in u' (r', h')
- ) else unit_dpm false
- in fun one_dpm -> unit_set (bind_dpm one_dpm eliminator)
+ ) else dpm_unit false
+ in fun one_dpm -> set_unit (dpm_bind one_dpm eliminator)
which can be further simplified to:
then (fun (r, h) ->
let obj = List.nth h (r 'x')
let (a, r', h') = (obj, r, h)
- in let u' = (fun e -> unit_dpm (q e)) a
+ in let u' = (fun e -> dpm_unit (q e)) a
in u' (r', h')
- ) else unit_dpm false
- in fun one_dpm -> unit_set (bind_dpm one_dpm eliminator)
+ ) else dpm_unit false
+ in fun one_dpm -> set_unit (dpm_bind one_dpm eliminator)
let eliminator = fun truth_value ->
if truth_value
then (fun (r, h) ->
let obj = List.nth h (r 'x')
- in let u' = unit_dpm (q obj)
+ in let u' = dpm_unit (q obj)
in u' (r, h)
- ) else unit_dpm false
- in fun one_dpm -> unit_set (bind_dpm one_dpm eliminator)
+ ) else dpm_unit false
+ in fun one_dpm -> set_unit (dpm_bind one_dpm eliminator)
-->
let eliminator = fun truth_value ->
then (fun (r, h) ->
let obj = List.nth h (r 'x')
in (q obj, r, h)
- ) else unit_dpm false
- in fun one_dpm -> unit_set (bind_dpm one_dpm eliminator)
+ ) else dpm_unit false
+ in fun one_dpm -> set_unit (dpm_bind one_dpm eliminator)
This is a function that takes a `bool dpm` as input and returns a `bool dpm set` as output.
then let obj = List.nth h (r 'x') in q obj
else false
in (truth_value', r, h))
- in fun one_dpm -> unit_set (bind_dpm one_dpm eliminator)
+ in fun one_dpm -> set_unit (dpm_bind one_dpm eliminator)
Can you persuade yourself that these are equivalent?)
* Reviewing: now we've determined how to define \[[Q]] and \[[x]] such that \[[Qx]] can be the result of applying the function \[[Q]] to the `entity dpm` \[[x]]. And \[[Qx]] in turn is now a function that takes a `bool dpm` as input and returns a `bool dpm set` as output. We monadically bind this operaration to whatever `bool dpm set` we already have on hand:
- bind_set u \[[Qx]]
+ set_bind u \[[Qx]]
or:
<pre><code>u updated with \[[∃x]] ≡
let extend one_dpm (d : entity) =
- bind_dpm one_dpm (new_peg_and_assign 'x' d)
- in bind_set u (fun one_dpm -> List.map (fun d -> extend one_dpm d) domain)
+ dpm_bind one_dpm (new_peg_and_assign 'x' d)
+ in set_bind u (fun one_dpm -> List.map (fun d -> extend one_dpm d) domain)
</code></pre>
where `new_peg_and_assign` is the operation we defined in [hint 3](/hints/assignment_7_hint_3):
or, being explicit about which "bind" operation we're representing here with `>>=`, that is:
- <pre><code>bind_set (bind_set u \[[∃x]]) \[[Px]]
+ <pre><code>set_bind (set_bind u \[[∃x]]) \[[Px]]
</code></pre>
* Let's compare this to what \[[∃xPx]] would look like on a non-dynamic semantics, for example, where we use a simple Reader monad to implement variable binding. Reminding ourselves, we'd be working in a framework like this. (Here we implement environments or assignments as functions from variables to entities, instead of as lists of pairs of variables and entities. An assignment `r` here is what `fun c -> List.assoc c r` would have been in [week7](
type assignment = char -> entity;;
type 'a reader = assignment -> 'a;;
- let unit_reader (value : 'a) : 'a reader = fun r -> value;;
+ let reader_unit (value : 'a) : 'a reader = fun r -> value;;
- let bind_reader (u : 'a reader) (f : 'a -> 'b reader) : 'b reader =
+ let reader_bind (u : 'a reader) (f : 'a -> 'b reader) : 'b reader =
fun r ->
let a = u r
in let u' = f a
fun entity_reader ->
fun r ->
let obj = entity_reader r
- in unit_reader (predicate obj)
+ in reader_unit (predicate obj)
The meaning of \[[Qx]] would then be:
\[[Qx]] ≡ \[[Q]] \[[x]] ≡
fun r ->
let obj = getx r
- in unit_reader (q obj)
+ in reader_unit (q obj)
</code></pre>
Recall also how we defined \[[lambda x]], or as [we called it before](/reader_monad_for_variable_binding), \\[[who(x)]]:
fun (lifted_predicate : lifted_unary) ->
fun r -> exists (fun (obj : entity) ->
- lifted_predicate (unit_reader obj) r)
+ lifted_predicate (reader_unit obj) r)
That would be the meaning of \[[∃]], which we'd use like this:
in clause r'
in let lifted_exists =
fun lifted_predicate ->
- fun r -> exists (fun obj -> lifted_predicate (unit_reader obj) r)
+ fun r -> exists (fun obj -> lifted_predicate (reader_unit obj) r)
in fun bool_reader -> lifted_exists (shift 'x' bool_reader)
which we can simplify to:
in clause r'
in let lifted_exists =
fun lifted_predicate ->
- fun r -> exists (fun obj -> lifted_predicate (unit_reader obj) r)
+ fun r -> exists (fun obj -> lifted_predicate (reader_unit obj) r)
in fun bool_reader -> lifted_exists (shifted bool_reader)
fun bool_reader ->
let new_value = entity_reader r
in let r' = fun var -> if var = 'x' then new_value else r var
in bool_reader r'
- in fun r -> exists (fun obj -> shifted' (unit_reader obj) r)
+ in fun r -> exists (fun obj -> shifted' (reader_unit obj) r)
fun bool_reader ->
let shifted'' r obj =
- let new_value = (unit_reader obj) r
+ let new_value = (reader_unit obj) r
in let r' = fun var -> if var = 'x' then new_value else r var
in bool_reader r'
in fun r -> exists (fun obj -> shifted'' r obj)
let new_dpm = fun (r, h) ->
(* if one_dpm isn't already false at (r, h),
we want to check its behavior when updated with phi
- bind_set (unit_set one_dpm) phi === phi one_dpm; do you remember why? *)
+ set_bind (set_unit one_dpm) phi === phi one_dpm; do you remember why? *)
let (truth_value, r', h') = one_dpm (r, h)
in let truth_value' = truth_value && (truths (phi one_dpm) (r, h) = [])
(* new_dpm must return a (bool, r, h) *)
in (truth_value', r', h')
- in unit_set new_dpm;;
+ in set_unit new_dpm;;
**Thanks to Simon Charlow** for catching a subtle error in previous versions of this function. Fixed 1 Dec.
* Representing \[[and φ ψ]] is simple:
let and_op (phi : clause) (psi : clause) : clause =
- fun one_dpm -> bind_set (phi one_dpm) psi;;
+ fun one_dpm -> set_bind (phi one_dpm) psi;;
(* now u >>= and_op phi psi === u >>= phi >>= psi; do you remember why? *)
(These probably still manifest the bug Simon spotted.)
let or_op (phi : clause) (psi : clause) =
- fun one_dpm -> unit_set (
+ fun one_dpm -> set_unit (
fun (r, h) ->
let truth_value' = (
truths (phi one_dpm) (r, h) <> [] ||
- truths (bind_set (negate_op phi one_dpm) psi) (r, h) <> []
+ truths (set_bind (negate_op phi one_dpm) psi) (r, h) <> []
) in (truth_value', r, h))
let if_op (phi : clause) (psi : clause) : clause =
- fun one_dpm -> unit_set (
+ fun one_dpm -> set_unit (
fun (r, h) ->
let truth_value' = List.for_all (fun one_dpm ->
let (truth_value, _, _) = one_dpm (r, h)
type assignment = char -> int;;
type store = entity list;;
type 'a dpm = assignment * store -> 'a * assignment * store;;
- let unit_dpm (x : 'a) : 'a dpm = fun (r, h) -> (x, r, h);;
- let bind_dpm (u: 'a dpm) (f : 'a -> 'b dpm) : 'b dpm =
+ let dpm_unit (x : 'a) : 'a dpm = fun (r, h) -> (x, 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')
type 'a set = 'a list;;
- let empty_set : 'a set = [];;
- let unit_set (x : 'a) : 'a set = [x];;
- let bind_set (u : 'a set) (f : 'a -> 'b set) : 'b set =
+ let set_empty : 'a set = [];;
+ let set_unit (x : 'a) : 'a set = [x];;
+ let set_bind (u : 'a set) (f : 'a -> 'b set) : 'b set =
List.concat (List.map f u);;
type clause = bool dpm -> bool dpm set;;
fun entity_dpm ->
let eliminator = fun truth_value ->
if truth_value = false
- then unit_dpm false
- else bind_dpm entity_dpm (fun e -> unit_dpm (f e))
- in fun one_dpm -> unit_set (bind_dpm one_dpm eliminator);;
+ then dpm_unit false
+ else dpm_bind entity_dpm (fun e -> dpm_unit (f e))
+ in fun one_dpm -> set_unit (dpm_bind one_dpm eliminator);;
(* doing the same thing for binary predicates *)
let lift_predicate2 (f : entity -> entity -> bool) : entity dpm -> entity dpm -> clause =
fun entity1_dpm entity2_dpm ->
let eliminator = fun truth_value ->
if truth_value = false
- then unit_dpm false
- else bind_dpm entity1_dpm (fun e1 -> bind_dpm entity2_dpm (fun e2 -> unit_dpm (f e1 e2)))
- in fun one_dpm -> unit_set (bind_dpm one_dpm eliminator);;
+ then dpm_unit false
+ else dpm_bind entity1_dpm (fun e1 -> dpm_bind entity2_dpm (fun e2 -> dpm_unit (f e1 e2)))
+ in fun one_dpm -> set_unit (dpm_bind one_dpm eliminator);;
let new_peg_and_assign (var_to_bind : char) (d : entity) : bool -> bool dpm =
fun truth_value ->
(* from hint 5 *)
let exists var : clause =
let extend one_dpm (d : entity) =
- bind_dpm one_dpm (new_peg_and_assign var d)
+ dpm_bind one_dpm (new_peg_and_assign var d)
in fun one_dpm -> List.map (fun d -> extend one_dpm d) domain
(* include negate_op, and_op, or_op, and if_op as above *)
* More:
(* some handy utilities *)
- let (>>=) = bind_set;;
+ let (>>=) = set_bind;;
let getx = get 'x';;
let gety = get 'y';;
let initial_set = [fun (r,h) -> (true,r,h)];;
let rec bind (u : 'a tree) (f : 'a -> 'b tree) : 'b tree =
match u with
- | Leaf a -> (fun b -> Leaf b) (f a)
+ | Leaf a -> (fun b -> b) (f a) (* see below *)
| Node (l, r) -> (fun l' r' -> Node (l', r')) (bind l f) (bind r f);;
(* monadic operations for the TreeT monadic transformer *)
(* alternatively, an env could be implemented as type char -> int *)
type 'a reader = env -> 'a;;
- let unit_reader (value : 'a) : 'a reader =
+ let reader_unit (value : 'a) : 'a reader =
fun e -> value;;
- let bind_reader (u : 'a reader) (f : 'a -> 'b reader) : 'b reader =
+ let reader_bind (u : 'a reader) (f : 'a -> 'b reader) : 'b reader =
fun e -> let a = u e
in let u' = f a
in u' e;;
(* this corresponds to having only a single mutable variable *)
type 'a state = store -> ('a, store);;
- let unit_state (value : 'a) : 'a state =
+ let state_unit (value : 'a) : 'a state =
fun s -> (value, s);;
- let bind_state (u : 'a state) (f : 'a -> 'b state) : 'b state =
+ let state_bind (u : 'a state) (f : 'a -> 'b state) : 'b state =
fun s -> let (a, s') = u s
in let u' = f a
in u' s';;