author jim Sun, 1 Mar 2015 16:49:26 +0000 (11:49 -0500) committer Linux User Sun, 1 Mar 2015 16:49:26 +0000 (11:49 -0500)

index 90043d7..d3646d7 100644 (file)
Assignment 5

-Types and OCaml
----------------
+≡

-0.     Recall that the S combinator is given by \x y z. x z (y z).
-       Give two different typings for this function in OCaml.
-       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

+## Option / Maybe Types ##

-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?
+You've already defined and worked with `map` as a function on lists. Now we're going to work instead with the type OCaml defines like this:

-               let rec f x = f x;;
+    type ('a) option = None | Some of 'a

-               let rec f x = f f;;

-               let rec f x = f x in f f;;
+    data Maybe a = Nothing | Just a

-               let rec f x = f x in f ();;
+That is, instances of this type are either some `'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 list guaranteed to have a length &leq; 1.

-               let rec f () = f f;;
+In one of the homework sessions, 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?

-               let rec f () = f ();;
+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`. We won't confuse a bin that contains a bin with an empty bin. (Not even if the contained bin is itself empty.)

-               let rec f () = f () in f f;;
+1.  Your first problem is to write a `maybe_map` function for these types. Here is the type of the function you should write:

-               let rec f () = f () in f ();;
+        (* OCaml *)
+        maybe_map : ('a -> 'b) -> ('a) option -> ('b) option

-2.     Throughout this problem, assume that we have
+        maybe_map :: (a -> b) -> Maybe a -> Maybe b

-               let rec blackhole x = blackhole x;;
+    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`.

-       All of the following are well-typed.
-       Which ones terminate?  What are the generalizations?
+    One way to extract the contents of a option or Maybe value is to pattern match on that value, as you did with lists. In OCaml:

-               blackhole;;
+        match x with
+        | None -> ...
+        | Some y -> ...

-               blackhole ();;

-               fun () -> blackhole ();;
+        case x of {
+          Nothing -> ...;
+          Just y -> ...
+        }

-               (fun () -> blackhole ()) ();;
+    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. You may want to review the [[Rosetta pages here]] and also read some of the tutorials we linked to [[for OCaml]] or [[for Haskell]]. [WHERE]

-               if true then blackhole else blackhole;;

-               if false then blackhole else blackhole;;
+2.  Next write a `maybe_map2` function. Its type should be:

-               if true then blackhole else blackhole ();;
+        (* OCaml *)
+        maybe_map2 ('a -> 'b -> 'c) -> ('a) option -> ('b) option -> ('c) option

-               if false then blackhole else blackhole ();;
+        maybe_map2 :: (a -> b -> c) -> Maybe a -> Maybe b -> Maybe c

-               if true then blackhole () else blackhole;;

-               if false then blackhole () else blackhole;;

-               if true then blackhole () else blackhole ();;
+## Color Trees ##

-               if false then blackhole () else blackhole ();;
+(The questions on Color and Search Trees are adapted from homeworks in Chapters 1 and 2 of Friedman and Wand, *Essentials of Programming Languages*.)

-               let _ = blackhole in 2;;
+Here are type definitions for one kind of binary tree:

-               let _ = blackhole () in 2;;
+    (* 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

-4.     This problem is to begin thinking about controlling order of evaluation.
-The following expression 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 OCaml expression,
-and "no" is any other OCaml expression (of the same type as "yes"!),
-and that "bool" is any boolean.  Then we can try the following:
-"if bool then yes else no" should be equivalent to
+    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_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 lists 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))
+
+    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 (_, c, _) -> c = Red
+
+    case t of {
+      Leaf n -> False;
+      Branch _ c _ -> c == Red
+    }
+
+These expressions query whether `t` is a branching `color_tree` (not a leaf) whose root is labeled `Red`.
+
+Choose one of these languages and write the following functions.
+
+
+3.  Define a function `tree_map` whose type is (as shown by OCaml): `('a -> 'b) -> ('a) color_tree -> ('b) color_tree`. It expects a function `f` and an `('a) color_tree`, and returns a new tree with the same structure and inner branch labels as the original, but with all of its leaves now having had `f` applied to their original value. So for example, `map (2*) t1` would return `t1` with all of its leaf values doubled.
+
+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.
+
+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`?
+
+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.)
+
+7.  How would you use the function defined in problem 4 to make a copy of a tree with the same structure and inner node labels, but where the leftmost leaf is now labeled `0`, the second-leftmost leaf is now labeled `1`, and so on.
+
+8.  (More challenging.) Write a recursive function that makes a copy of a tree with the same structure and inner node labels, but replaces each leaf label with the int that reports how many of that leaf's ancestors are labeled `Red`. For example, if we give your function a tree:
+
+    <pre>
+        Red
+        / \
+      Blue \
+      / \  Green
+     a   b  / \
+           c   Red
+               / \
+              d   e
+    </pre>
+
+    (for any leaf values `a` through `e`), it should return:
+
+    <pre>
+        Red
+        / \
+      Blue \
+      / \  Green
+     1   1  / \
+           1   Red
+               / \
+              2   2
+    </pre>
+
+9.  (More challenging.) Assume you have a `color_tree` whose leaves are labeled with `int`s (which might be negative). For this problem, assume also that the the same color never labels multiple inner 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.
+
+
+## Search Tree ##
+
+(More challenging.) For the next problem, assume the following type definition:
+
+    (* OCaml *)
+    type search_tree = Nil | Inner of search_tree * int * search_tree
+
+    data Search_tree = Nil | Inner Search_tree Int Search_tree  deriving (Show)
+
+That is, its leaves have no labels and its inner nodes are labeled with `int`s. Additionally, assume that all the `int`s in nodes descending to the left from a given node will be less than the `int` of that parent node, and all the `int`s in nodes descending to the right will be greater. We can't straightforwardly specify this constraint in OCaml's or Haskell's type definitions. We just have to be sure to maintain it by hand.
+
+10. Write a function `search_for` with the following type, as displayed by OCaml:
+
+        type direction = Left | Right
+        search_for : int -> search_tree -> direction list option

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

-       This almost works.  For instance,
+        data Direction = Left | Right  deriving (Eq, Show)
+        search_for :: Int -> Search_tree -> Maybe [Direction]

-               if true then 1 else 2;;
+    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]`.

-       evaluates to 1, and

-               let b = true in let y = 1 in let n = 2 in
-               match b with true -> y | false -> n;;
+## More Map2s ##

-       also evaluates to 1.  Likewise,
+Above, you defined `maybe_map2` [WHERE]. Before we encountered `map2` for lists. There are in fact several different approaches to mapping two lists together.

-               if false then 1 else 2;;
+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:

-       and
+        (* OCaml *)
+        map2_zip : ('a -> 'b -> 'c) -> ('a) list -> ('b) list -> ('c) list

-               let b = false in let y = 1 in let n = 2 in
-               match b with true -> y | false -> n;;
+    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 that do this. This also corresponds to what you can write as a list comprehension in Haskell like this:

-       both evaluate to 2.
+        :set -XParallelListComp
+        [ f x y | x <- xs | y <- ys ]

-       However,
+    But we want you to write this function from scratch.)

-               let rec blackhole x = blackhole x in
-               if true then blackhole else blackhole ();;
+12. What is the relation between the function you just wrote, and the `maybe_map2` function you wrote for an earlier problem?

-       terminates, but
+13. Another strategy is to take the *cross product* of the two lists. If the function:

-               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;;
+        (* OCaml *)
+        map2_cross : ('a -> 'b -> 'c) -> ('a) list -> ('b) list -> ('c) list list

-       does not terminate.  Incidentally, `match bool with true -> yes |
-       false -> no;;` works as desired, but your assignment is to solve it
-       without using the magical evaluation order properties of either `if`
-       or of `match`.  That is, you must keep the `let` statements, though
-       you're allowed to adjust what `b`, `y`, and `n` get assigned to.
+    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.

-       [[hints/assignment 5 hint 1]]
+A similar choice between "zipping" and "crossing" could be made when `map2`-ing two trees. For example, the trees:

-Booleans, Church numerals, and v3 lists in OCaml
-------------------------------------------------
+<pre>
+    0       5
+   / \     / \
+  1   2   6   7
+ / \         / \
+ 3  4        8  9
+</pre>

-(These questions adapted from web materials by Umut Acar. See
+could be "zipped" like this (ignoring any parts of branches on the one tree that extend farther than the corresponding branch on the other):
+
+<pre>
+   f 0 5
+   /    \
+f 1 6  f 2 7
+</pre>
+
+14. 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.
+
+[LOOKUP in APPLICATIVE]
+
+*   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 last week [WHERE] where you converted `[3, 2, 0, 1]` not into `[[3,3,3], [2,2], [], ]` --- which still has the same structure, that is length, as the original --- but rather into `[3, 3, 3, 2, 2, 1]` --- which doesn't.
+
+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.
+
+
+    type Identifier = String
+    data Lambda_term = Var Identifier | Abstract Identifier _____ | App ________
+
+15. Again, we've left some gaps. Choose one of these languages and fill in the gaps to complete the definition.
+
+16. Write a function `occurs_free` that has the following type:
+
+    occurs_free : identifier -> lambda_term -> bool
+
+That's how OCaml would show it. Haskell would use double colons `::` instead, and would also capitalize all the type names. Your function should tell us whether the supplied identifier ever occurs free in the supplied `lambda_term`.
+
+
+
+
+## Encoding Booleans, Church numerals, and Right-Fold Lists in System F ##
+
+(These questions are adapted from web materials by Umut Acar. See
<http://www.mpi-sws.org/~umut/>.)

+
+(For the System F questions, you can either download and compile Pierce's evaluator for system F to test your work [WHERE], or work on paper.)
+
+
+
+
Let's think about the encodings of booleans, numerals and lists in System F,
-and get data-structures with the same form working in OCaml. (Of course, OCaml
-has *native* versions of these datas-structures: its `true`, `1`, and `[1;2;3]`.
+and get data-structures with the same form working in OCaml or Haskell. (Of course, OCaml and Haskell
+have *native* versions of these datas-structures: 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.
+Recall from class System F, or the polymorphic λ-calculus, with this grammar:

-       types τ ::= c | 'a | τ1 → τ2 | ∀'a. τ
-       expressions e ::= x | λx:τ. e | e1 e2 | Λ'a. e | e [τ]
+    types ::= type_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 := ∀'a. 'a → 'a → 'a
-       true := Λ'a. λt:'a. λf :'a. t
-       false := Λ'a. λt:'a. λf :'a. f
+    bool ≡ ∀α. α -> α -> α
+    true ≡ Λα. λy:α. λn:α. y
+    false ≡ Λα. λy:α. λn:α. n

It's used like this:

-       b [τ] e1 e2
+    b [T] res1 res2

-where b is a boolean value, and τ is the shared type of e1 and e2.
+where `b` is a boolean value, and `T` is the shared type of `res1` and `res2`.

-**Exercise**. 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.
+17. How should we implement the following terms? Note that the result
+of applying them to the appropriate arguments should also give us a term of
+type `bool`.

+    (a) the term `not` that takes an argument of type `bool` and computes its negation
+    (b) the term `and` that takes two arguments of type `bool` and computes their conjunction
+    (c) the term `or` that takes two arguments of type `bool` and computes their disjunction

-The type nat (for "natural number") may be encoded as follows:
+The type `nat` (for "natural number") may be encoded as follows:

-       nat := ∀'a. 'a → ('a → 'a) → 'a
-       zero := Λ'a. λz:'a. λs:'a → 'a. z
-       succ := λn:nat. Λ'a. λz:'a. λs:'a → 'a. s (n ['a] z s)
+    nat ≡ ∀α. (α -> α) -> α -> α
+    zero ≡ Λα. λs:α -> α. λz:α. z
+    succ ≡ λn:nat. Λα. λs:α -> α. λz:α. s (n [α] s z)

-A nat n is deﬁned by what it can do, which is to compute a function iterated n
+A number `n` is deﬁned by what it can do, which is to compute a function iterated n
times. In the polymorphic encoding above, the result of that iteration can be
-any type 'a, as long as you have a base element z : 'a and a function s : 'a → 'a.
+any type `α`, as long as you have a function `s : α -> α` and a base element `z : α`.

-**Exercise**: get booleans and Church numbers working in OCaml,
-including OCaml versions of bool, true, false, zero, iszero, succ, and pred.
-It's especially useful to do a version of pred, starting with one
-of the (untyped) versions available in the lambda library
-accessible from the main wiki page.  The point of the excercise
-is to do these things on your own, so avoid using the built-in
-OCaml booleans and integers.
+18. Get booleans and Church numbers working in OCaml or Haskell,
+including versions of `bool`, `true`, `false`, `zero`, `zero?` (though this is not a legal function name in either of those languages, use something else), `succ`, and `pred`.
+It's especially useful to do a version of `pred`, starting with one of the (untyped) versions available in the lambda library accessible from the main wiki page. [WHERE]  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.

-Consider the following list type:
+Consider the following list type, specified using OCaml or Haskell datatypes:

-       type 'a list = Nil | Cons of 'a * 'a list
+    (* OCaml *)
+    type ('a) my_list = Nil | Cons of 'a * 'a my_list

-We can encode τ lists, lists of elements of type τ as follows:
+     data My_list a = Nil | Cons a (My_list a)

-       τ list := ∀'a. 'a → (τ → 'a → 'a) → 'a
-       nil τ := Λ'a. λn:'a. λc:τ → 'a → 'a. n
-       make_list τ := λh:τ. λt:τ list. Λ'a. λn:'a. λc:τ → 'a → 'a. c h (t ['a] n c)
+We can encode that type into System F as a right-fold, just as we did in the untyped Lambda Calculus, like this:

-More generally, the polymorphic list type is:
+    list_T ≡ ∀α. (T -> α -> α) -> α -> α
+    nil_T ≡ Λα. λc:T -> α -> α. λn:α. n
+    cons_T ≡ λx:T. λxs:list_T. Λα. λc:T -> α -> α. λn:α. c x (xs [α] c n)

-       list := ∀'b. ∀'a. 'a → ('b → 'a → 'a) → 'a
+A more general polymorphic list type is:

-As with nats, recursion is built into the datatype.
+    list ≡ ∀β. ∀α. (β -> α -> α) -> α -> α

-We can write functions like map:
+As with nats, the natural recursion is built into our encoding of this datatype. So we can write functions like `map`:

-       map : (σ → τ ) → σ list → τ list
+    map : (S -> T) -> list_S -> list_T

<!--
-               = λf :σ → τ. λl:σ list. l [τ list] nil τ (λx:σ. λy:τ list. make_list τ (f x) y
+    = λf:S -> T. λxs:list. xs [S] [list [T]] (λx:S. λys:list [T]. cons [T] (f x) ys) (nil [T])
-->

-**Excercise** convert this function to OCaml. We've given you the type; you
-only need to give the term.
+19. Convert this list encoding and the `map` function to OCaml or Haskell. Call it `sysf_list`, `sysf_nil` and so on, to avoid collision with the names for native lists in these languages.

-Also give us the type and definition for a `head` function. Think about what
-value to give back if the argument is the empty list.  Ultimately, we might
-want to make use of our `'a option` technique, but for this assignment, just
-pick a strategy, no matter how clunky.
+20. Also give us the type and definition for a `sysf_head` function. Think about what value to give back if the argument is the empty list.  Ultimately, we might want to make use of the option/Maybe technique explored in questions 1--2, but for this assignment, just pick a strategy, no matter how clunky.

-Be sure to test your proposals with simple lists. (You'll have to `make_list`
-the lists yourself; don't expect OCaml to magically translate between its
-native lists and the ones you buil.d)
+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.)

-<!--
-Consider the following simple binary tree type:
+21. Modify the implementation of the predecessor function [[given in the class notes|topics/week5_system_f]] [WHERE] to implement a `sysf_tail` function for your lists.

-       type 'a tree = Leaf | Node of 'a tree * 'a * 'a tree

-**Excercise**
-Write a function `sum_leaves` that computes the sum of all the leaves in an int
-tree.

-Write a function `in_order` : τ tree → τ list that computes the in-order
-traversal of a binary tree. You may assume the above encoding of lists; deﬁne
-any auxiliary functions you need.
--->

-1. Modify the implementation of the predecessor function [[given in
-the class notes|topics/week5_system_f]] to implement a tail function
-for system F to test your work if you like, or work on paper.)

------------

-Read the material on dividing by zero/towards monads from <strike>the end of lecture
-notes for week 6</strike> the start of lecture notes for week 7, then write a function `lift'` that generalized the
-correspondence between + and `add'`: that is, `lift'` takes any two-place
-operation on integers and returns a version that takes arguments of type `int
-option` instead, returning a result of `int option`.  In other words, `lift'`
-will have type:

-       (int -> int -> int) -> (int option) -> (int option) -> (int option)
+## More on Types ##
+
+22.  Recall that the S combinator is given by `\f g x. f x (g x)`. Give two different typings for this term in OCaml. 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 [WHERE] of "principal types".
+
+
+
+
+## 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.
+
+
+23.  Which of the following expressions is well-typed in OCaml? For those that are, give the type of the expression as a whole. For those that are not, why not?
+
+        let rec f x = f x;;
+
+        let rec f x = f f;;
+
+        let rec f x = f x in f f;;
+
+        let rec f x = f x in f ();;
+
+        let rec f () = f f;;
+
+        let rec f () = f ();;
+
+        let rec f () = f () in f f;;
+
+        let rec f () = f () in f ();;
+
+24.  Throughout this problem, assume that we have:
+
+        let rec blackhole x = blackhole x;;
+
+    <!-- Haskell could say: `let blackhole = \x -> fix (\f -> f)` -->
+
+    All of the following are well-typed. Which ones terminate?  What are the generalizations?
+
+        blackhole;;
+
+        blackhole ();;
+
+        fun () -> blackhole ();;
+
+        (fun () -> blackhole ()) ();;
+
+        if true then blackhole else blackhole;;
+
+        if false then blackhole else blackhole;;
+
+        if true then blackhole else blackhole ();;
+
+        if false then blackhole else blackhole ();;
+
+        if true then blackhole () else blackhole;;
+
+        if false then blackhole () else blackhole;;
+
+        if true then blackhole () else blackhole ();;
+
+        if false then blackhole () else blackhole ();;
+
+        let _ = blackhole in 2;;
+
+        let _ = blackhole () in 2;;
+
+25.  This problem is to think about how to control order of evaluation.
+The following expression 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 ();;

-so that `lift' (+) (Some 3) (Some 4)` will evalute to `Some 7`.
-Don't worry about why you need to put `+` inside of parentheses.
-You should make use of `bind'` in your definition of `lift'`:
+    terminates, but

-       let bind' (u: int option) (f: int -> (int option)) =
-               match u with None -> None | Some x -> f x;;
+        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.

+    [[hints/assignment 5 hint 1]] WHERE