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 sentence1 lex (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 sentence2 lex (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 sentence2 lex (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 (t : 'a tree) (f : 'a -> 'b reader) : '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 l f) (fun l' -> reader_bind (tree_monadize r f) (fun r' -> reader_unit (Node (l', r'))));; ... and so on for different monads? Well, notice that `tree\_monadizer` takes arguments whose types resemble that of a monadic `bind` function. Here's a schematic bind function compared with `tree\_monadizer`: bind (u:'a Monad) (f: 'a -> 'b Monad): 'b Monad tree\_monadizer (u:'a Tree) (f: 'a -> 'b Monad): 'b Tree Monad Comparing these types makes it clear that `tree\_monadizer` provides a way to distribute an arbitrary monad M across the leaves of any tree to form a new tree inside an M box. The more general 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]].