Red / \ Blue \ / \ Green a b / \ c Red / \ d e(for any leaf values `a` through `e`), it should return:

Red / \ Blue \ / \ Green 1 1 / \ 1 Red / \ 2 2HERE 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 ## (More challenging.) For the next problem, assume the following type definition: (* OCaml *) type search_tree = Nil | Inner of search_tree * int * search_tree -- Haskell data Search_tree = Nil | Inner Search_tree Int Search_tree deriving (Show) That is, its leaves have no labels and its inner nodes are labeled with `int`s. Additionally, assume that all the `int`s in branches descending to the left from a given node will be less than the `int` of that parent node, and all the `int`s in branches descending to the right will be greater. We can't straightforwardly specify this constraint in OCaml's or Haskell's type definitions. We just have to be sure to maintain it by hand. 10. Write a function `search_for` with the following type, as displayed by OCaml: type direction = Left | Right search_for : int -> search_tree -> direction list option Haskell would say instead: data Direction = Left | Right deriving (Eq, Show) search_for :: Int -> Search_tree -> Maybe [Direction] 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 ## In question 2 above, you defined `maybe_map2`. [[Before|assignment1]] we encountered `map2` for lists. There are in fact several different approaches to mapping two lists together. 11. One approach is to apply the supplied function to the first element of each list, and then to the second element of each list, and so on, until the lists are exhausted. If the lists are of different lengths, you might stop with the shortest, or you might raise an error. Different implementations make different choices about that. Let's call this function: (* OCaml *) map2_zip : ('a -> 'b -> 'c) -> ('a) list -> ('b) list -> ('c) list Write a recursive function that implements this, in Haskell or OCaml. Let's say you can stop when the shorter list runs out, if they're of different lengths. (OCaml and Haskell each already have functions in their standard libraries --- `map2` or `zipWith` -- that do this. And it also corresponds to a list comprehension you can write in Haskell like this: :set -XParallelListComp [ f x y | x <- xs | y <- 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? 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 *) map2_cross : ('a -> 'b -> 'c) -> ('a) list -> ('b) list -> ('c) list 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. 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:

0 5 / \ / \ 1 2 6 7 / \ / \ 3 4 8 9could be "zipped" like this (ignoring any parts of branches on the one tree that extend farther than the corresponding branch on the other):

f 0 5 / \ f 1 6 f 2 714. You can try defining that if you like, for extra credit. "Crossing" the trees would instead add copies of the second tree as subtrees replacing each leaf of the original tree, with the leaves of that larger tree labeled with `f` applied to `3` and `6`, then `f` applied to `3` and `8`, and so on across the fringe of the second tree; then beginning again (in the subtree that replaces the `4` leaf) with `f` applied to `4` and `6`, and so on. * In all the plain `map` functions, whether for lists, or for `option`/`Maybe`s, or for trees, the structure of the result exactly matched the structure of the argument. * In the `map2` functions, whether for lists or for `option`/`Maybe`s or for trees, and whether done in the "zipping" style or in the "crossing" style, the structure of the result may be a bit different from the structure of the arguments. But the *structure* of the arguments is enough to determine the structure of the result; you don't have to look at the specific list elements or labels on a tree's leaves or nodes to know what the *structure* of the result will be. * We can imagine more radical transformations, where the structure of the result *does* depend on what specific elements the original structure(s) had. For example, what if we had to transform a tree by turning every leaf into a subtree that contained all of those leaf's prime factors? Or consider our problem from [[assignment3]] where you converted `[3, 1, 0, 2]` not into `[[3,3,3], [1], [], [2,2]]` --- which still has the same structure, that is length, as the original --- but rather into `[3, 3, 3, 1, 2, 2]` --- which doesn't. (Some of you had the idea last week to define this last transformation in Haskell as `[x | x <- [3,1,0,2], y <- [0..(x-1)]]`, which just looks like a cross product, that we counted under the *previous* bullet point. However, in that expression, the second list's structure depends upon the specific values of the elements in the first list. So it's still true, as I said, that you can't specify the structure of the output list without looking at those elements.) These three levels of how radical a transformation you are making to a structure, and the parallels between the transformations to lists, to `option`/`Maybe`s, and to trees, will be ideas we build on in coming weeks. ## Untyped Lambda Terms ## In OCaml, you can define some datatypes that represent terms in the untyped Lambda Calculus like this: type identifier = string type lambda_term = Var of identifier | Abstract of identifier * _____ | App of _____ We've left some gaps. In Haskell, you'd define it instead like this: type Identifier = String data Lambda_term = Var Identifier | Abstract Identifier _____ | App ________ deriving (Show) Again, we've left some gaps. (The use of `type` for the first line in Haskell and `data` for the second line is not a typo. The first specifies that `Identifier` will be just a shorthand for an already existing type. The second introduces a new datatype, with its own variant/constructor tags.) 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`. 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 ## (For the System F questions, you can either work on paper, or [download and compile](http://www.cis.upenn.edu/~bcpierce/tapl/resources.html#checkers) Pierce's evaluator for system F to test your work. Under the "implementations" link on that page, you want to use Pierce's `fullpoly` or the `fullomega` code. The Chapters of Pierce's book *Types and Programming Languages* most relevant to this week's lectures are 22 and 23; though for context we also recommend at least Chapters 8, 9, 11, 20, and 29. We don't expect most of you to follow these recommendations now, or even to be comfortable enough yet with the material to be *able* to. We're providing the pointers as references that some might conceivably pursue now, and others later.) Let's think about the encodings of booleans, numerals and lists in System F, and get datatypes with the same form working in OCaml or Haskell. (Of course, OCaml and Haskell have *native* versions of these types: OCaml's `true`, `1`, and `[1;2;3]`. But the point of our exercise requires that we ignore those.) Recall from class System F, or the polymorphic λ-calculus, with this grammar: types ::= constants | α ... | type1 -> type2 | ∀α. type expressions ::= x ... | λx:type. expr | expr1 expr2 | Λα. expr | expr [type] The boolean type, and its two values, may be encoded as follows: Bool ≡ ∀α. α -> α -> α true ≡ Λα. λy:α. λn:α. y false ≡ Λα. λy:α. λn:α. n It's used like this: b [T] res1 res2 where `b` is a `Bool` value, and `T` is the shared type of `res1` and `res2`. 17. How should we implement the following terms? Note that the result of applying them to the appropriate arguments should also give us a term of type `Bool`. (a) the term `not` that takes an argument of type `Bool` and computes its negation (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 ≡ ∀α. (α -> α) -> α -> α zero ≡ Λα. λs:α -> α. λz:α. z succ ≡ λn:Nat. Λα. λs:α -> α. λz:α. s (n [α] s z) A number `n` is deﬁned by what it can do, which is to compute a function iterated `n` times. In the polymorphic encoding above, the result of that iteration can be any type `α`, as long as your function is of type `α -> α` and you have a base element of type `α`. 18. Translate these encodings of booleans and Church numbers into OCaml or Haskell, implementing versions of `sysf_bool`, `sysf_true`, `sysf_false`, `sysf_nat`, `sysf_zero`, `sysf_iszero` (this is what we'd earlier write as `zero?`, but you can't use `?`s in function names in OCaml or Haskell), `sysf_succ`, and `sysf_pred`. We include the `sysf_` prefixes so as not to collide with any similarly-named native functions or values in these languages. The point of the exercise is to do these things on your own, so avoid using the built-in OCaml or Haskell booleans and integers. Keep in mind the capitalization rules. In OCaml, types are written `sysf_bool`, and in Haskell, they are capitalized `Sysf_bool`. In both languages, variant/constructor tags (like `None` or `Some`) are capitalized, and function names start lowercase. But for this problem, you shouldn't need to use any variant/constructor tags. To get you started, here is how to define `sysf_bool` and `sysf_true` in OCaml: type ('a) sysf_bool = 'a -> 'a -> 'a let sysf_true : ('a) sysf_bool = fun y n -> y And here in Haskell: type Sysf_bool a = a -> a -> a -- this is another case where Haskell uses `type` instead of `data` -- To my mind the natural thing to write next would be: let sysf_true :: Sysf_bool a = \y n -> y -- But for complicated reasons, that won't work, and you need to do this instead: let { sysf_true :: Sysf_bool a; sysf_true = \y n -> y } -- Or this: let sysf_true = (\y n -> y) :: Sysf_bool a 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; ... } You can't however, put a `forall a.` in the `type Sysf_bool ...` declaration. The reasons for this are too complicated to explain here. Note also that `sysf_true` can be applied to further arguments directly: sysf_true 10 20 You don't do anything like System F's `true [int] 10 20`. The OCaml and Haskell interpreters figure out what type `sysf_true` needs to be specialized to (in this case, to `int`), and do that automatically. 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_nat) : 'b 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 *) Consider the following list type, specified using OCaml or Haskell datatypes: (* OCaml *) type ('t) my_list = Nil | Cons of 't * 't my_list -- Haskell data My_list t = Nil | Cons t (My_list t) deriving (Show) We can encode that type into System F in terms of its right-fold, just as we did in the untyped Lambda Calculus, like this: list_T ≡ ∀α. (T -> α -> α) -> α -> α nil_T ≡ Λα. λc:T -> α -> α. λn:α. n cons_T ≡ λx:T. λxs:list_T. Λα. λc:T -> α -> α. λn:α. c x (xs [α] c n) As with `Nat`s, the natural recursion on the type is built into our encoding of it. There is some awkwardness here, because System F doesn't have any parameterized types like OCaml's `('t) my_list` or Haskell's `My_list t`. For those, we need to use a more complex system called System F