X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=blobdiff_plain;f=exercises%2Fassignment5_answers.mdwn;h=9be28e21a5493191a8200d8f902c191878e38720;hp=f62f8b4f190fc4a00db8416f6e6c9a96a270db39;hb=442a8534983a824eec968ce2bb113fe60e0b1007;hpb=9201e22a70ab4dc37c2d5996d18fa09ef00ea706

diff --git a/exercises/assignment5_answers.mdwn b/exercises/assignment5_answers.mdwn
index f62f8b4f..9be28e21 100644
--- a/exercises/assignment5_answers.mdwn
+++ b/exercises/assignment5_answers.mdwn
@@ -263,7 +263,7 @@ Choose one of these languages and write the following functions.
 
         let rec tree_best_sofar (t : 'a color_tree) (lead : maybe_leader) : maybe_leader * int =
           match t with
-          | Leaf a -> (None, a)
+          | Leaf a -> (lead, a)
           | Branch(l, col, r) ->
               let (lead',left_score) = tree_best_sofar l lead in
               let (lead'',right_score) = tree_best_sofar r lead' in
@@ -436,6 +436,8 @@ Again, we've left some gaps. (The use of `type` for the first line in Haskell an
 
         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
@@ -504,7 +506,7 @@ type `Bool`.
     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.
+    `P -> ∀α. Q` is equivalent to `∀α. 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:
@@ -557,36 +559,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 *)
-
-<!--
-        (* 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: