+## 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 ();;