-let lex (s:string) k = match s with - | "everyone" -> Node (Leaf "forall x", k "x") - | "someone" -> Node (Leaf "exists y", k "y") - | _ -> k s;; - -let sentence1 = Node (Leaf "John", - Node (Node (Leaf "saw", - Leaf "everyone"), - Leaf "yesterday"));; -+ let lex (s:string) k = match s with + | "everyone" -> Node (Leaf "forall x", k "x") + | "someone" -> Node (Leaf "exists y", k "y") + | _ -> k s;; Then we can crudely approximate quantification as follows: -

-# tree_monadize lex sentence1 (fun x -> x);; -- : string tree = -Node - (Leaf "forall x", - Node (Leaf "John", Node (Node (Leaf "saw", Leaf "x"), Leaf "yesterday"))) -+ # let sentence1 = Node (Leaf "John", + Node (Node (Leaf "saw", + Leaf "everyone"), + Leaf "yesterday"));; + + # tree_monadize lex sentence1 (fun x -> x);; + - : string tree = + Node + (Leaf "forall x", + Node (Leaf "John", Node (Node (Leaf "saw", Leaf "x"), Leaf "yesterday"))) In order to see the effects of evaluation order, observe what happens when we combine two quantifiers in the same sentence: -

-# let sentence2 = Node (Leaf "everyone", Node (Leaf "saw", Leaf "someone"));; -# tree_monadize lex sentence2 (fun x -> x);; -- : string tree = -Node - (Leaf "forall x", - Node (Leaf "exists y", Node (Leaf "x", Node (Leaf "saw", Leaf "y")))) -+ # let sentence2 = Node (Leaf "everyone", Node (Leaf "saw", Leaf "someone"));; + # tree_monadize lex sentence2 (fun x -> x);; + - : string tree = + Node + (Leaf "forall x", + Node (Leaf "exists y", Node (Leaf "x", Node (Leaf "saw", Leaf "y")))) The universal takes scope over the existential. If, however, we -replace the usual tree_monadizer with tree_monadizer_rev, we get +replace the usual `tree_monadizer` with `tree_monadizer_rev`, we get inverse scope: -

-# tree_monadize_rev lex sentence2 (fun x -> x);; -- : string tree = -Node - (Leaf "exists y", - Node (Leaf "forall x", Node (Leaf "x", Node (Leaf "saw", Leaf "y")))) -+ # tree_monadize_rev lex sentence2 (fun x -> x);; + - : string tree = + Node + (Leaf "exists y", + Node (Leaf "forall x", Node (Leaf "x", Node (Leaf "saw", Leaf "y")))) There are many crucially important details about quantification that -are being simplified here, and the continuation treatment here is not +are being simplified here, and the continuation treatment used here is not scalable for a number of reasons. Nevertheless, it will serve to give an idea of how continuations can provide insight into the behavior of -quantifiers. +quantifiers. -The Binary Tree monad ---------------------- +The Tree monad +============== -Of course, by now you may have realized that we have discovered a new -monad, the Binary Tree monad. Just as mere lists are in fact a monad, +Of course, by now you may have realized that we are working with a new +monad, the binary, leaf-labeled Tree monad. Just as mere lists are in fact a monad, so are trees. Here is the type constructor, unit, and bind: type 'a tree = Leaf of 'a | Node of ('a tree) * ('a tree);; @@ -484,20 +478,20 @@ To check the other two laws, we need to make the following observation: it is easy to prove based on `tree_bind` by a simple induction on the structure of the first argument that the tree resulting from `bind u f` is a tree with the same strucure as `u`, -except that each leaf `a` has been replaced with `f a`: +except that each leaf `a` has been replaced with the tree returned by `f a`: . . __|__ __|__ - | | | | + | | /\ | a1 . f a1 . _|__ __|__ - | | | | + | | | /\ . a5 . f a5 bind _|__ f = __|__ - | | | | + | | | /\ . a4 . f a4 __|__ __|___ - | | | | + | | /\ /\ a2 a3 f a2 f a3 Given this equivalence, the right identity law @@ -535,7 +529,7 @@ Now when we bind this tree to `g`, we get At this point, it should be easy to convince yourself that using the recipe on the right hand side of the associative law will -built the exact same final tree. +build the exact same final tree. So binary trees are a monad. @@ -548,25 +542,5 @@ that is intended to represent non-deterministic computations as a tree. What's this have to do with tree\_monadize? -------------------------------------------- -So we've defined a Tree monad: - - type 'a tree = Leaf of 'a | Node of ('a tree) * ('a tree);; - 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);; - -What's this have to do with the `tree_monadize` functions we defined earlier? - - let rec tree_monadize (f : 'a -> 'b reader) (t : 'a tree) : 'b tree reader = - match t with - | Leaf a -> reader_bind (f a) (fun b -> reader_unit (Leaf b)) - | Node (l, r) -> reader_bind (tree_monadize f l) (fun l' -> - reader_bind (tree_monadize f r) (fun r' -> - reader_unit (Node (l', r'))));; - -... and so on for different monads? - -The answer is that each of those `tree_monadize` functions is adding a Tree monad *layer* to a pre-existing Reader (and so on) monad. We discuss that further here: [[Monad Transformers]]. +Our different implementations of `tree_monadize` above were different *layerings* of the Tree monad with other monads (Reader, State, List, and Continuation). We'll explore that further here: [[Monad Transformers]].