tree_walker leaf_handler joiner t 0
-9. (More challenging.) Assume you have a `color_tree` whose leaves are labeled with `int`s (which may be negative). For this problem, assume also that no color labels multiple `Branch`s (non-leaf nodes). Write a recursive function that reports which color has the greatest "score" when you sum up all the values of its descendent leaves. Since some leaves may have negative values, the answer won't always be the color at the tree root. In the case of ties, you can return whichever of the highest scoring colors you like.
+9. (More challenging.) Assume you have a `color_tree` whose leaves are labeled with `int`s (which may be negative). For this problem, assume also that no color labels multiple `Branch`s (non-leaf nodes). Write a recursive function that reports which color has the greatest "score" when you sum up all the values of its descendant leaves. Since some leaves may have negative values, the answer won't always be the color at the tree root. In the case of ties, you can return whichever of the highest scoring colors you like.
HERE IS A DIRECT OCAML SOLUTION:
true ≡ Λα. λy:α. λn:α. y
false ≡ Λα. λy:α. λn:α. n
not ≡ λp:Bool. p [Bool] false true
- and ≡ λp:Bool. λq:Bool. p [Bool] (q [Bool]) false
- or ≡ λp:Bool. λq:Bool. p [Bool] true (q [Bool])
+ and ≡ λp:Bool. λq:Bool. p [Bool] q false
+ or ≡ λp:Bool. λq:Bool. p [Bool] true q
+
+ When I first wrote up these answers, I had put `(q [Bool])` where I now have just `q` in the body of `and` and `or`. On reflection,
+ this isn't necessary, because `q` is already of that type. But as I learned by checking these answers with Pierce's evaluator, it's
+ also a mistake. What we want is a result whose type is `Bool`, that is, `∀α. α -> α -> α`. `(q [Bool])` doesn't have that type, but
+ rather the type `Bool -> Bool -> Bool`. The first, desired, type has an outermost `∀`. The second, wrong type doesn't; it only has `∀`s
+ inside the antecedents and consequents of the various arrows. The last one of those could be promoted to be an outermost `∀`, since
+ `P -> ∀α. Q ≡ ∀α. P -> Q` when `α` is not free in `P`. But that couldn't be done with the others.
The type `Nat` (for "natural number") may be encoded as follows: