fix another typo on ski_evaluator
[lambda.git] / exercises / assignment5_answers.mdwn
1 <!-- λ Λ ∀ ≡ α β ω Ω -->
2
3
4 ## Option / Maybe Types ##
5
6 You've already (in [[assignment1]] and [[/topics/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:
7
8     type ('a) option = None | Some of 'a
9
10 and Haskell defines like this:
11
12     data Maybe a = Nothing | Just a
13
14 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.
15
16 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?
17
18 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.)
19
20 1.  Your first problem is to write a `maybe_map` function for these types. Here is the type of the function you should write:
21
22         (* OCaml *)
23         maybe_map : ('a -> 'b) -> ('a) option -> ('b) option
24
25         -- Haskell
26         maybe_map :: (a -> b) -> Maybe a -> Maybe b
27
28     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.)
29
30     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:
31
32         match m with
33         | None -> ...
34         | Some y -> ...
35
36     In Haskell:
37
38         case m of {
39           Nothing -> ...;
40           Just y -> ...
41         }
42
43     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`.
44
45     You may want to review [[Rosetta pages|/rosetta1]] and also read some of the tutorials we linked to for [[/learning OCaml]] or [[/learning Haskell]].
46
47     HERE IS AN OCAML ANSWER:
48
49         let maybe_map (f: 'a -> 'b) -> (u : 'a option) : 'b option =
50           match u with
51           | Some a -> Some (f a)
52           | None -> None
53
54
55 2.  Next write a `maybe_map2` function. Its type should be:
56
57         (* OCaml *)
58         maybe_map2 : ('a -> 'b -> 'c) -> ('a) option -> ('b) option -> ('c) option
59
60         -- Haskell
61         maybe_map2 :: (a -> b -> c) -> Maybe a -> Maybe b -> Maybe c
62
63
64     HERE IS AN OCAML ANSWER:
65
66         let maybe_map2 (f : 'a -> 'b -> 'c) (u : 'a option) (v : 'b option) : 'c option =
67           match (u, v) with
68           | Some a, Some b -> Some (f a b)
69           | None, _ -> None
70           | _, None -> None
71
72
73
74 ## Color Trees ##
75
76 (The questions on Color and Search Trees are adapted from homeworks in Chapters 1 and 2 of Friedman and Wand, *Essentials of Programming Languages*.)
77
78 Here are type definitions for one kind of binary tree:
79
80     (* OCaml *)
81     type color = Red | Green | Blue | ... (* you can add as many as you like *)
82     type ('a) color_tree = Leaf of 'a | Branch of 'a color_tree * color * 'a color_tree
83
84     -- Haskell
85     data Color = Red | Green | Blue | ...  deriving (Eq, Show)
86     data Color_tree a = Leaf a | Branch (Color_tree a) Color (Color_tree a)  deriving (Show)
87
88 These trees always have colors labeling their inner branching nodes, and will have elements of some type `'a` labeling their leaves. `(int) color_tree`s will have `int`s there, `(bool) color_tree`s will have `bool`s 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.
89
90 Here's how you create an instance of such a tree:
91
92     (* OCaml *)
93     let t1 = Branch (Leaf 1, Red, Branch (Leaf 2, Green, Leaf 0))
94
95     -- Haskell
96     let t1 = Branch (Leaf 1) Red (Branch (Leaf 2) Green (Leaf 0))
97
98 Here's how you pattern match such a tree, binding variables to its components:
99
100     (* OCaml *)
101     match t with
102     | Leaf n -> false
103     | Branch (_, col, _) -> col = Red
104
105     -- Haskell
106     case t of {
107       Leaf n -> False;
108       Branch _ col _ -> col == Red
109     }
110
111 These expressions query whether `t` is a branching `color_tree` (that is, not a leaf) whose root is labeled `Red`.
112
113 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.) *In*equality is expressed as `<>` in OCaml and `/=` in Haskell.
114
115 Choose one of these languages and write the following functions.
116
117
118 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.
119
120     HERE IS A DIRECT OCAML ANSWER:
121
122         let rec tree_map (f: 'a -> 'b) (t: 'a color_tree) : 'b color_tree =
123           match t with
124           | Leaf a -> Leaf (f a)
125           | Branch (l,col,r) ->
126               let l' = tree_map f l in
127               let r' = tree_map f r in
128               Branch(l', col, r')
129
130     IT MIGHT BE USEFUL TO GENERALIZE THIS PATTERN, LIKE SO:
131
132         let rec tree_walker (leaf_handler: 'a -> 'h) (joiner : 'h -> color -> 'h -> 'h) (t: 'a color_tree) : 'h =
133           match t with
134           | Leaf a -> leaf_handler a
135           | Branch (l,col,r) ->
136               let lh = tree_walker leaf_handler joiner l in
137               let rh = tree_walker leaf_handler joiner r in
138               joiner lh col rh
139
140     <!-- traverse (k: a-> Mb) t = Leaf a -> map Leaf (k a) | Branch(l,col,r) -> map3 Branch l' c' r' -->
141
142     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`
143
144
145 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.
146
147     HERE IS A DIRECT OCAML ANSWER:
148
149         let rec tree_foldleft (g: 'z -> 'a -> 'z) (z : 'z) (t: 'a color_tree) : 'z =
150           match t with
151           | Leaf a -> g z a
152           | Branch (l,_,r) ->
153               let z' = tree_foldleft g z l in
154               let z'' = tree_foldleft g z' r in
155               r''
156
157     HERE IS AN ANSWER THAT RE-USES OUR `tree_walker` FUNCTION FROM THE PREVIOUS ANSWER:
158
159         let tree_foldleft g z t =
160           let leaf_handler a = fun z -> g z a in
161           let joiner lh _ rh = fun z -> rh (lh z) in
162           let expects_z = tree_walker leaf_handler joiner t in
163           expects_z z
164
165     <!-- traverse (k: a-> Mb) t = Leaf a -> map Leaf (k a) | Branch(l,col,r) -> map3 Branch l' c' r' -->
166     <!-- linearize (f: a->Mon) t = Leaf a -> f a | Branch(l,col,r) -> l' && [col' &&] r' -->
167
168     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.
169
170
171 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`?
172
173     ANSWER: `tree_foldleft (fun z a -> z + a) 0 your_tree`
174
175 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.)
176
177     ANSWER: `tree_foldleft (fun z a -> a :: z) [] your_tree`
178
179 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.)
180
181     HERE IS A DIRECT OCAML ANSWER, FOLLOWING [[the hint|assignment5_hint3]]:
182
183         let rec enumerate_from (t:'a color_tree) counter =
184           match t with
185           | Leaf x -> (Leaf counter, counter+1)
186           | Branch (left,col,right) -> let (left',counter') = enumerate_from left counter in
187                                        let (right',counter'') = enumerate_from right counter' in
188                                        (Branch (left',col,right'), counter'')
189
190         (* then this will be the function we were asked for *)
191         let enumerate t =
192           let (t', _) = enumerate_from t 0 in
193           t'
194
195     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`:
196
197         let enumerate t =
198           let leaf_handler a = fun counter -> (Leaf counter, counter+1) in
199           let joiner lh col rh =
200             fun counter ->
201               let (left',counter') = lh counter in
202               let (right',counter'') = rh counter' in
203               (Branch (left',col,right'), counter'') in
204           fst (tree_walker leaf_handler joiner t 0)
205
206
207 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:
208
209     <pre>
210         Red
211         / \
212       Blue \
213       / \  Green
214      a   b  / \
215            c   Red
216                / \
217               d   e
218     </pre>
219
220     (for any leaf values `a` through `e`), it should return:
221
222     <pre>
223         Red
224         / \
225       Blue \
226       / \  Green
227      1   1  / \
228            1   Red
229                / \
230               2   2
231     </pre>
232
233     HERE IS A DIRECT OCAML SOLUTION:
234
235         let rec tree_red_ancestors_from (cur : int) (t : 'a tree) : int tree =
236           match t with
237           | Leaf a -> Leaf cur
238           | Branch(l, col, r) ->
239               let cur' = if col = Red then cur + 1 else cur in
240               let l' = tree_red_ancestors_from cur' l in
241               let r' = tree_red_ancestors_from cur' r in
242               Branch(l',col,r')
243
244         (* here is the function we were asked for *)
245         let tree_red_ancestors t = tree_red_ancestors_from 0 t
246
247
248     HERE IS HOW TO DO IT USING `tree_walker`:
249
250         let tree_red_ancestors t =
251           let leaf_handler a = fun cur -> Leaf cur in
252           let joiner lh col rh = fun cur ->
253             let cur' = if col = Red then cur + 1 else cur in
254             Branch(lh cur', col, rh cur') in
255           tree_walker leaf_handler joiner t 0
256
257
258 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.
259
260     HERE IS A DIRECT OCAML SOLUTION:
261
262         type maybe_leader = (color * int) option
263
264         let rec tree_best_sofar (t : 'a color_tree) (lead : maybe_leader) : maybe_leader * int =
265           match t with
266           | Leaf a -> (lead, a)
267           | Branch(l, col, r) ->
268               let (lead',left_score) = tree_best_sofar l lead in
269               let (lead'',right_score) = tree_best_sofar r lead' in
270               let my_score = left_score + right_score in
271               (match lead'' with
272               | None -> Some(col,my_score), my_score
273               | Some(_, lead_score) -> (if my_score > lead_score then Some(col,my_score) else lead''), my_score)
274
275         (* Note that the invocations of that function have to return who-is-the-current-leader?
276            plus their OWN score, even if they are not the current leader. Their parents need the
277            second value to calculate whether they should become the current leader. *)
278
279         (* here is the function we were asked for *)
280         let tree_best t =
281           match tree_best_sofar t None with
282           | Some(leader,leader_score), _ -> leader
283           | None, _ -> failwith "no colors"
284
285
286     HERE IS HOW TO DO IT USING `tree_walker`:
287
288         let tree_best_sofar t =
289           let leaf_handler a = fun leader -> leader, a in
290           let joiner lh col rh = fun leader ->
291             let (leader',left_score) = lh leader in
292             let (leader'',right_score) = rh leader' in
293             let my_score = left_score + right_score in
294             (match leader'' with
295             | None -> Some(col,my_score), my_score
296             | Some(_,leader_score) -> (if my_score > leader_score then Some(col,my_score) else leader''), my_score) in
297           tree_walker leaf_handler joiner t
298
299     Then `tree_best` could be defined as in the direct answer.
300
301
302 ## Search Trees ##
303
304 (More challenging.) For the next problem, assume the following type definition:
305
306     (* OCaml *)
307     type search_tree = Nil | Inner of search_tree * int * search_tree
308
309     -- Haskell
310     data Search_tree = Nil | Inner Search_tree Int Search_tree  deriving (Show)
311
312 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.
313
314 10. Write a function `search_for` with the following type, as displayed by OCaml:
315
316         type direction = Left | Right
317         search_for : int -> search_tree -> direction list option
318
319     Haskell would say instead:
320
321         data Direction = Left | Right  deriving (Eq, Show)
322         search_for :: Int -> Search_tree -> Maybe [Direction]
323
324     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]`.
325
326     HERE IS AN OCAML ANSWER:
327
328         let search_for (sought : int) (t : search_tree) : direction list option =
329           let rec aux (trace : direction list) t =
330             match t with
331             | Nil -> None
332             | Inner(l,x,r) when sought < x -> aux (Left::trace) l
333             | Inner(l,x,r) when sought > x -> aux (Right::trace) r
334             | _ -> Some(List.rev trace) in
335         aux [] t
336
337
338 ## More Map2s ##
339
340 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.
341
342 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:
343
344         (* OCaml *)
345         map2_zip : ('a -> 'b -> 'c) -> ('a) list -> ('b) list -> ('c) list
346
347     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:
348
349         :set -XParallelListComp
350         [ f x y | x <- xs | y <- ys ]
351
352     <!-- or `f <$/fmap> ZipList xs <*/ap> ZipList ys`; or `pure f <*> ...`; or `liftA2 f (ZipList xs) (ZipList ys)` -->
353     But we want you to write this function from scratch.)
354
355     HERE IS AN OCAML ANSWER:
356
357         let rec map2_zip f xs ys =
358           match xs, ys with
359           | [], _ -> []
360           | _, [] -> []
361           | x'::xs', y'::ys' -> f x' y' :: map2_zip f xs' ys'
362
363 12. What is the relation between the function you just wrote, and the `maybe_map2` function you wrote for problem 2, above?
364
365     ANSWER: option/Maybe types are like lists constrained to be of length 0 or 1.
366
367 13. Another strategy is to take the *cross product* of the two lists. If the function:
368
369         (* OCaml *)
370         map2_cross : ('a -> 'b -> 'c) -> ('a) list -> ('b) list -> ('c) list
371
372     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.
373     <!-- in Haskell, `liftA2 f xs ys` -->
374
375     HERE IS AN OCAML ANSWER:
376
377         let rec map2_cross f xs ys =
378           match xs with
379           | [] -> []
380           | x'::xs' -> List.append (List.map (f x') ys) (map2_cross f xs' ys)
381
382 A similar choice between "zipping" and "crossing" could be made when `map2`-ing two trees. For example, the trees:
383
384 <pre>
385     0       5
386    / \     / \
387   1   2   6   7
388  / \         / \
389  3  4        8  9
390 </pre>
391
392 could be "zipped" like this (ignoring any parts of branches on the one tree that extend farther than the corresponding branch on the other):
393
394 <pre>
395    f 0 5
396    /    \
397 f 1 6  f 2 7
398 </pre>
399
400 14. You can try defining that if you like, for extra credit.
401
402 "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.
403
404 *   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.
405
406 *   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.
407
408 *   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.
409     (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.)
410
411 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.
412
413
414
415
416
417 ## Untyped Lambda Terms ##
418
419 In OCaml, you can define some datatypes that represent terms in the untyped Lambda Calculus like this:
420
421     type identifier = string
422     type lambda_term = Var of identifier | Abstract of identifier * _____ | App of _____
423
424 We've left some gaps.
425
426 In Haskell, you'd define it instead like this:
427
428     type Identifier = String
429     data Lambda_term = Var Identifier | Abstract Identifier _____ | App ________  deriving (Show)
430
431 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.)
432
433 15. Choose one of these languages and fill in the gaps to complete the definition.
434
435     HERE IS AN OCAML DEFINITION:
436
437         type lambda_term = Var of identifier | Abstract of identifier * lambda_term | App of lambda_term * lambda_term
438
439 <a id="occurs_free"></a>
440
441 16. Write a function `occurs_free` that has the following type:
442
443         occurs_free : identifier -> lambda_term -> bool
444
445     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`.
446
447     HERE IS AN OCAML ANSWER:
448
449         let rec occurs_free (ident : identifier) (term : lambda_term) : bool =
450           match term with
451           | Var var_ident -> ident = var_ident (* `x` is free in Var "x" but not in Var "y" *)
452           | 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 *)
453           | App (head, arg) -> occurs_free ident head || occurs_free ident arg
454
455   
456
457 ## Encoding Booleans, Church numerals, and Right-Fold Lists in System F ##
458
459 <!-- These questions are adapted from web materials by Umut Acar. Were at <http://www.mpi-sws.org/~umut/>. Now he's moved to <http://www.umut-acar.org/> and I can't find the page anymore. -->
460
461 (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.)
462
463
464 Let's think about the encodings of booleans, numerals and lists in System F,
465 and get datatypes with the same form working in OCaml or Haskell. (Of course, OCaml and Haskell
466 have *native* versions of these types: OCaml's `true`, `1`, and `[1;2;3]`.
467 But the point of our exercise requires that we ignore those.)
468
469 Recall from class System F, or the polymorphic λ-calculus, with this grammar:
470
471     types ::= constants | α ... | type1 -> type2 | ∀α. type
472     expressions ::= x ... | λx:type. expr | expr1 expr2 | Λα. expr | expr [type]
473
474 The boolean type, and its two values, may be encoded as follows:
475
476     Bool ≡ ∀α. α -> α -> α
477     true ≡ Λα. λy:α. λn:α. y
478     false ≡ Λα. λy:α. λn:α. n
479
480 It's used like this:
481
482     b [T] res1 res2
483
484 where `b` is a `Bool` value, and `T` is the shared type of `res1` and `res2`.
485
486
487 17. How should we implement the following terms? Note that the result
488 of applying them to the appropriate arguments should also give us a term of
489 type `Bool`.
490
491     (a) the term `not` that takes an argument of type `Bool` and computes its negation  
492     (b) the term `and` that takes two arguments of type `Bool` and computes their conjunction  
493     (c) the term `or` that takes two arguments of type `Bool` and computes their disjunction
494
495     ANSWERS:
496
497         Bool ≡ ∀α. α -> α -> α
498         true ≡ Λα. λy:α. λn:α. y
499         false ≡ Λα. λy:α. λn:α. n
500         not ≡ λp:Bool. p [Bool] false true
501         and ≡ λp:Bool. λq:Bool. p [Bool] q false
502         or ≡ λp:Bool. λq:Bool. p [Bool] true q
503
504     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,
505     this isn't necessary, because `q` is already a `Bool`. But as I learned by checking these answers with Pierce's evaluator, it's
506     also a mistake. What we want is a result whose type _is_ `Bool`, that is, `∀α. α -> α -> α`. `(q [Bool])` doesn't have that type, but
507     rather the type `Bool -> Bool -> Bool`. The first, desired, type has an outermost `∀`. The second, wrong type doesn't; it only has `∀`s
508     inside the antecedents and consequents of the various arrows. The last one of those could be promoted to be an outermost `∀`, since
509     `P -> ∀α. Q` is equivalent to `∀α. P -> Q` when `α` is not free in `P`. But that couldn't be done with the others.
510
511
512 The type `Nat` (for "natural number") may be encoded as follows:
513
514     Nat ≡ ∀α. (α -> α) -> α -> α
515     zero ≡ Λα. λs:α -> α. λz:α. z
516     succ ≡ λn:Nat. Λα. λs:α -> α. λz:α. s (n [α] s z)
517
518 A number `n` is defined by what it can do, which is to compute a function iterated `n`
519 times. In the polymorphic encoding above, the result of that iteration can be
520 any type `α`, as long as your function is of type `α -> α` and you have a base element of type `α`.
521
522
523 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.
524
525     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.
526
527     To get you started, here is how to define `sysf_bool` and `sysf_true` in OCaml:
528
529         type ('a) sysf_bool = 'a -> 'a -> 'a
530         let sysf_true : ('a) sysf_bool = fun y n -> y
531
532     And here in Haskell:
533
534         type Sysf_bool a = a -> a -> a  -- this is another case where Haskell uses `type` instead of `data`
535         -- To my mind the natural thing to write next would be:
536         let sysf_true :: Sysf_bool a = \y n -> y
537         -- But for complicated reasons, that won't work, and you need to do this instead:
538         let { sysf_true :: Sysf_bool a; sysf_true = \y n -> y }
539         -- Or this:
540         let sysf_true = (\y n -> y) :: Sysf_bool a
541
542     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:
543
544         :set -XExplicitForAll
545         let { sysf_true :: forall a. Sysf_bool a; ... }
546         -- or
547         let { sysf_true :: forall a. a -> a -> a; ... }
548
549     You can't however, put a `forall a.` in the `type Sysf_bool ...` declaration. The reasons for this are too complicated to explain here.
550
551     Note also that `sysf_true` can be applied to further arguments directly:
552
553         sysf_true 10 20
554
555     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.
556
557     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]].
558
559
560     OCAML ANSWERS:
561
562         type 'a sysf_bool = 'a -> 'a -> 'a
563         let sysf_true : 'a sysf_bool = fun y n -> y
564         let sysf_false : 'a sysf_bool = fun y n -> n
565
566         type 'a sysf_nat = ('a -> 'a) -> 'a -> 'a
567         let sysf_zero : 'a sysf_nat = fun s z -> z
568
569         let sysf_iszero (n : ('a sysf_bool) sysf_nat) : 'a sysf_bool = n (fun _ -> sysf_false) sysf_true
570         (* Annoyingly, though, if you just say sysf_iszero sysf_zero, you'll get an answer that isn't fully polymorphic.
571            This is explained in the comments linked below. The way to get a polymorphic result is to say instead
572            `fun next -> sysf_iszero sysf_zero next`. *)
573
574         let sysf_succ (n : 'a sysf_nat) : 'a sysf_nat = fun s z -> s (n s z)
575         (* Again, to get a polymorphic result you'll want to call `fun next -> sysf_succ sysf_zero next` *)
576
577     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.)
578
579         type 'a natpair = ('a nat -> 'a nat -> 'a nat) -> 'a nat
580         let natpair (x : 'a nat) (y : 'a nat) : 'a natpair = fun f -> f x y
581         let fst x y = x
582         let snd x y = y
583         let shift (p : 'a natpair) : 'a natpair = natpair (succ (p fst)) (p fst)
584         let pred (n : ('a natpair) nat) : 'a nat = n shift (natpair zero zero) snd
585
586         (* As before, to get polymorphic results you need to eta-expand your applications. Witness:
587           # let one = succ zero;;
588           val one : '_a nat = <fun>
589           # let one next = succ zero next;;
590           val one : ('a -> 'a) -> 'a -> 'a = <fun>
591           # let two = succ one;;
592           val two : '_a nat = <fun>
593           # let two next = succ one next;;
594           val two : ('a -> 'a) -> 'a -> 'a = <fun>
595           # pred two;;
596           - : '_a nat = <fun>
597           # fun next -> pred two next;;
598           - : ('a -> 'a) -> 'a -> 'a = <fun>
599         *)
600
601 Consider the following list type, specified using OCaml or Haskell datatypes:
602
603     (* OCaml *)
604     type ('t) my_list = Nil | Cons of 't * 't my_list
605
606      -- Haskell
607      data My_list t = Nil | Cons t (My_list t)  deriving (Show)
608
609 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:
610
611     list_T ≡ ∀α. (T -> α -> α) -> α -> α
612     nil_T ≡ Λα. λc:T -> α -> α. λn:α. n
613     cons_T ≡ λx:T. λxs:list_T. Λα. λc:T -> α -> α. λn:α. c x (xs [α] c n)
614
615 As with `Nat`s, the natural recursion on the type is built into our encoding of it.
616
617 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<sub>ω</sub>. System F *can* already define a more polymorphic list type:
618
619     list ≡ ∀τ. ∀α. (τ -> α -> α) -> α -> α
620
621 But this is more awkward to work with, because for functions like `map` we want to give them not just the type:
622
623     (T -> S) -> list -> list
624
625 but more specifically, the type:
626
627     (T -> S) -> list [T] -> list [S]
628
629 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:
630
631     (T -> S) -> list_T -> list_S
632
633 <!--
634     = λf:T -> S. λxs:list. xs [T] [list [S]] (λx:T. λys:list [S]. cons [S] (f x) ys) (nil [S])
635 -->
636
637 *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|assignment5 hint4]].*
638
639 19. 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`.)
640
641 20. 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. 
642
643 21. Modify your implementation of the predecessor function for Church numerals, above, to implement a `sysf_tail` function for your lists.
644
645 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.)
646
647
648
649
650
651 ## More on Types ##
652
653 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**:
654
655         # let k (y:'a) (n:'b) = y ;;
656         val k : 'a -> 'b -> 'a = [fun]
657         # k 1 true ;;
658         - : int = 1
659
660     If you can't understand how one term can have several types, recall our discussion in this week's notes of "principal types". 
661
662     ANSWER: OCaml shows the principal typing for S as follows:
663
664         # let s = fun f g x -> f x (g x);;
665         val s : ('a -> 'b -> 'c) -> ('a -> 'b) -> 'a -> 'c = <fun>
666
667     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:
668
669         # let s' = (s : ('a -> 'b -> 'a) -> ('a -> 'b) -> 'a -> 'a);;
670         val s' : ('a -> 'b -> 'a) -> ('a -> 'b) -> 'a -> 'a = <fun>
671
672
673 ## Evaluation Order ##
674
675 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.
676
677
678 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?
679
680         a. let rec f x = f x
681         b. let rec f x = f f
682         c. let rec f x = f x in f f
683         d. let rec f x = f x in f ()
684         e. let rec f () = f f
685         f. let rec f () = f ()
686         g. let rec f () = f () in f f
687         h. let rec f () = f () in f ()
688
689     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.
690
691     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:
692
693         type 'a ok = Cons of ('a -> 'a ok)
694
695     But this is not:
696
697         type 'a notok = 'a -> 'a notok
698
699     (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.
700
701     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.
702     
703
704 24.  Throughout this problem, assume that we have:
705
706         let rec blackhole x = blackhole x
707
708     <!-- Haskell could say: `let blackhole = \x -> fix (\f -> f)` -->
709     All of the following are well-typed. Which ones terminate?  What generalizations can you make?
710
711         a. blackhole
712         b. blackhole ()
713         c. fun () -> blackhole ()
714         d. (fun () -> blackhole ()) ()
715         e. if true then blackhole else blackhole
716         f. if false then blackhole else blackhole
717         g. if true then blackhole else blackhole ()
718         h. if false then blackhole else blackhole ()
719         i. if true then blackhole () else blackhole
720         j. if false then blackhole () else blackhole
721         k. if true then blackhole () else blackhole ()
722         l. if false then blackhole () else blackhole ()
723         m. let _ = blackhole in 2
724         n. let _ = blackhole () in 2
725
726     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.
727
728 25.  This problem aims to get you thinking about how to control order of evaluation.
729 Here is an attempt to make explicit the behavior of `if ... then ... else ...` explored in the previous question.
730 The idea is to define an `if ... then ... else ...` expression using
731 other expression types.  So assume that `yes` is any (possibly complex) OCaml expression,
732 and `no` is any other OCaml expression (of the same type as `yes`!),
733 and that `bool` is any boolean expression.  Then we can try the following:
734 `if bool then yes else no` should be equivalent to
735
736         let b = bool in
737         let y = yes in
738         let n = no in
739         match b with true -> y | false -> n
740
741     This almost works.  For instance,
742
743         if true then 1 else 2
744
745     evaluates to `1`, and
746
747         let b = true in let y = 1 in let n = 2 in
748         match b with true -> y | false -> n
749
750     also evaluates to `1`.  Likewise,
751
752         if false then 1 else 2
753
754     and
755
756         let b = false in let y = 1 in let n = 2 in
757         match b with true -> y | false -> n
758
759     both evaluate to `2`.
760
761     However,
762
763         let rec blackhole x = blackhole x in
764         if true then blackhole else blackhole ()
765
766     terminates, but
767
768         let rec blackhole x = blackhole x in
769         let b = true in
770         let y = blackhole in
771         let n = blackhole () in
772         match b with true -> y | false -> n
773
774     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.
775
776     Here's a [[hint|assignment5 hint1]].
777
778     ANSWER:
779
780         let rec blackhole x = blackhole x in
781         let b = true in
782         let y () = blackhole in
783         let n () = blackhole () in
784         (match b with true -> y | false -> n) ()
785
786     If you said instead, on the last line:
787
788         match b with true -> y () | false -> n ()
789
790     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.
791
792     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 ()`.