<!-- traverse (k: a-> Mb) t = Leaf a -> map Leaf (k a) | Branch(l,col,r) -> map3 Branch l' c' r' -->
<!-- linearize (f: a->Mon) t = Leaf a -> f a | Branch(l,col,r) -> l' && [col' &&] r' -->
- If you look at the definition of `tree_walker` above, you'll see that its interface doesn't supply the `leaf_handler` function with any input like z; the `leaf_handler` only gets the content of each leaf to work on. Thus we're forced to make our `leaf_handler` return a function, that will get its `z` input later. (The strategy used here is like [[the strategy for reversing a list using fold_right in assignment2|assignment2_answers/#cps-reverse]].) Then the `joiner` function chains the results of handling the two branches together, so that when the seed `z` is supplied, we feed it first to `lh` and then the result of that to `rh`. The result of processing any tree then will be a function that expects a `z` argument. Finally, we supply the `z` argument that `tree_foldleft` was invoked with.
+ If you look at the definition of `tree_walker` above, you'll see that its interface doesn't supply the `leaf_handler` function with any input like `z`; the `leaf_handler` only gets the content of each leaf to work on. Thus we're forced to make our `leaf_handler` return a function, that will get its `z` input later. (The strategy used here is like [[the strategy for reversing a list using fold_right in assignment2|assignment2_answers/#cps-reverse]].) Then the `joiner` function chains the results of handling the two branches together, so that when the seed `z` is supplied, we feed it first to `lh` and then the result of that to `rh`. The result of processing any tree then will be a function that expects a `z` argument. Finally, we supply the `z` argument that `tree_foldleft` was invoked with.
5. How would you use the function defined in problem 4 (the previous problem) to sum up the values labeling the leaves of an `(int) color_tree`?
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:
type lambda_term = Var of identifier | Abstract of identifier * lambda_term | App of lambda_term * lambda_term
+<a id="occurs_free"></a>
+
16. Write a function `occurs_free` that has the following type:
occurs_free : identifier -> lambda_term -> bool
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 a `Bool`. 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:
-- Or this:
let sysf_true = (\y n -> y) :: Sysf_bool a
- :set -XExplicitForAll
+ Note that in both OCaml and Haskell code, the generalization `∀α` on the free type variable `α` is implicit. If you really want to, you can supply it explicitly in Haskell by saying:
+
+ :set -XExplicitForAll
let { sysf_true :: forall a. Sysf_bool a; ... }
-- or
let { sysf_true :: forall a. a -> a -> a; ... }
OCAML ANSWERS:
- type ('a) sysf_bool = 'a -> 'a -> 'a
- let sysf_true : ('a) sysf_bool = fun y n -> y
- let sysf_false : ('a) sysf_bool = fun y n -> n
+ type 'a sysf_bool = 'a -> 'a -> 'a
+ let sysf_true : 'a sysf_bool = fun y n -> y
+ let sysf_false : 'a sysf_bool = fun y n -> n
- type ('a) sysf_nat = ('a -> 'a) -> 'a -> 'a
- let sysf_zero : ('a) sysf_nat = fun s z -> z
+ type 'a sysf_nat = ('a -> 'a) -> 'a -> 'a
+ let sysf_zero : 'a sysf_nat = fun s z -> z
- let sysf_iszero (n : 'a sysf_nat) : 'b sysf_bool = n (fun _ -> sysf_false) sysf_true
+ let sysf_iszero (n : ('a sysf_bool) sysf_nat) : 'a sysf_bool = n (fun _ -> sysf_false) sysf_true
(* Annoyingly, though, if you just say sysf_iszero sysf_zero, you'll get an answer that isn't fully polymorphic.
This is explained in the comments linked below. The way to get a polymorphic result is to say instead
`fun next -> sysf_iszero sysf_zero next`. *)
let sysf_succ (n : 'a sysf_nat) : 'a sysf_nat = fun s z -> s (n s z)
- (* Again, to use this you'll want to call `fun next -> sysf_succ sysf_zero next` *)
-
- let sysf_pred (n : 'a sysf_nat) : 'a sysf_nat = (* NOT DONE *)
-
-<!--
- (* Using a System F-style encoding of pairs, rather than native OCaml pairs ... *)
- let pair a b = fun f -> f a b in
- let snd x y next = y next in
- let shift p next = p (fun x y -> pair (sysf_succ x) x) next in (* eta-expanded as in previous definitions *)
- fun next -> n shift (pair sysf_zero sysf_zero) snd next
-
- let pair = \a b. \f. f a b in
- let snd = \x y. y in
- let shift = \p. p (\x y. pair (succ x) x) in
- let pred = \n. n shift (pair 0 err) snd in
--->
-
+ (* Again, to get a polymorphic result you'll want to call `fun next -> sysf_succ sysf_zero next` *)
+
+ And here is how to get `sysf_pred`, using a System-F-style encoding of pairs. (For brevity, I'll leave off the `sysf_` prefixes.)
+
+ type 'a natpair = ('a nat -> 'a nat -> 'a nat) -> 'a nat
+ let natpair (x : 'a nat) (y : 'a nat) : 'a natpair = fun f -> f x y
+ let fst x y = x
+ let snd x y = y
+ let shift (p : 'a natpair) : 'a natpair = natpair (succ (p fst)) (p fst)
+ let pred (n : ('a natpair) nat) : 'a nat = n shift (natpair zero zero) snd
+
+ (* As before, to get polymorphic results you need to eta-expand your applications. Witness:
+ # let one = succ zero;;
+ val one : '_a nat = <fun>
+ # let one next = succ zero next;;
+ val one : ('a -> 'a) -> 'a -> 'a = <fun>
+ # let two = succ one;;
+ val two : '_a nat = <fun>
+ # let two next = succ one next;;
+ val two : ('a -> 'a) -> 'a -> 'a = <fun>
+ # pred two;;
+ - : '_a nat = <fun>
+ # fun next -> pred two next;;
+ - : ('a -> 'a) -> 'a -> 'a = <fun>
+ *)
Consider the following list type, specified using OCaml or Haskell datatypes:
type 'a notok = 'a -> 'a notok
- (In the technical jargon, OCaml has isorecursive not equirecursive types.) In any case, the reason that OCaml rejects b, e, and g is not the mere fact that they involve self-application, but the fact that typing them would require constructing one of the kinds of infinite chains of unbroken arrows that OCaml forbids. In case c, we can already see that the type of `f` is acceptable (it was ok in case a), and the self-application doesn't impose any new typing constraints because it never returns, so it can have any result type at all.
+ (In the technical jargon, OCaml has isorecursive not equirecursive types.) In any case, the reason that OCaml rejects b is not the mere fact that it involves self-application, but the fact that typing it would require constructing one of the kinds of infinite chains of unbroken arrows that OCaml forbids. In case c, we can already see that the type of `f` is acceptable (it was ok in case a), and the self-application doesn't impose any new typing constraints because it never returns, so it can have any result type at all.
- In case g, the typing fails not specifically because of a self-application, but because OCaml has already determined that `f` has to take a `()` argument, and even before settling on `f`'s final type, one thing it knows about `f` is that it isn't `()`. So `let rec f () = f () in f f` fails for the same reason that `let rec f () = f () in f id` would.
+ In cases e and g, the typing fails not specifically because of a self-application, but because OCaml has already determined that `f` has to take a `()` argument, and even before settling on `f`'s final type, one thing it knows about `f` is that it isn't `()`. So `let rec f () = f () in f f` fails for the same reason that `let rec f () = f () in f id` would.
24. Throughout this problem, assume that we have:
m. let _ = blackhole in 2
n. let _ = blackhole () in 2
- ANSWERS: These terminate: a,c,e,f,g,j,m; these don't: b,d,h,i,k,l,n. Generalization: blackhole is a suspended infinite loop, that is forced by feeding it an argument. The expressions that feed blackhole an argument (in a context that is not itself an unforced suspension) won't terminate.
+ ANSWERS: These terminate: a,c,e,f,g,j,m; these don't: b,d,h,i,k,l,n. Generalization: blackhole is a suspended infinite loop, that is forced by feeding it an argument. The expressions that feed blackhole an argument (in a context that is not itself an unforced suspension) won't terminate. Also, unselected clauses of `if`-terms aren't ever evaluated.
25. This problem aims to get you thinking about how to control order of evaluation.
Here is an attempt to make explicit the behavior of `if ... then ... else ...` explored in the previous question.
match b with true -> y () | false -> n ()
- that would arguably still be relying on the special evaluation order properties of OCaml's native `match`. You'd be assuming that `n ()` wouldn't be evaluated in the computation that ends up selecting the other branch. That is correct, but to avoid making that assumption, you should instead first select the `y` or `n` result, _and then afterwards_ force the result. That's what we do in the above answer.
+ that would arguably still be relying on the special evaluation order properties of OCaml's native `match`. You'd be assuming that `n ()` wouldn't be evaluated in the computation that ends up selecting the other branch. Your assumption would be correct, but to avoid making that assumption, you should instead first select the `y` or `n` result, _and then afterwards_ force the result. That's what we do in the above answer.
+
+ Question: don't the rhs of all the match clauses in `match b with true -> y | false -> n` have to have the same type? How can they, when one of them is `blackhole` and the other is `blackhole ()`? The answer has two parts. First is that an expression is allowed to have different types when it occurs several times on the same line: consider `let id x = x in (id 5, id true)`, which evaluates just fine. The second is that `blackhole` will get the type `'a -> 'b`, that is, it can have any functional type at all. So the principle types of `y` and `n` end up being `y : unit -> 'a -> 'b` and `n : unit -> 'c`. (The consequent of `n` isn't constrained to use the same type variable as the consequent of `y`.) OCaml can legitimately infer these to be the same type by unifying the types `'c` and `'a -> 'b`; that is, it instantiates `'c` to the functional type had by `y ()`.