fix another typo on ski_evaluator
[lambda.git] / exercises / assignment5.mdwn
1 <!-- λ Λ ∀ ≡ α β ω Ω -->
2
3 This is a long and substantial assignment. On the one hand, it doesn't have any stumpers like we gave you in past weeks, such as defining `pred` or mutual recursion. (Well, we *do* ask you to define `pred` again, but now you understand a basic strategy for doing so, so it's no longer a stumper.) On the other hand, there are a bunch of problems; many of them demand a modest amount of time; and this week you're coming to terms with both System F *and* with OCaml or Haskell. So it's a lot to do.
4
5 The upside is that there won't be any new homework assigned this week, and you can take longer to complete this assignment if you need to. As always, don't get stuck on the "More challenging" questions if you find them too hard. Be sure to send us your work even if it's not entirely completed, so we can see where you are. And consult with us (over email or in person on Wednesday) about things you don't understand, especially issues you're having working with OCaml or Haskell, or with translating between System F and them. We will update this homework page with clarifications or explanations that your questions prompt.
6
7 We will also be assigning some philosophy of language readings for you to look at before this Thursday's seminar meeting.
8
9 Those, and lecture notes from this past week, will be posted shortly.
10
11
12
13 ## Option / Maybe Types ##
14
15 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:
16
17     type ('a) option = None | Some of 'a
18
19 and Haskell defines like this:
20
21     data Maybe a = Nothing | Just a
22
23 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.
24
25 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?
26
27 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.)
28
29 1.  Your first problem is to write a `maybe_map` function for these types. Here is the type of the function you should write:
30
31         (* OCaml *)
32         maybe_map : ('a -> 'b) -> ('a) option -> ('b) option
33
34         -- Haskell
35         maybe_map :: (a -> b) -> Maybe a -> Maybe b
36
37     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.)
38
39     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:
40
41         match m with
42         | None -> ...
43         | Some y -> ...
44
45     In Haskell:
46
47         case m of {
48           Nothing -> ...;
49           Just y -> ...
50         }
51
52     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`.
53
54     You may want to review [[Rosetta pages|/rosetta1]] and also read some of the tutorials we linked to for [[/learning OCaml]] or [[/learning Haskell]].
55
56
57 2.  Next write a `maybe_map2` function. Its type should be:
58
59         (* OCaml *)
60         maybe_map2 : ('a -> 'b -> 'c) -> ('a) option -> ('b) option -> ('c) option
61
62         -- Haskell
63         maybe_map2 :: (a -> b -> c) -> Maybe a -> Maybe b -> Maybe c
64
65
66
67 ## Color Trees ##
68
69 (The questions on Color and Search Trees are adapted from homeworks in Chapters 1 and 2 of Friedman and Wand, *Essentials of Programming Languages*.)
70
71 Here are type definitions for one kind of binary tree:
72
73     (* OCaml *)
74     type color = Red | Green | Blue | ... (* you can add as many as you like *)
75     type ('a) color_tree = Leaf of 'a | Branch of 'a color_tree * color * 'a color_tree
76
77     -- Haskell
78     data Color = Red | Green | Blue | ...  deriving (Eq, Show)
79     data Color_tree a = Leaf a | Branch (Color_tree a) Color (Color_tree a)  deriving (Show)
80
81 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.
82
83 Here's how you create an instance of such a tree:
84
85     (* OCaml *)
86     let t1 = Branch (Leaf 1, Red, Branch (Leaf 2, Green, Leaf 0))
87
88     -- Haskell
89     let t1 = Branch (Leaf 1) Red (Branch (Leaf 2) Green (Leaf 0))
90
91 Here's how you pattern match such a tree, binding variables to its components:
92
93     (* OCaml *)
94     match t with
95     | Leaf n -> false
96     | Branch (_, c, _) -> c = Red
97
98     -- Haskell
99     case t of {
100       Leaf n -> False;
101       Branch _ c _ -> c == Red
102     }
103
104 These expressions query whether `t` is a branching `color_tree` (that is, not a leaf) whose root is labeled `Red`.
105
106 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.
107
108 Choose one of these languages and write the following functions.
109
110
111 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.
112
113 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.
114
115 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`?
116
117 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.)
118
119 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.)
120
121 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:
122
123     <pre>
124         Red
125         / \
126       Blue \
127       / \  Green
128      a   b  / \
129            c   Red
130                / \
131               d   e
132     </pre>
133
134     (for any leaf values `a` through `e`), it should return:
135
136     <pre>
137         Red
138         / \
139       Blue \
140       / \  Green
141      1   1  / \
142            1   Red
143                / \
144               2   2
145     </pre>
146
147 9.  (More challenging.) Assume you have a `color_tree` whose leaves are labeled with `int`s (which may be negative). For this problem, assume also that no color labels multiple `Branch`s (non-leaf nodes). Write a recursive function that reports which color has the greatest "score" when you sum up all the values of its descendent leaves. Since some leaves may have negative values, the answer won't always be the color at the tree root. In the case of ties, you can return whichever of the highest scoring colors you like.
148
149
150 ## Search Trees ##
151
152 (More challenging.) For the next problem, assume the following type definition:
153
154     (* OCaml *)
155     type search_tree = Nil | Inner of search_tree * int * search_tree
156
157     -- Haskell
158     data Search_tree = Nil | Inner Search_tree Int Search_tree  deriving (Show)
159
160 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.
161
162 10. Write a function `search_for` with the following type, as displayed by OCaml:
163
164         type direction = Left | Right
165         search_for : int -> search_tree -> direction list option
166
167     Haskell would say instead:
168
169         data Direction = Left | Right  deriving (Eq, Show)
170         search_for :: Int -> Search_tree -> Maybe [Direction]
171
172     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]`.
173
174
175 ## More Map2s ##
176
177 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.
178
179 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:
180
181         (* OCaml *)
182         map2_zip : ('a -> 'b -> 'c) -> ('a) list -> ('b) list -> ('c) list
183
184     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:
185
186         :set -XParallelListComp
187         [ f x y | x <- xs | y <- ys ]
188
189     <!-- or `f <$/fmap> ZipList xs <*/ap> ZipList ys`; or `pure f <*> ...`; or `liftA2 f (ZipList xs) (ZipList ys)` -->
190     But we want you to write this function from scratch.)
191
192 12. What is the relation between the function you just wrote, and the `maybe_map2` function you wrote for problem 2, above?
193
194 13. Another strategy is to take the *cross product* of the two lists. If the function:
195
196         (* OCaml *)
197         map2_cross : ('a -> 'b -> 'c) -> ('a) list -> ('b) list -> ('c) list
198
199     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.
200     <!-- in Haskell, `liftA2 f xs ys` -->
201
202 A similar choice between "zipping" and "crossing" could be made when `map2`-ing two trees. For example, the trees:
203
204 <pre>
205     0       5
206    / \     / \
207   1   2   6   7
208  / \         / \
209  3  4        8  9
210 </pre>
211
212 could be "zipped" like this (ignoring any parts of branches on the one tree that extend farther than the corresponding branch on the other):
213
214 <pre>
215    f 0 5
216    /    \
217 f 1 6  f 2 7
218 </pre>
219
220 14. You can try defining that if you like, for extra credit.
221
222 "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.
223
224 *   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.
225
226 *   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.
227
228 *   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.
229     (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.)
230
231 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.
232
233
234
235
236
237 ## Untyped Lambda Terms ##
238
239 In OCaml, you can define some datatypes that represent terms in the untyped Lambda Calculus like this:
240
241     type identifier = string
242     type lambda_term = Var of identifier | Abstract of identifier * _____ | App of _____
243
244 We've left some gaps.
245
246 In Haskell, you'd define it instead like this:
247
248     type Identifier = String
249     data Lambda_term = Var Identifier | Abstract Identifier _____ | App ________  deriving (Show)
250
251 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.)
252
253 15. Choose one of these languages and fill in the gaps to complete the definition.
254
255 <a id="occurs_free"></a>
256
257 16. Write a function `occurs_free` that has the following type:
258
259         occurs_free : identifier -> lambda_term -> bool
260
261     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`.
262
263
264
265
266 ## Encoding Booleans, Church numerals, and Right-Fold Lists in System F ##
267
268 <!-- 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. -->
269
270 (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.)
271
272
273 Let's think about the encodings of booleans, numerals and lists in System F,
274 and get datatypes with the same form working in OCaml or Haskell. (Of course, OCaml and Haskell
275 have *native* versions of these types: OCaml's `true`, `1`, and `[1;2;3]`.
276 But the point of our exercise requires that we ignore those.)
277
278 Recall from class System F, or the polymorphic λ-calculus, with this grammar:
279
280     types ::= constants | α ... | type1 -> type2 | ∀α. type
281     expressions ::= x ... | λx:type. expr | expr1 expr2 | Λα. expr | expr [type]
282
283 The boolean type, and its two values, may be encoded as follows:
284
285     Bool ≡ ∀α. α -> α -> α
286     true ≡ Λα. λy:α. λn:α. y
287     false ≡ Λα. λy:α. λn:α. n
288
289 It's used like this:
290
291     b [T] res1 res2
292
293 where `b` is a `Bool` value, and `T` is the shared type of `res1` and `res2`.
294
295
296 17. How should we implement the following terms? Note that the result
297 of applying them to the appropriate arguments should also give us a term of
298 type `Bool`.
299
300     (a) the term `not` that takes an argument of type `Bool` and computes its negation  
301     (b) the term `and` that takes two arguments of type `Bool` and computes their conjunction  
302     (c) the term `or` that takes two arguments of type `Bool` and computes their disjunction
303
304 The type `Nat` (for "natural number") may be encoded as follows:
305
306     Nat ≡ ∀α. (α -> α) -> α -> α
307     zero ≡ Λα. λs:α -> α. λz:α. z
308     succ ≡ λn:Nat. Λα. λs:α -> α. λz:α. s (n [α] s z)
309
310 A number `n` is defined by what it can do, which is to compute a function iterated `n`
311 times. In the polymorphic encoding above, the result of that iteration can be
312 any type `α`, as long as your function is of type `α -> α` and you have a base element of type `α`.
313
314
315 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.
316
317     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.
318
319     To get you started, here is how to define `sysf_bool` and `sysf_true` in OCaml:
320
321         type ('a) sysf_bool = 'a -> 'a -> 'a
322         let sysf_true : ('a) sysf_bool = fun y n -> y
323
324     And here in Haskell:
325
326         type Sysf_bool a = a -> a -> a  -- this is another case where Haskell uses `type` instead of `data`
327         -- To my mind the natural thing to write next would be:
328         let sysf_true :: Sysf_bool a = \y n -> y
329         -- But for complicated reasons, that won't work, and you need to do this instead:
330         let { sysf_true :: Sysf_bool a; sysf_true = \y n -> y }
331         -- Or this:
332         let sysf_true = (\y n -> y) :: Sysf_bool a
333
334     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:
335
336         :set -XExplicitForAll
337         let { sysf_true :: forall a. Sysf_bool a; ... }
338         -- or
339         let { sysf_true :: forall a. a -> a -> a; ... }
340
341     You can't however, put a `forall a.` in the `type Sysf_bool ...` declaration. The reasons for this are too complicated to explain here.
342
343     Note also that `sysf_true` can be applied to further arguments directly:
344
345         sysf_true 10 20
346
347     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.
348
349     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]].
350
351
352
353 Consider the following list type, specified using OCaml or Haskell datatypes:
354
355     (* OCaml *)
356     type ('t) my_list = Nil | Cons of 't * 't my_list
357
358      -- Haskell
359      data My_list t = Nil | Cons t (My_list t)  deriving (Show)
360
361 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:
362
363     list_T ≡ ∀α. (T -> α -> α) -> α -> α
364     nil_T ≡ Λα. λc:T -> α -> α. λn:α. n
365     cons_T ≡ λx:T. λxs:list_T. Λα. λc:T -> α -> α. λn:α. c x (xs [α] c n)
366
367 As with `Nat`s, the natural recursion on the type is built into our encoding of it.
368
369 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:
370
371     list ≡ ∀τ. ∀α. (τ -> α -> α) -> α -> α
372
373 But this is more awkward to work with, because for functions like `map` we want to give them not just the type:
374
375     (T -> S) -> list -> list
376
377 but more specifically, the type:
378
379     (T -> S) -> list [T] -> list [S]
380
381 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:
382
383     (T -> S) -> list_T -> list_S
384
385 <!--
386     = λf:T -> S. λxs:list. xs [T] [list [S]] (λx:T. λys:list [S]. cons [S] (f x) ys) (nil [S])
387 -->
388
389 *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]].*
390
391 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`.)
392
393 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. 
394
395 21. Modify your implementation of the predecessor function for Church numerals, above, to implement a `sysf_tail` function for your lists.
396
397 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.)
398
399
400
401
402
403
404 ## More on Types ##
405
406 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**:
407
408         # let k (y:'a) (n:'b) = y ;;
409         val k : 'a -> 'b -> 'a = [fun]
410         # k 1 true ;;
411         - : int = 1
412
413     If you can't understand how one term can have several types, recall our discussion in this week's notes of "principal types". 
414
415
416
417
418 ## Evaluation Order ##
419
420 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.
421
422
423 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?
424
425         let rec f x = f x
426         let rec f x = f f
427         let rec f x = f x in f f
428         let rec f x = f x in f ()
429         let rec f () = f f
430         let rec f () = f ()
431         let rec f () = f () in f f
432         let rec f () = f () in f ()
433
434 24.  Throughout this problem, assume that we have:
435
436         let rec blackhole x = blackhole x
437
438     <!-- Haskell could say: `let blackhole = \x -> fix (\f -> f)` -->
439     All of the following are well-typed. Which ones terminate?  What generalizations can you make?
440
441         blackhole
442         blackhole ()
443         fun () -> blackhole ()
444         (fun () -> blackhole ()) ()
445         if true then blackhole else blackhole
446         if false then blackhole else blackhole
447         if true then blackhole else blackhole ()
448         if false then blackhole else blackhole ()
449         if true then blackhole () else blackhole
450         if false then blackhole () else blackhole
451         if true then blackhole () else blackhole ()
452         if false then blackhole () else blackhole ()
453         let _ = blackhole in 2
454         let _ = blackhole () in 2
455
456 25.  This problem aims to get you thinking about how to control order of evaluation.
457 Here is an attempt to make explicit the behavior of `if ... then ... else ...` explored in the previous question.
458 The idea is to define an `if ... then ... else ...` expression using
459 other expression types.  So assume that `yes` is any (possibly complex) OCaml expression,
460 and `no` is any other OCaml expression (of the same type as `yes`!),
461 and that `bool` is any boolean expression.  Then we can try the following:
462 `if bool then yes else no` should be equivalent to
463
464         let b = bool in
465         let y = yes in
466         let n = no in
467         match b with true -> y | false -> n
468
469     This almost works.  For instance,
470
471         if true then 1 else 2
472
473     evaluates to `1`, and
474
475         let b = true in let y = 1 in let n = 2 in
476         match b with true -> y | false -> n
477
478     also evaluates to `1`.  Likewise,
479
480         if false then 1 else 2
481
482     and
483
484         let b = false in let y = 1 in let n = 2 in
485         match b with true -> y | false -> n
486
487     both evaluate to `2`.
488
489     However,
490
491         let rec blackhole x = blackhole x in
492         if true then blackhole else blackhole ()
493
494     terminates, but
495
496         let rec blackhole x = blackhole x in
497         let b = true in
498         let y = blackhole in
499         let n = blackhole () in
500         match b with true -> y | false -> n
501
502     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.
503
504     Here's a [[hint|assignment5 hint1]].