Option / Maybe Types

You've already (in assignment1 and week2 encodings) defined and worked with map as a function on lists. Now we're going to work instead with the type OCaml defines like this:

type ('a) option = None | Some of 'a

and Haskell defines like this:

data Maybe a = Nothing | Just a

That is, instances of this type are either an instance of 'a (this can be any type), wrapped up in a Some or Just box, or they are a separate value representing a failure. This is sort of like working with a set or a list guaranteed to be either singleton or empty.

In one of the homework meetings, Chris posed the challenge: you know those dividers they use in checkout lines to separate your purchases from the next person's? What if you wanted to buy one of those dividers? How could they tell whether it belonged to your purchases or was separating them from others?

The OCaml and Haskell solution is to use not supermarket dividers but instead those gray bins from airport security. If you want to buy something, it goes into a bin. (OCaml's Some, Haskell's Just). If you want to separate your stuff from the next person, you send an empty bin (OCaml's None, Haskell's Nothing). If you happen to be buying a bin, OK, you put that into a bin. In OCaml it'd be Some None (or Some (Some stuff) if the bin you're buying itself contains some stuff); in Haskell Just Nothing. This way, we can't confuse a bin that contains a bin with an empty bin. (Not even if the contained bin is itself empty.)

1. Your first problem is to write a maybe_map function for these types. Here is the type of the function you should write:

   (* OCaml *)
   maybe_map : ('a -> 'b) -> ('a) option -> ('b) option
   
   -- Haskell
   maybe_map :: (a -> b) -> Maybe a -> Maybe b
   

   If your maybe_map function is given a None or Nothing as its second argument, that should be what it returns. Otherwise, it should apply the function it got as its first argument to the contents of the Some or Just bin that it got as its second, and return the result, wrapped back up in a Some or Just. (Yes, we know that the fmap function in Haskell already implements this functionality. Your job is to write it yourself.)

   One way to extract the contents of an option/Maybe value is to pattern match on that value, as you did with lists. In OCaml:

   match m with
   | None -> ...
   | Some y -> ...
   

   In Haskell:

   case m of {
     Nothing -> ...;
     Just y -> ...
   }
   

   Some other tips: In OCaml you write recursive functions using let rec, in Haskell you just use let (it's already assumed to be recursive). In OCaml when you finish typing something and want the interpreter to parse it, check and display its type, and evaluate it, type ;; and then return. In Haskell, if you want to display the type of an expression expr, type :t expr or :i expr.

   You may want to review Rosetta pages 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:

   (* OCaml *)
   maybe_map2 : ('a -> 'b -> 'c) -> ('a) option -> ('b) option -> ('c) option
   
   -- Haskell
   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

(The questions on Color and Search Trees are adapted from homeworks in Chapters 1 and 2 of Friedman and Wand, Essentials of Programming Languages.)

Here are type definitions for one kind of binary tree:

(* OCaml *)
type color = Red | Green | Blue | ... (* you can add as many as you like *)
type ('a) color_tree = Leaf of 'a | Branch of 'a color_tree * color * 'a color_tree

-- Haskell
data Color = Red | Green | Blue | ...  deriving (Eq, Show)
data Color_tree a = Leaf a | Branch (Color_tree a) Color (Color_tree a)  deriving (Show)

These trees always have colors labeling their inner branching nodes, and will have elements of some type 'a labeling their leaves. (int) color_trees will have ints there, (bool) color_trees will have bools there, and so on. The deriving (Eq, Show) part at the end of the Haskell declarations is boilerplate to tell Haskell you want to be able to compare the colors for equality, and also that you want the Haskell interpreter to display colors and trees to you when they are the result of evaluating an expression.

Here's how you create an instance of such a tree:

(* OCaml *)
let t1 = Branch (Leaf 1, Red, Branch (Leaf 2, Green, Leaf 0))

-- Haskell
let t1 = Branch (Leaf 1) Red (Branch (Leaf 2) Green (Leaf 0))

Here's how you pattern match such a tree, binding variables to its components:

(* OCaml *)
match t with
| Leaf n -> false
| Branch (_, col, _) -> col = Red

-- Haskell
case t of {
  Leaf n -> False;
  Branch _ col _ -> col == Red
}

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

Notice that for equality, you should use single = in OCaml and double == in Haskell. (Double == in OCaml will often give the same results, but it is subtly different in ways we're not yet in a position to explain.) Inequality is expressed as <> in OCaml and /= in Haskell.

Choose one of these languages and write the following functions.

1. 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
   

   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

2. 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
   

   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.) 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.

3. 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

4. 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

5. 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, if you need one.)

   HERE IS A DIRECT OCAML ANSWER, FOLLOWING the hint:

   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)
   

6. (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:

       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   2
   

   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
   

7. (More challenging.) Assume you have a color_tree whose leaves are labeled with ints (which may be negative). For this problem, assume also that no color labels multiple Branchs (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 -> (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
         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 ints. Additionally, assume that all the ints in branches descending to the left from a given node will be less than the int of that parent node, and all the ints 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.

1. 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 we encountered map2 for lists. There are in fact several different approaches to mapping two lists together.

1. 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'
   

2. 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.

3. 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  9

could 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 7

1. 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/Maybes, 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/Maybes 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/Maybes, 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.)

1. 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
   

1. 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 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.

1. 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 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:

Nat ≡ ∀α. (α -> α) -> α -> α
zero ≡ Λα. λs:α -> α. λz:α. z
succ ≡ λn:Nat. Λα. λs:α -> α. λz:α. s (n [α] s z)

A number n is defined 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 α.

1. 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_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:

(* 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 Nats, 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_ω. System F can already define a more polymorphic list type:

list ≡ ∀τ. ∀α. (τ -> α -> α) -> α -> α

But this is more awkward to work with, because for functions like map we want to give them not just the type:

(T -> S) -> list -> list

but more specifically, the type:

(T -> S) -> list [T] -> list [S]

Yet we haven't given ourselves the capacity to talk about list [S] and so on as a type in System F. Hence, I'll just use the more clumsy, ad hoc specification of map's type as:

(T -> S) -> list_T -> list_S

Update: Never mind, don't bother with the next three questions. They proved to be more difficult to implement in OCaml than we expected. Here is some explanation.

1. Convert this list encoding and the map function to OCaml or Haskell. Again, call the type sysf_list, and the functions sysf_nil, sysf_cons, and sysf_map, to avoid collision with the names for native lists and functions in these languages. (In OCaml and Haskell you can say ('t) sysf_list or Sysf_list t.)

2. Also give us the type and definition for a sysf_head function. Think about what value to give back if its argument is the empty list. It might be cleanest to use the option/Maybe technique explored in questions 1--2, but for this assignment, just pick a strategy, no matter how clunky.

3. Modify your implementation of the predecessor function for Church numerals, above, to implement a sysf_tail function for your lists.

Be sure to test your proposals with simple lists. (You'll have to sysf_cons up a few sample lists yourself; don't expect OCaml or Haskell to magically translate between their native lists and the ones you've just defined.)

More on Types

1. 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:

   # let k (y:'a) (n:'b) = y ;;
   val k : 'a -> 'b -> 'a = [fun]
   # k 1 true ;;
   - : int = 1
   

   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

Do these last three problems specifically with OCaml in mind, not Haskell. Analogues of the questions exist in Haskell, but because the default evaluation rules for these languages are different, it's too complicated to look at how these questions should be translated into the Haskell setting.

1. 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?

   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.

2. Throughout this problem, assume that we have:

   let rec blackhole x = blackhole x
   

   All of the following are well-typed. Which ones terminate? What generalizations can you make?

   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.

3. 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. The idea is to define an if ... then ... else ... expression using other expression types. So assume that yes is any (possibly complex) OCaml expression, and no is any other OCaml expression (of the same type as yes!), and that bool is any boolean expression. Then we can try the following: if bool then yes else no should be equivalent to

     let b = bool in
     let y = yes in
     let n = no in
     match b with true -> y | false -> n
   

   This almost works. For instance,

     if true then 1 else 2
   

   evaluates to 1, and

     let b = true in let y = 1 in let n = 2 in
     match b with true -> y | false -> n
   

   also evaluates to 1. Likewise,

     if false then 1 else 2
   

   and

     let b = false in let y = 1 in let n = 2 in
     match b with true -> y | false -> n
   

   both evaluate to 2.

   However,

     let rec blackhole x = blackhole x in
     if true then blackhole else blackhole ()
   

   terminates, but

     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
   

   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.

   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 ().