**Quantification and default quantifier scope construal**.
-We saw in the copy-string example and in the same-fringe example that
-local properties of a tree (whether a character is `S` or not, which
+We saw in the copy-string example ("abSd") and in the same-fringe example that
+local properties of a structure (whether a character is `'S'` or not, which
integer occurs at some leaf position) can control global properties of
the computation (whether the preceeding string is copied or not,
whether the computation halts or proceeds). Local control of
| "someone" -> Node (Leaf "exists y", k "y")
| _ -> k s;;
- let sentence1 = Node (Leaf "John",
+Then we can crudely approximate quantification as follows:
+
+ # 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
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);;
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
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.
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.
+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]].
-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]].