warning about mu, some tweaks

[lambda.git] / exercises / assignment5_answers.mdwn

diff --git a/exercises/assignment5_answers.mdwn b/exercises/assignment5_answers.mdwn
index 7388948..9618cd3 100644 (file)
--- a/exercises/assignment5_answers.mdwn
+++ b/exercises/assignment5_answers.mdwn
@@ -1,14 +1,5 @@
 <!-- λ Λ ∀ ≡ α β ω Ω -->
 
 <!-- λ Λ ∀ ≡ α β ω Ω -->
 

-This is a long and substantial assignment. On the one hand, it doesn't have any stumpers like we gave you in past weeks, such as defining `pred` or mutual recursion. (Well, we *do* ask you to define `pred` again, but now you understand a basic strategy for doing so, so it's no longer a stumper.) On the other hand, there are a bunch of problems; many of them demand a modest amount of time; and this week you're coming to terms with both System F *and* with OCaml or Haskell. So it's a lot to do.
-
-The upside is that there won't be any new homework assigned this week, and you can take longer to complete this assignment if you need to. As always, don't get stuck on the "More challenging" questions if you find them too hard. Be sure to send us your work even if it's not entirely completed, so we can see where you are. And consult with us (over email or in person on Wednesday) about things you don't understand, especially issues you're having working with OCaml or Haskell, or with translating between System F and them. We will update this homework page with clarifications or explanations that your questions prompt.
-
-We will also be assigning some philosophy of language readings for you to look at before this Thursday's seminar meeting.
-
-Those, and lecture notes from this past week, will be posted shortly.
-
-

 
 ## Option / Maybe Types ##
 
 
 ## Option / Maybe Types ##
 


@@ -53,6 +44,13 @@ The OCaml and Haskell solution is to use not supermarket dividers but instead th
 
     You may want to review [[Rosetta pages|/rosetta1]] and also read some of the tutorials we linked to for [[/learning OCaml]] or [[/learning Haskell]].
 
 
     You may want to review [[Rosetta pages|/rosetta1]] and also read some of the tutorials we linked to for [[/learning OCaml]] or [[/learning Haskell]].
 

+    HERE IS AN OCAML ANSWER:
+
+        let maybe_map (f: 'a -> 'b) -> (u : 'a option) : 'b option =
+          match u with
+          | Some a -> Some (f a)
+          | None -> None
+

 
 2.  Next write a `maybe_map2` function. Its type should be:
 
 
 2.  Next write a `maybe_map2` function. Its type should be:
 


@@ -63,6 +61,15 @@ The OCaml and Haskell solution is to use not supermarket dividers but instead th
         maybe_map2 :: (a -> b -> c) -> Maybe a -> Maybe b -> Maybe c
 
 
         maybe_map2 :: (a -> b -> c) -> Maybe a -> Maybe b -> Maybe c
 
 

+    HERE IS AN OCAML ANSWER:
+
+        let maybe_map2 (f : 'a -> 'b -> 'c) (u : 'a option) (v : 'b option) : 'c option =
+          match (u, v) with
+          | Some a, Some b -> Some (f a b)
+          | None, _ -> None
+          | _, None -> None
+
+

 
 ## Color Trees ##
 
 
 ## Color Trees ##
 


@@ -93,12 +100,12 @@ Here's how you pattern match such a tree, binding variables to its components:
     (* OCaml *)
     match t with
     | Leaf n -> false
     (* OCaml *)
     match t with
     | Leaf n -> false

-    | Branch (_, c, _) -> c = Red
+    | Branch (_, col, _) -> col = Red

 
     -- Haskell
     case t of {
       Leaf n -> False;
 
     -- Haskell
     case t of {
       Leaf n -> False;

-      Branch _ c _ -> c == Red
+      Branch _ col _ -> col == Red

     }
 
 These expressions query whether `t` is a branching `color_tree` (that is, not a leaf) whose root is labeled `Red`.
     }
 
 These expressions query whether `t` is a branching `color_tree` (that is, not a leaf) whose root is labeled `Red`.


@@ -110,14 +117,93 @@ Choose one of these languages and write the following functions.
 
 3.  Define a function `tree_map` whose type is (as shown by OCaml): `('a -> 'b) -> ('a) color_tree -> ('b) color_tree`. It expects a function `f` and an `('a) color_tree`, and returns a new tree with the same structure and inner branch colors as the original, but with all of its leaves now having had `f` applied to their original value. So for example, `map (fun x->2*x) t1` would return `t1` with all of its leaf values doubled.
 
 
 3.  Define a function `tree_map` whose type is (as shown by OCaml): `('a -> 'b) -> ('a) color_tree -> ('b) color_tree`. It expects a function `f` and an `('a) color_tree`, and returns a new tree with the same structure and inner branch colors as the original, but with all of its leaves now having had `f` applied to their original value. So for example, `map (fun x->2*x) t1` would return `t1` with all of its leaf values doubled.
 

+    HERE IS A DIRECT OCAML ANSWER:
+
+        let rec tree_map (f: 'a -> 'b) (t: 'a color_tree) : 'b color_tree =
+          match t with
+          | Leaf a -> Leaf (f a)
+          | Branch (l,col,r) ->
+              let l' = tree_map f l in
+              let r' = tree_map f r in
+              Branch(l', col, r')
+
+    IT MIGHT BE USEFUL TO GENERALIZE THIS PATTERN, LIKE SO:
+
+        let rec tree_walker (leaf_handler: 'a -> 'h) (joiner : 'h -> color -> 'h -> 'h) (t: 'a color_tree) : 'h =
+          match t with
+          | Leaf a -> leaf_handler a
+          | Branch (l,col,r) ->
+              let lh = tree_walker leaf_handler joiner l in
+              let rh = tree_walker leaf_handler joiner r in
+              joiner lh col rh
+
+    <!-- traverse (k: a-> Mb) t = Leaf a -> map Leaf (k a) | Branch(l,col,r) -> map3 Branch l' c' r' -->
+
+    THEN `tree_map f t` can be defined as `tree_walker (fun a -> Leaf (f a)) (fun l' col r' -> Branch(l',col,r')) t`
+
+

 4.  Define a function `tree_foldleft` that accepts an argument `g : 'z -> 'a -> 'z` and a seed value `z : 'z` and a tree  `t : ('a) color_tree`, and returns the result of applying `g` first to `z` and `t`'s leftmost leaf, and then applying `g` to *that result* and `t`'s second-leftmost leaf, and so on, all the way across `t`'s fringe. In our examples, only the leaf values affect the result; the inner branch colors are ignored.
 
 4.  Define a function `tree_foldleft` that accepts an argument `g : 'z -> 'a -> 'z` and a seed value `z : 'z` and a tree  `t : ('a) color_tree`, and returns the result of applying `g` first to `z` and `t`'s leftmost leaf, and then applying `g` to *that result* and `t`'s second-leftmost leaf, and so on, all the way across `t`'s fringe. In our examples, only the leaf values affect the result; the inner branch colors are ignored.
 

+    HERE IS A DIRECT OCAML ANSWER:
+
+        let rec tree_foldleft (g: 'z -> 'a -> 'z) (z : 'z) (t: 'a color_tree) : 'z =
+          match t with
+          | Leaf a -> g z a
+          | Branch (l,_,r) ->
+              let z' = tree_foldleft g z l in
+              let z'' = tree_foldleft g z' r in
+              r''
+
+    HERE IS AN ANSWER THAT RE-USES OUR `tree_walker` FUNCTION FROM THE PREVIOUS ANSWER:
+
+        let tree_foldleft g z t =
+          let leaf_handler a = fun z -> g z a in
+          let joiner lh _ rh = fun z -> rh (lh z) in
+          let expects_z = tree_walker leaf_handler joiner t in
+          expects_z z
+
+    <!-- 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.
+
+

 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`?
 
 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`?
 

+    ANSWER: `tree_foldleft (fun z a -> z + a) 0 your_tree`
+

 6.  How would you use the function defined in problem 4 to enumerate a tree's fringe? (Don't worry about whether it comes out left-to-right or right-to-left.)
 
 6.  How would you use the function defined in problem 4 to enumerate a tree's fringe? (Don't worry about whether it comes out left-to-right or right-to-left.)
 

+    ANSWER: `tree_foldleft (fun z a -> a :: z) [] your_tree`
+

 7.  Write a recursive function to make a copy of a `color_tree` with the same structure and inner branch colors, but where the leftmost leaf is now labeled `0`, the second-leftmost leaf is now labeled `1`, and so on. (Here's a [[hint|assignment5 hint3]], if you need one.)
 
 7.  Write a recursive function to make a copy of a `color_tree` with the same structure and inner branch colors, but where the leftmost leaf is now labeled `0`, the second-leftmost leaf is now labeled `1`, and so on. (Here's a [[hint|assignment5 hint3]], if you need one.)
 

+    HERE IS A DIRECT OCAML ANSWER, FOLLOWING [[the hint|assignment5_hint3]]:
+
+        let rec enumerate_from (t:'a color_tree) counter =
+          match t with
+          | Leaf x -> (Leaf counter, counter+1)
+          | Branch (left,col,right) -> let (left',counter') = enumerate_from left counter in
+                                       let (right',counter'') = enumerate_from right counter' in
+                                       (Branch (left',col,right'), counter'')
+
+        (* then this will be the function we were asked for *)
+        let enumerate t =
+          let (t', _) = enumerate_from t 0 in
+          t'
+
+    IT WOULD ALSO BE POSSIBLE TO WRITE THIS USING OUR `tree_walker` FUNCTION, USING A TECHNIQUE THAT COMBINES THE STRATEGY USED ABOVE WITH THE ONE USED IN `tree_foldleft`:
+
+        let enumerate t =
+          let leaf_handler a = fun counter -> (Leaf counter, counter+1) in
+          let joiner lh col rh =
+            fun counter ->
+              let (left',counter') = lh counter in
+              let (right',counter'') = rh counter' in
+              (Branch (left',col,right'), counter'') in
+          fst (tree_walker leaf_handler joiner t 0)
+
+

 8.  (More challenging.) Write a recursive function that makes a copy of a `color_tree` with the same structure and inner branch colors, but replaces each leaf label with the `int` that reports how many of that leaf's ancestors are labeled `Red`. For example, if we give your function a tree:
 
     <pre>
 8.  (More challenging.) Write a recursive function that makes a copy of a `color_tree` with the same structure and inner branch colors, but replaces each leaf label with the `int` that reports how many of that leaf's ancestors are labeled `Red`. For example, if we give your function a tree:
 
     <pre>


@@ -144,7 +230,73 @@ Choose one of these languages and write the following functions.
               2   2
     </pre>
 
               2   2
     </pre>
 

-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.
+    HERE IS A DIRECT OCAML SOLUTION:
+
+        let rec tree_red_ancestors_from (cur : int) (t : 'a tree) : int tree =
+          match t with
+          | Leaf a -> Leaf cur
+          | Branch(l, col, r) ->
+              let cur' = if col = Red then cur + 1 else cur in
+              let l' = tree_red_ancestors_from cur' l in
+              let r' = tree_red_ancestors_from cur' r in
+              Branch(l',col,r')
+
+        (* here is the function we were asked for *)
+        let tree_red_ancestors t = tree_red_ancestors_from 0 t
+
+
+    HERE IS HOW TO DO IT USING `tree_walker`:
+
+        let tree_red_ancestors t =
+          let leaf_handler a = fun cur -> Leaf cur in
+          let joiner lh col rh = fun cur ->
+            let cur' = if col = Red then cur + 1 else cur in
+            Branch(lh cur', col, rh cur') in
+          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 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 maybe_leader = (color * int) option
+
+        let rec tree_best_sofar (t : 'a color_tree) (lead : maybe_leader) : maybe_leader * int =
+          match t with
+          | Leaf a -> (None, 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
+              let my_score = left_score + right_score in
+              (match lead'' with
+              | None -> Some(col,my_score), my_score
+              | Some(_, lead_score) -> (if my_score > lead_score then Some(col,my_score) else lead''), my_score)
+
+        (* Note that the invocations of that function have to return who-is-the-current-leader?
+           plus their OWN score, even if they are not the current leader. Their parents need the
+           second value to calculate whether they should become the current leader. *)
+
+        (* here is the function we were asked for *)
+        let tree_best t =
+          match tree_best_sofar t None with
+          | Some(leader,leader_score), _ -> leader
+          | None, _ -> failwith "no colors"
+
+
+    HERE IS HOW TO DO IT USING `tree_walker`:
+
+        let tree_best_sofar t =
+          let leaf_handler a = fun leader -> leader, a in
+          let joiner lh col rh = fun leader ->
+            let (leader',left_score) = lh leader in
+            let (leader'',right_score) = rh leader' in
+            let my_score = left_score + right_score in
+            (match leader'' with
+            | None -> Some(col,my_score), my_score
+            | Some(_,leader_score) -> (if my_score > leader_score then Some(col,my_score) else leader''), my_score) in
+          tree_walker leaf_handler joiner t
+
+    Then `tree_best` could be defined as in the direct answer.

 
 
 ## Search Trees ##
 
 
 ## Search Trees ##


@@ -171,6 +323,17 @@ That is, its leaves have no labels and its inner nodes are labeled with `int`s.
 
     Your function should search through the tree for the specified `int`. If it's never found, it should return the value OCaml calls `None` and Haskell calls `Nothing`. If it finds the `int` right at the root of the `search_tree`, it should return the value OCaml calls `Some []` and Haskell calls `Just []`. If it finds the `int` by first going down the left branch from the tree root, and then going right twice, it should return `Some [Left; Right; Right]` or `Just [Left, Right, Right]`.
 
 
     Your function should search through the tree for the specified `int`. If it's never found, it should return the value OCaml calls `None` and Haskell calls `Nothing`. If it finds the `int` right at the root of the `search_tree`, it should return the value OCaml calls `Some []` and Haskell calls `Just []`. If it finds the `int` by first going down the left branch from the tree root, and then going right twice, it should return `Some [Left; Right; Right]` or `Just [Left, Right, Right]`.
 

+    HERE IS AN OCAML ANSWER:
+
+        let search_for (sought : int) (t : search_tree) : direction list option =
+          let rec aux (trace : direction list) t =
+            match t with
+            | Nil -> None
+            | Inner(l,x,r) when sought < x -> aux (Left::trace) l
+            | Inner(l,x,r) when sought > x -> aux (Right::trace) r
+            | _ -> Some(List.rev trace) in
+        aux [] t
+

 
 ## More Map2s ##
 
 
 ## More Map2s ##
 


@@ -189,8 +352,18 @@ In question 2 above, you defined `maybe_map2`. [[Before|assignment1]] we encount
     <!-- or `f <$/fmap> ZipList xs <*/ap> ZipList ys`; or `pure f <*> ...`; or `liftA2 f (ZipList xs) (ZipList ys)` -->
     But we want you to write this function from scratch.)
 
     <!-- or `f <$/fmap> ZipList xs <*/ap> ZipList ys`; or `pure f <*> ...`; or `liftA2 f (ZipList xs) (ZipList ys)` -->
     But we want you to write this function from scratch.)
 

+    HERE IS AN OCAML ANSWER:
+
+        let rec map2_zip f xs ys =
+          match xs, ys with
+          | [], _ -> []
+          | _, [] -> []
+          | x'::xs', y'::ys' -> f x' y' :: map2_zip f xs' ys'
+

 12. What is the relation between the function you just wrote, and the `maybe_map2` function you wrote for problem 2, above?
 
 12. What is the relation between the function you just wrote, and the `maybe_map2` function you wrote for problem 2, above?
 

+    ANSWER: option/Maybe types are like lists constrained to be of length 0 or 1.
+

 13. Another strategy is to take the *cross product* of the two lists. If the function:
 
         (* OCaml *)
 13. Another strategy is to take the *cross product* of the two lists. If the function:
 
         (* OCaml *)


@@ -199,6 +372,13 @@ In question 2 above, you defined `maybe_map2`. [[Before|assignment1]] we encount
     is applied to the arguments `f`, `[x0, x1, x2]`, and `[y0, y1]`, then the result should be: `[f x0 y0, f x0 y1, f x1 y0, f x1 y1, f x2 y0, f x2 y1]`. Write this function.
     <!-- in Haskell, `liftA2 f xs ys` -->
 
     is applied to the arguments `f`, `[x0, x1, x2]`, and `[y0, y1]`, then the result should be: `[f x0 y0, f x0 y1, f x1 y0, f x1 y1, f x2 y0, f x2 y1]`. Write this function.
     <!-- in Haskell, `liftA2 f xs ys` -->
 

+    HERE IS AN OCAML ANSWER:
+
+        let rec map2_cross f xs ys =
+          match xs with
+          | [] -> []
+          | x'::xs' -> List.append (List.map (f x') ys) (map2_cross f xs' ys)
+

 A similar choice between "zipping" and "crossing" could be made when `map2`-ing two trees. For example, the trees:
 
 <pre>
 A similar choice between "zipping" and "crossing" could be made when `map2`-ing two trees. For example, the trees:
 
 <pre>


@@ -252,14 +432,25 @@ Again, we've left some gaps. (The use of `type` for the first line in Haskell an
 
 15. Choose one of these languages and fill in the gaps to complete the definition.
 
 
 15. Choose one of these languages and fill in the gaps to complete the definition.
 

+    HERE IS AN OCAML DEFINITION:
+
+        type lambda_term = Var of identifier | Abstract of identifier * lambda_term | App of lambda_term * lambda_term
+

 16. Write a function `occurs_free` that has the following type:
 
         occurs_free : identifier -> lambda_term -> bool
 
     That's how OCaml would show it. Haskell would use double colons `::` instead, and would also capitalize all the type names. Your function should tell us whether the supplied identifier ever occurs free in the supplied `lambda_term`.
 
 16. Write a function `occurs_free` that has the following type:
 
         occurs_free : identifier -> lambda_term -> bool
 
     That's how OCaml would show it. Haskell would use double colons `::` instead, and would also capitalize all the type names. Your function should tell us whether the supplied identifier ever occurs free in the supplied `lambda_term`.
 

+    HERE IS AN OCAML ANSWER:

 
 

+        let rec occurs_free (ident : identifier) (term : lambda_term) : bool =
+          match term with
+          | Var var_ident -> ident = var_ident (* `x` is free in Var "x" but not in Var "y" *)
+          | Abstract(bound_ident, body) -> ident <> bound_ident && occurs_free ident body (* `x` is free in \y. x but not in \x. blah or \y. y *)
+          | App (head, arg) -> occurs_free ident head || occurs_free ident arg

 
 

+  

 
 ## Encoding Booleans, Church numerals, and Right-Fold Lists in System F ##
 
 
 ## Encoding Booleans, Church numerals, and Right-Fold Lists in System F ##
 


@@ -299,6 +490,23 @@ type `Bool`.
     (b) the term `and` that takes two arguments of type `Bool` and computes their conjunction  
     (c) the term `or` that takes two arguments of type `Bool` and computes their disjunction
 
     (b) the term `and` that takes two arguments of type `Bool` and computes their conjunction  
     (c) the term `or` that takes two arguments of type `Bool` and computes their disjunction
 

+    ANSWERS:
+
+        Bool ≡ ∀α. α -> α -> α
+        true ≡ Λα. λy:α. λn:α. y
+        false ≡ Λα. λy:α. λn:α. n
+        not ≡ λp:Bool. p [Bool] false true
+        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:
 
     Nat ≡ ∀α. (α -> α) -> α -> α
 The type `Nat` (for "natural number") may be encoded as follows:
 
     Nat ≡ ∀α. (α -> α) -> α -> α


@@ -329,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
 
         -- 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; ... }
         let { sysf_true :: forall a. Sysf_bool a; ... }
         -- or
         let { sysf_true :: forall a. a -> a -> a; ... }


@@ -345,6 +555,46 @@ any type `α`, as long as your function is of type `α -> α` and you have a bas
     It's especially useful for you to implement a version of a System F encoding `pred`, starting with one of the (untyped) versions available in [[assignment3 answers]].
 
 
     It's especially useful for you to implement a version of a System F encoding `pred`, starting with one of the (untyped) versions available in [[assignment3 answers]].
 
 

+    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_nat = ('a -> 'a) -> 'a -> 'a
+        let sysf_zero : 'a sysf_nat = fun s z -> z
+
+        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 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:
 
 
 Consider the following list type, specified using OCaml or Haskell datatypes:
 


@@ -396,7 +646,6 @@ Be sure to test your proposals with simple lists. (You'll have to `sysf_cons` up
 
 
 
 
 
 

-

 ## More on Types ##
 
 22.  Recall that the **S** combinator is given by `\f g x. f x (g x)`. Give two different typings for this term in OCaml or Haskell. To get you started, here's one typing for **K**:
 ## More on Types ##
 
 22.  Recall that the **S** combinator is given by `\f g x. f x (g x)`. Give two different typings for this term in OCaml or Haskell. To get you started, here's one typing for **K**:


@@ -408,7 +657,15 @@ Be sure to test your proposals with simple lists. (You'll have to `sysf_cons` up
 
     If you can't understand how one term can have several types, recall our discussion in this week's notes of "principal types". 
 
 
     If you can't understand how one term can have several types, recall our discussion in this week's notes of "principal types". 
 

+    ANSWER: OCaml shows the principal typing for S as follows:
+
+        # let s = fun f g x -> f x (g x);;
+        val s : ('a -> 'b -> 'c) -> ('a -> 'b) -> 'a -> 'c = <fun>
+
+    You can get a more specific type by unifying any two or more of the above type variables. Thus, here is one other type that S can have:

 
 

+        # let s' = (s : ('a -> 'b -> 'a) -> ('a -> 'b) -> 'a -> 'a);;
+        val s' : ('a -> 'b -> 'a) -> ('a -> 'b) -> 'a -> 'a = <fun>

 
 
 ## Evaluation Order ##
 
 
 ## Evaluation Order ##


@@ -418,14 +675,29 @@ Do these last three problems specifically with OCaml in mind, not Haskell. Analo
 
 23.  Which of the following expressions is well-typed in OCaml? For those that are, give the type of the expression as a whole. For those that are not, why not?
 
 
 23.  Which of the following expressions is well-typed in OCaml? For those that are, give the type of the expression as a whole. For those that are not, why not?
 

-        let rec f x = f x
-        let rec f x = f f
-        let rec f x = f x in f f
-        let rec f x = f x in f ()
-        let rec f () = f f
-        let rec f () = f ()
-        let rec f () = f () in f f
-        let rec f () = f () in f ()
+        a. let rec f x = f x
+        b. let rec f x = f f
+        c. let rec f x = f x in f f
+        d. let rec f x = f x in f ()
+        e. let rec f () = f f
+        f. let rec f () = f ()
+        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.
+
+    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:
 
 
 24.  Throughout this problem, assume that we have:
 


@@ -434,20 +706,22 @@ Do these last three problems specifically with OCaml in mind, not Haskell. Analo
     <!-- Haskell could say: `let blackhole = \x -> fix (\f -> f)` -->
     All of the following are well-typed. Which ones terminate?  What generalizations can you make?
 
     <!-- Haskell could say: `let blackhole = \x -> fix (\f -> f)` -->
     All of the following are well-typed. Which ones terminate?  What generalizations can you make?
 

-        blackhole
-        blackhole ()
-        fun () -> blackhole ()
-        (fun () -> blackhole ()) ()
-        if true then blackhole else blackhole
-        if false then blackhole else blackhole
-        if true then blackhole else blackhole ()
-        if false then blackhole else blackhole ()
-        if true then blackhole () else blackhole
-        if false then blackhole () else blackhole
-        if true then blackhole () else blackhole ()
-        if false then blackhole () else blackhole ()
-        let _ = blackhole in 2
-        let _ = blackhole () in 2
+        a. blackhole
+        b. blackhole ()
+        c. fun () -> blackhole ()
+        d. (fun () -> blackhole ()) ()
+        e. if true then blackhole else blackhole
+        f. if false then blackhole else blackhole
+        g. if true then blackhole else blackhole ()
+        h. if false then blackhole else blackhole ()
+        i. if true then blackhole () else blackhole
+        j. if false then blackhole () else blackhole
+        k. if true then blackhole () else blackhole ()
+        l. if false then blackhole () else blackhole ()
+        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. 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.
 
 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.


@@ -498,3 +772,19 @@ and that `bool` is any boolean expression.  Then we can try the following:
     does not terminate.  Incidentally, using the shorter `match bool with true -> yes | false -> no` rather than the longer `let b = bool ... in match b with ...` *would* work as we desire. But your assignment is to control the evaluation order *without* using the special evaluation order properties of OCaml's native `if` or of its `match`. That is, you must keep the `let b = ... in match b with ...` structure in your answer, though you are allowed to adjust what `b`, `y`, and `n` get assigned to.
 
     Here's a [[hint|assignment5 hint1]].
     does not terminate.  Incidentally, using the shorter `match bool with true -> yes | false -> no` rather than the longer `let b = bool ... in match b with ...` *would* work as we desire. But your assignment is to control the evaluation order *without* using the special evaluation order properties of OCaml's native `if` or of its `match`. That is, you must keep the `let b = ... in match b with ...` structure in your answer, though you are allowed to adjust what `b`, `y`, and `n` get assigned to.
 
     Here's a [[hint|assignment5 hint1]].

+
+    ANSWER:
+
+        let rec blackhole x = blackhole x in
+        let b = true in
+        let y () = blackhole in
+        let n () = blackhole () in
+        (match b with true -> y | false -> n) ()
+
+    If you said instead, on the last line:
+
+        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 ()`.