X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=blobdiff_plain;f=exercises%2Fassignment5_answers.mdwn;h=f62f8b4f190fc4a00db8416f6e6c9a96a270db39;hp=b591330b05409c2b54aa2e0e07de4a73bbfde570;hb=9201e22a70ab4dc37c2d5996d18fa09ef00ea706;hpb=fdca7e1fb19e83509ce56851768d8ce827fafbed
diff --git a/exercises/assignment5_answers.mdwn b/exercises/assignment5_answers.mdwn
index b591330b..f62f8b4f 100644
--- a/exercises/assignment5_answers.mdwn
+++ b/exercises/assignment5_answers.mdwn
@@ -165,7 +165,7 @@ Choose one of these languages and write the following functions.
- 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`?
@@ -255,7 +255,7 @@ Choose one of these languages and write the following functions.
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:
@@ -496,8 +496,15 @@ type `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:
@@ -530,7 +537,9 @@ any type `Î±`, as long as your function is of type `Î± -> Î±` and you have a bas
-- 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; ... }
@@ -667,7 +676,20 @@ Do these last three problems specifically with OCaml in mind, not Haskell. Analo
g. let rec f () = f () in f f
h. let rec f () = f () in f ()
- ANSWER: All are well-typed except for b, e, and g, which involve self-application. d and h are well-typed but enter an infinite loop. Surprisingly, OCaml's type-checker accepts c, and it too enters an infinite loop. Not sure how to explain why OCaml's type-checker accepts that.
+ ANSWER: All are well-typed except for b, e, and g, which involve self-application. d and h are well-typed but enter an infinite loop. Surprisingly, OCaml's type-checker accepts c, and it too enters an infinite loop.
+
+ OCaml is not in principle opposed to self-application: `let id x = x in id id` works fine. Neither is it in principle opposed to recursive/infinite types. But it demands that they not be infinite chains of unbroken arrows. There have to be some intervening datatype constructors. Thus this is an acceptable type definition:
+
+ type 'a ok = Cons of ('a -> 'a ok)
+
+ But this is not:
+
+ 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 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 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:
@@ -691,7 +713,7 @@ Do these last three problems specifically with OCaml in mind, not Haskell. Analo
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.
@@ -755,4 +777,6 @@ and that `bool` is any boolean expression. Then we can try the following:
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 ()`.