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"));;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")))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"))))The universal takes scope over the existential. If, however, we 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"))))There are many crucially important details about quantification that are being simplified here, and the continuation treatment 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. The Binary 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, so are trees. Here is the type constructor, unit, and bind: 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);; For once, let's check the Monad laws. The left identity law is easy: Left identity: bind (unit a) f = bind (Leaf a) f = f a 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`: . . __|__ __|__ | | | | a1 . f a1 . _|__ __|__ | | | | . a5 . f a5 bind _|__ f = __|__ | | | | . a4 . f a4 __|__ __|___ | | | | a2 a3 f a2 f a3 Given this equivalence, the right identity law Right identity: bind u unit = u falls out once we realize that bind (Leaf a) unit = unit a = Leaf a As for the associative law, Associativity: bind (bind u f) g = bind u (\a. bind (f a) g) we'll give an example that will show how an inductive proof would proceed. Let `f a = Node (Leaf a, Leaf a)`. Then . ____|____ . . | | bind __|__ f = __|_ = . . | | | | __|__ __|__ a1 a2 f a1 f a2 | | | | a1 a1 a1 a1 Now when we bind this tree to `g`, we get . _____|______ | | . . __|__ __|__ | | | | g a1 g a1 g a1 g a1 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. So binary trees are a monad. Haskell combines this monad with the Option monad to provide a monad called a [SearchTree](http://hackage.haskell.org/packages/archive/tree-monad/0.2.1/doc/html/src/Control-Monad-SearchTree.html#SearchTree) 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]].