In fact you've already seen this several times this semester---recall how in our implementation of pairs in the untyped lambda-calculus, the handler who wanted to use the pair's components had *in the first place to be supplied to the pair as an argument*. So the exotica from the end of the seminar was already on the scene in some of our earliest steps. Recall also what we did with v2 and v5 lists. Version 5 lists were the ones that let us abort a fold early:
go back and re-read the material on "Aborting a Search Through a List" in [[Week4]].
-This inversion of control should also remind you of Montague's treatment of subject terms in ["The Proper Treatment of Quantification in Ordinary English"](http://www.blackwellpublishing.com/content/BPL_Images/Content_store/Sample_chapter/0631215417%5CPortner.pdf) (PTQ).
+This inversion of control should also remind you of Montague's treatment of determiner phrases in ["The Proper Treatment of Quantification in Ordinary English"](http://www.blackwellpublishing.com/content/BPL_Images/Content_store/Sample_chapter/0631215417%5CPortner.pdf) (PTQ).
A naive semantics for atomic sentences will say the subject term is of type `e`, and the predicate of type `e -> t`, and that the subject provides an argument to the function expressed by the predicate.
-Monatague proposed we instead take subject terms to be of type `(e -> t) -> t`, and that now it'd be the predicate (still of type `e -> t`) that provides an argument to the function expressed by the subject.
+Monatague proposed we instead take the subject term to be of type `(e -> t) -> t`, and that now it'd be the predicate (still of type `e -> t`) that provides an argument to the function expressed by the subject.
If all the subject did then was supply an `e` to the `e -> t` it receives as an argument, we wouldn't have gained anything we weren't already able to do. But of course, there are other things the subject can do with the `e -> t` it receives as an argument. For instance, it can check whether anything in the domain satisfies that `e -> t`; or whether most things do; and so on.
This inversion of who is the argument and who is the function receiving the argument is paradigmatic of working with continuations.
-Continuations come in many varieties. There are **undelimited continuations**, expressed in Scheme via `(call/cc (lambda (k) ...))` or the shorthand `(let/cc k ...)`. These capture "the entire rest of the computation." There are also **delimited continuations**, expressed in Scheme via `(reset ... (shift k ...) ...)` or `(prompt ... (control k ...) ...)` or any of several other operations. There are subtle differences between these that we won't be exploring in the seminar. Ken Shan has done amazing work exploring the relations of these operations to each other.
+Continuations come in many varieties. There are **undelimited continuations**, expressed in Scheme via `(call/cc (lambda (k) ...))` or the shorthand `(let/cc k ...)`. (`call/cc` is itself shorthand for `call-with-current-continuation`.) These capture "the entire rest of the computation." There are also **delimited continuations**, expressed in Scheme via `(reset ... (shift k ...) ...)` or `(prompt ... (control k ...) ...)` or any of several other operations. There are subtle differences between those that we won't be exploring in the seminar. Ken Shan has done amazing work exploring the relations of these operations to each other.
When working with continuations, it's easiest in the first place to write them out explicitly, the way that we explicitly wrote out the `snapshot` continuation when we transformed this:
the execution of `tz` above. There will once again be one initial and
four recursive calls to `tc`, and `zipped` will take on the values
`"bSd"`, `"Sd"`, `"d"`, and `""` (and, once again, on the final call,
-the first `match` clause will fire, so the the variable `zipper` will
+the first `match` clause will fire, so the the variable `zipped` will
not be instantiated).
I have not called the functional argument `unzipped`, although that is
The reason the task is well-suited to the list zipper is in part
because the list monad has an intimate connection with continuations.
-The following section explores this connection. We'll return to the
-list task after talking about generalized quantifiers below.
+We'll explore this next.
Rethinking the list monad
-------------------------
-To construct a monad, the key element is to settle on a type
-constructor, and the monad more or less naturally follows from that.
-We'll remind you of some examples of how monads follow from the type
-constructor in a moment. This will involve some review of familiar
+To construct a monad, the key element is to settle on how to implement its type, and
+the monad more or less naturally follows from that.
+We'll remind you of some examples of how monads follow from their types
+in a moment. This will involve some review of familiar
material, but it's worth doing for two reasons: it will set up a
pattern for the new discussion further below, and it will tie together
some previously unconnected elements of the course (more specifically,
version 3 lists and monads).
-For instance, take the **Reader Monad**. Once we decide that the type
-constructor is
+For instance, take the **Reader Monad**. Once we decide to define its type as:
type 'a reader = env -> 'a
Since the type of the `bind` operator is required to be
- r_bind : ('a reader) -> ('a -> 'b reader) -> ('b reader)
+ r_bind : 'a reader -> ('a -> 'b reader) -> 'b reader
We can reason our way to the traditional reader `bind` function as
follows. We start by declaring the types determined by the definition
of a bind operation:
- let r_bind (u : 'a reader) (f : 'a -> 'b reader) : ('b reader) = ...
+ let r_bind (u : 'a reader) (f : 'a -> 'b reader) : 'b reader = ...
Now we have to open up the `u` box and get out the `'a` object in order to
feed it to `f`. Since `u` is a function from environments to
This types to `env -> 'b reader`, but we want to end up with `env ->
'b`. Once again, the easiest way to turn a `'b reader` into a `'b` is to apply it to an environment. So we end up as follows:
- r_bind (u : 'a reader) (f : 'a -> 'b reader) : ('b reader) = f (u e) e
+ r_bind (u : 'a reader) (f : 'a -> 'b reader) : 'b reader =
+ fun e -> f (u e) e
And we're done. This gives us a bind function of the right type. We can then check whether, in combination with the unit function we chose, it satisfies the monad laws, and behaves in the way we intend. And it does.
Our other familiar monad is the **List Monad**, which we were told
looks like this:
- type 'a list = ['a];;
+ (* type 'a list = ['a];; *)
l_unit (a : 'a) = [a];;
l_bind u f = List.concat (List.map f u);;
will provide a connection with continuations.
Recall that `List.map` takes a function and a list and returns the
-result to applying the function to the elements of the list:
+result of applying the function to the elements of the list:
List.map (fun i -> [i; i+1]) [1; 2] ~~> [[1; 2]; [2; 3]]
-and `List.concat` takes a list of lists and erases the embedded list
+and `List.concat` takes a list of lists and erases one level of embedded list
boundaries:
List.concat [[1; 2]; [2; 3]] ~~> [1; 2; 2; 3]
type `'a`, and we want to make use of each of them (rather than
arbitrarily throwing some of them away). The only
thing we know for sure we can do with an object of type `'a` is apply
-the function of type `'a -> 'a list` to them. Once we've done so, we
+the function of type `'a -> 'b list` to them. Once we've done so, we
have a collection of lists, one for each of the `'a`'s. One
possibility is that we could gather them all up in a list, so that
`bind' [1; 2] (fun i -> [i; i]) ~~> [[1; 1]; [2; 2]]`. But that restricts
the object returned by the second argument of `bind` to always be of
-type `'b list list`. We can eliminate that restriction by flattening
+type `('something list) list`. We can eliminate that restriction by flattening
the list of lists into a single list: this is
just `List.concat` applied to the output of `List.map`. So there is some logic to the
choice of unit and bind for the list monad.
can stop. These types should remind you of the simply-typed lambda calculus
types for Church numerals (`(o -> o) -> o -> o`) with one extra type
thrown in, the type of the element at the head of the list
-(in this case, an int).
+(in this case, an `int`).
So here's our type constructor for our hand-rolled lists:
fun k z -> u (fun a b -> f a k b) z
-Now let's think about what this does. It's a wrapper around `u`. In order to behave as the list which is the result of mapping `f` over each element of `u`, and then joining (`concat`ing) the results, this wrapper would have to accept arguments `k` and `z` and fold them in just the same way that the list which is the result of mapping `f` and then joining the results would fold them. Will it?
+Now let's think about what this does. It's a wrapper around `u`. In order to behave as the list `v` which is the result of mapping `f` over each element of `u`, and then joining (`concat`ing) the results, this wrapper would have to accept arguments `k` and `z` and fold them in just the same way that `v` would.
+Will it?
-Suppose we have a list' whose contents are `[1; 2; 4; 8]`---that is, our list' will be `fun f z -> f 1 (f 2 (f 4 (f 8 z)))`. We call that list' `u`. Suppose we also have a function `f` that for each `int` we give it, gives back a list of the divisors of that `int` that are greater than 1. Intuitively, then, binding `u` to `f` should give us:
+Suppose we have a list' whose contents are `[1; 2; 4; 8]`---that is, our list' `u` will be `fun f z -> f 1 (f 2 (f 4 (f 8 z)))`. Suppose we also have a function `f` that for each `int` we give it, gives back a list of the divisors of that `int` that are greater than 1. Intuitively, then, binding `u` to `f` should give us:
+ v =
List.concat (List.map f u) =
List.concat [[]; [2]; [2; 4]; [2; 4; 8]] =
[2; 2; 4; 2; 4; 8]
-Or rather, it should give us a list' version of that, which takes a function `k` and value `z` as arguments, and returns the right fold of `k` and `z` over those elements. What does our formula
+Or rather, it should give us a list' version of that, which takes a function `k` and value `z` as arguments, and returns the right fold of `k` and `z` over those elements. Does our formula
fun k z -> u (fun a b -> f a k b) z
-do? Well, for each element `a` in `u`, it applies `f` to that `a`, getting one of the lists:
+do that? Well, for each element `a` in `u`, it applies `f` to that `a`, getting one of the lists:
[] ; result of applying f to leftmost a
[2]
[2; 4]
[2; 4; 8] ; result of applying f to rightmost a
-(or rather, their list' versions). Then it takes the accumulated result `b` of previous steps in the fold, and it folds `k` and `b` over the list generated by `f a`. The result of doing so is passed on to the next step as the accumulated result so far.
+(or rather, their list' versions). Then it takes the accumulated result `b` of previous steps in the `k`,`z`-fold, and it folds `k` and `b` over the list generated by `f a`. The result of doing so is passed on to the next step of the `k`,`z`-fold as the new accumulated result `b`.
So if, for example, we let `k` be `+` and `z` be `0`, then the computation would proceed:
will deliver just the same folds, for arbitrary choices of `k` and `z` (with the right types), and arbitrary `list'`s `u` and appropriately-typed `f`s, as
+ fun k z -> List.fold_right k v z =
fun k z -> List.fold_right k (List.concat (List.map f u)) z
would.
Let's make some more tests:
- l_bind [1; 2] (fun i -> [i; i+1]) ~~> [1; 2; 2; 3]
+ # l_bind [1; 2] (fun i -> [i; i+1]);;
+ - : int list = [1; 2; 2; 3]
- l'_bind (fun f z -> f 1 (f 2 z))
- (fun i -> fun f z -> f i (f (i+1) z)) ~~> <fun>
+ # l'_bind (fun f z -> f 1 (f 2 z)) (fun i -> fun f z -> f i (f (i+1) z));;
+ - : (int -> '_a -> '_a) -> '_a -> '_a = <fun>
Sigh. OCaml won't show us our own list. So we have to choose an `f`
and a `z` that will turn our hand-crafted lists into standard OCaml
lists, so that they will print out.
# let cons h t = h :: t;; (* OCaml is stupid about :: *)
- # l'_bind (fun f z -> f 1 (f 2 z))
- (fun i -> fun f z -> f i (f (i+1) z)) cons [];;
+ # l'_bind (fun f z -> f 1 (f 2 z)) (fun i -> fun f z -> f i (f (i+1) z)) cons [];;
- : int list = [1; 2; 2; 3]
Ta da!
Let's write a general function that will map individuals into their
corresponding generalized quantifier:
- gqize (a : e) = fun (p : e -> t) -> p a
+ gqize (a : e) = fun (p : e -> t) -> p a
-This function is what Partee 1987 calls LIFT, and it would be
-reasonable to use it here, but we will avoid that name, given that we
-use that word to refer to other functions.
+This function is what Partee 1987 calls LIFT, which is not an unreasonable name. But we will avoid her term here, since that word has been used to refer to other functions in our discussion.
This function wraps up an individual in a box. That is to say,
we are in the presence of a monad. The type constructor, the unit and
the bind follow naturally. We've done this enough times that we won't
-belabor the construction of the bind function, the derivation is
+belabor the construction of the bind function. The derivation is
highly similar to the List monad just given:
type 'a continuation = ('a -> 'b) -> 'b
- c_unit (a : 'a) = fun (p : 'a -> 'b) -> p a
- c_bind (u : ('a -> 'b) -> 'b) (f : 'a -> ('c -> 'd) -> 'd) : ('c -> 'd) -> 'd =
+ let c_unit (a : 'a) = fun (p : 'a -> 'b) -> p a
+ let c_bind (u : ('a -> 'b) -> 'b) (f : 'a -> ('c -> 'd) -> 'd) : ('c -> 'd) -> 'd =
fun (k : 'a -> 'b) -> u (fun (a : 'a) -> f a k)
Note that `c_unit` is exactly the `gqize` function that Montague used
-to lift individuals into the continuation monad.
+to lift individuals into generalized quantifiers.
That last bit in `c_bind` looks familiar---we just saw something like
it in the List monad. How similar is it to the List monad? Let's
examine the type constructor and the terms from the list monad derived
above:
- type ('a, 'b) list' = ('a -> 'b -> 'b) -> 'b -> 'b
- let l'_unit a = fun k z -> k a z
+ type ('a, 'b) list' = ('a -> 'b -> 'b) -> 'b -> 'b;;
+ (* that is of the form ('a -> 'r) -> 'r, where 'r = 'b -> 'b *)
+ let l'_unit a = fun k z -> k a z;;
This can be eta-reduced to:
and:
let l'_bind u f =
- (* we mentioned three versions of this, the fully eta-expanded: *)
+ (* we mentioned three versions of this, the eta-expanded: *)
fun k z -> u (fun a b -> f a k b) z
(* an intermediate version, and the fully eta-reduced: *)
fun k -> u (fun a -> f a k)
Our first task will be to replace each leaf with its double:
- let rec treemap (newleaf : 'a -> 'b) (t : 'a tree) : 'b tree =
+ let rec tree_map (leaf_modifier : 'a -> 'b) (t : 'a tree) : 'b tree =
match t with
- | Leaf i -> Leaf (newleaf i)
- | Node (l, r) -> Node (treemap newleaf l,
- treemap newleaf r);;
+ | Leaf i -> Leaf (leaf_modifier i)
+ | Node (l, r) -> Node (tree_map leaf_modifier l,
+ tree_map leaf_modifier r);;
-`treemap` takes a function that transforms old leaves into new leaves,
+`tree_map` takes a function that transforms old leaves into new leaves,
and maps that function over all the leaves in the tree, leaving the
structure of the tree unchanged. For instance:
let double i = i + i;;
- treemap double t1;;
+ tree_map double t1;;
- : int tree =
Node (Node (Leaf 4, Leaf 6), Node (Leaf 10, Node (Leaf 14, Leaf 22)))
| |
14 22
-We could have built the doubling operation right into the `treemap`
-code. However, because what to do to each leaf is a parameter, we can
+We could have built the doubling operation right into the `tree_map`
+code. However, because we've left what to do to each leaf as a parameter, we can
decide to do something else to the leaves without needing to rewrite
-`treemap`. For instance, we can easily square each leaf instead by
+`tree_map`. For instance, we can easily square each leaf instead by
supplying the appropriate `int -> int` operation in place of `double`:
let square i = i * i;;
- treemap square t1;;
+ tree_map square t1;;
- : int tree =ppp
Node (Node (Leaf 4, Leaf 9), Node (Leaf 25, Node (Leaf 49, Leaf 121)))
-Note that what `treemap` does is take some global, contextual
+Note that what `tree_map` does is take some global, contextual
information---what to do to each leaf---and supplies that information
-to each subpart of the computation. In other words, `treemap` has the
+to each subpart of the computation. In other words, `tree_map` has the
behavior of a reader monad. Let's make that explicit.
-In general, we're on a journey of making our treemap function more and
+In general, we're on a journey of making our `tree_map` function more and
more flexible. So the next step---combining the tree transformer with
-a reader monad---is to have the treemap function return a (monadized)
+a reader monad---is to have the `tree_map` function return a (monadized)
tree that is ready to accept any `int -> int` function and produce the
updated tree.
With previous readers, we always knew which kind of environment to
expect: either an assignment function (the original calculator
simulation), a world (the intensionality monad), an integer (the
-Jacobson-inspired link monad), etc. In this situation, it will be
-enough for now to expect that our reader will expect a function of
-type `int -> int`.
+Jacobson-inspired link monad), etc. In the present case, it will be
+enough to expect that our "environment" will be some function of type
+`int -> int`.
type 'a reader = (int -> int) -> 'a;; (* mnemonic: e for environment *)
let reader_unit (a : 'a) : 'a reader = fun _ -> a;;
let reader_bind (u: 'a reader) (f : 'a -> 'b reader) : 'b reader = fun e -> f (u e) e;;
-It's easy to figure out how to turn an `int` into an `int reader`:
+It would be a simple matter to turn an *integer* into an `int reader`:
- let int2int_reader : 'a -> 'b reader = fun (a : 'a) -> fun (op : 'a -> 'b) -> op a;;
- int2int_reader 2 (fun i -> i + i);;
+ let int_readerize : int -> int reader = fun (a : int) -> fun (modifier : int -> int) -> modifier a;;
+ int_readerize 2 (fun i -> i + i);;
- : int = 4
-But what do we do when the integers are scattered over the leaves of a
-tree? A binary tree is not the kind of thing that we can apply a
+But how do we do the analagous transformation when our `int`s are scattered over the leaves of a tree? How do we turn an `int tree` into a reader?
+A tree is not the kind of thing that we can apply a
function of type `int -> int` to.
- let rec treemonadizer (f : 'a -> 'b reader) (t : 'a tree) : 'b tree reader =
+But we can do this:
+
+ let rec tree_monadize (f : 'a -> 'b reader) (t : 'a tree) : 'b tree reader =
match t with
| Leaf i -> reader_bind (f i) (fun i' -> reader_unit (Leaf i'))
- | Node (l, r) -> reader_bind (treemonadizer f l) (fun x ->
- reader_bind (treemonadizer f r) (fun y ->
+ | Node (l, r) -> reader_bind (tree_monadize f l) (fun x ->
+ reader_bind (tree_monadize f r) (fun y ->
reader_unit (Node (x, y))));;
This function says: give me a function `f` that knows how to turn
something of type `'a` into an `'b reader`, and I'll show you how to
-turn an `'a tree` into an `'a tree reader`. In more fanciful terms,
-the `treemonadizer` function builds plumbing that connects all of the
+turn an `'a tree` into an `'b tree reader`. In more fanciful terms,
+the `tree_monadize` function builds plumbing that connects all of the
leaves of a tree into one connected monadic network; it threads the
-`'b reader` monad through the leaves.
+`'b reader` monad through the original tree's leaves.
- # treemonadizer int2int_reader t1 (fun i -> i + i);;
+ # tree_monadize int_readerize t1 double;;
- : int tree =
Node (Node (Leaf 4, Leaf 6), Node (Leaf 10, Node (Leaf 14, Leaf 22)))
Here, our environment is the doubling function (`fun i -> i + i`). If
-we apply the very same `int tree reader` (namely, `treemonadizer
-int2int_reader t1`) to a different `int -> int` function---say, the
+we apply the very same `int tree reader` (namely, `tree_monadize
+int_readerize t1`) to a different `int -> int` function---say, the
squaring function, `fun i -> i * i`---we get an entirely different
result:
- # treemonadizer int2int_reader t1 (fun i -> i * i);;
+ # tree_monadize int_readerize t1 square;;
- : int tree =
Node (Node (Leaf 4, Leaf 9), Node (Leaf 25, Node (Leaf 49, Leaf 121)))
Now that we have a tree transformer that accepts a reader monad as a
parameter, we can see what it would take to swap in a different monad.
+
+<!-- FIXME -->
+
For instance, we can use a state monad to count the number of nodes in
the tree.
let state_unit a = fun s -> (a, s);;
let state_bind_and_count u f = fun s -> let (a, s') = u s in f a (s' + 1);;
-Gratifyingly, we can use the `treemonadizer` function without any
+Gratifyingly, we can use the `tree_monadize` function without any
modification whatsoever, except for replacing the (parametric) type
`'b reader` with `'b state`, and substituting in the appropriate unit and bind:
- let rec treemonadizer (f : 'a -> 'b state) (t : 'a tree) : 'b tree state =
+ let rec tree_monadize (f : 'a -> 'b state) (t : 'a tree) : 'b tree state =
match t with
| Leaf i -> state_bind_and_count (f i) (fun i' -> state_unit (Leaf i'))
- | Node (l, r) -> state_bind_and_count (treemonadizer f l) (fun x ->
- state_bind_and_count (treemonadizer f r) (fun y ->
+ | Node (l, r) -> state_bind_and_count (tree_monadize f l) (fun x ->
+ state_bind_and_count (tree_monadize f r) (fun y ->
state_unit (Node (x, y))));;
Then we can count the number of nodes in the tree:
- # treemonadizer state_unit t1 0;;
+ # tree_monadize state_unit t1 0;;
- : int tree * int =
(Node (Node (Leaf 2, Leaf 3), Node (Leaf 5, Node (Leaf 7, Leaf 11))), 13)
One more revealing example before getting down to business: replacing
-`state` everywhere in `treemonadizer` with `list` gives us
+`state` everywhere in `tree_monadize` with `list` gives us
- # treemonadizer (fun i -> [ [i; square i] ]) t1;;
+ # tree_monadize (fun i -> [ [i; square i] ]) t1;;
- : int list tree list =
[Node
(Node (Leaf [2; 4], Leaf [3; 9]),
let continuation_unit a = fun k -> k a;;
let continuation_bind u f = fun k -> u (fun a -> f a k);;
- let rec treemonadizer (f : 'a -> ('b, 'r) continuation) (t : 'a tree) : ('b tree, 'r) continuation =
+ let rec tree_monadize (f : 'a -> ('b, 'r) continuation) (t : 'a tree) : ('b tree, 'r) continuation =
match t with
| Leaf i -> continuation_bind (f i) (fun i' -> continuation_unit (Leaf i'))
- | Node (l, r) -> continuation_bind (treemonadizer f l) (fun x ->
- continuation_bind (treemonadizer f r) (fun y ->
+ | Node (l, r) -> continuation_bind (tree_monadize f l) (fun x ->
+ continuation_bind (tree_monadize f r) (fun y ->
continuation_unit (Node (x, y))));;
We use the continuation monad described above, and insert the
-`continuation` type in the appropriate place in the `treemonadizer` code.
+`continuation` type in the appropriate place in the `tree_monadize` code.
We then compute:
- # treemonadizer (fun a k -> a :: (k a)) t1 (fun t -> []);;
+ # tree_monadize (fun a k -> a :: (k a)) t1 (fun t -> []);;
- : int list = [2; 3; 5; 7; 11]
+<!-- FIXME: what if we had fun t -> [-t]? why `t`? -->
+
We have found a way of collapsing a tree into a list of its leaves.
The continuation monad is amazingly flexible; we can use it to
simulate some of the computations performed above. To see how, first
-note that an interestingly uninteresting thing happens if we use the
-continuation unit as our first argument to `treemonadizer`, and then
+note that an interestingly uninteresting thing happens if we use
+`continuation_unit` as our first argument to `tree_monadize`, and then
apply the result to the identity function:
- # treemonadizer continuation_unit t1 (fun i -> i);;
+ # tree_monadize continuation_unit t1 (fun i -> i);;
- : int tree =
Node (Node (Leaf 2, Leaf 3), Node (Leaf 5, Node (Leaf 7, Leaf 11)))
That is, nothing happens. But we can begin to substitute more
-interesting functions for the first argument of `treemonadizer`:
+interesting functions for the first argument of `tree_monadize`:
(* Simulating the tree reader: distributing a operation over the leaves *)
- # treemonadizer (fun a k -> k (square a)) t1 (fun i -> i);;
+ # tree_monadize (fun a k -> k (square a)) t1 (fun i -> i);;
- : int tree =
Node (Node (Leaf 4, Leaf 9), Node (Leaf 25, Node (Leaf 49, Leaf 121)))
(* Simulating the int list tree list *)
- # treemonadizer (fun a k -> k [a; square a]) t1 (fun i -> i);;
+ # tree_monadize (fun a k -> k [a; square a]) t1 (fun i -> i);;
- : int list tree =
Node
(Node (Leaf [2; 4], Leaf [3; 9]),
Node (Leaf [5; 25], Node (Leaf [7; 49], Leaf [11; 121])))
(* Counting leaves *)
- # treemonadizer (fun a k -> 1 + k a) t1 (fun i -> 0);;
+ # tree_monadize (fun a k -> 1 + k a) t1 (fun i -> 0);;
- : int = 5
We could simulate the tree state example too, but it would require
As for the associative law,
- Associativity: bind (bind u f) g = bind u (\a. bind (fa) g)
+ 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