XGitUrl: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=blobdiff_plain;f=exercises%2Fassignment5_answers.mdwn;h=9618cd3c2f58a16d429703933fc0431a67d0c4d1;hp=8e195ec030edacf32c69e0381ee48b241afb4c13;hb=7c6b9557ee34b8106123687679fe43092fc48103;hpb=c94dd97cfde51a013f14eb8d9bb83aefd29413b7
diff git a/exercises/assignment5_answers.mdwn b/exercises/assignment5_answers.mdwn
index 8e195ec0..9618cd3c 100644
 a/exercises/assignment5_answers.mdwn
+++ b/exercises/assignment5_answers.mdwn
@@ 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 (nonleaf 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 (nonleaf 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; ... }
@@ 548,36 +557,44 @@ any type `Î±`, as long as your function is of type `Î± > Î±` and you have a bas
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 *)



+ (* 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 SystemFstyle 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 etaexpand your applications. Witness:
+ # let one = succ zero;;
+ val one : '_a nat =
+ # let one next = succ zero next;;
+ val one : ('a > 'a) > 'a > 'a =
+ # let two = succ one;;
+ val two : '_a nat =
+ # let two next = succ one next;;
+ val two : ('a > 'a) > 'a > 'a =
+ # pred two;;
+  : '_a nat =
+ # fun next > pred two next;;
+  : ('a > 'a) > 'a > 'a =
+ *)
Consider the following list type, specified using OCaml or Haskell datatypes:
@@ 677,9 +694,9 @@ Do these last three problems specifically with OCaml in mind, not Haskell. Analo
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 selfapplication, 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 selfapplication 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 selfapplication, 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 selfapplication 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 selfapplication, 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 selfapplication, 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:
@@ 704,7 +721,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.
@@ 769,3 +786,5 @@ 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. 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 ()`.