From: jim
Date: Sat, 21 Mar 2015 08:32:22 +0000 (0400)
Subject: more answers
XGitUrl: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=commitdiff_plain;h=9050fbccf4f1edc6c4de2999b968b61a50aae79c
more answers

diff git a/exercises/assignment5_answers.mdwn b/exercises/assignment5_answers.mdwn
index fd737786..2b29695a 100644
 a/exercises/assignment5_answers.mdwn
+++ b/exercises/assignment5_answers.mdwn
@@ 434,7 +434,7 @@ Again, we've left some gaps. (The use of `type` for the first line in Haskell an
HERE IS AN OCAML DEFINITION:
 type lambda_term = Var of identifier  Abstract of identifier * lambda_term  App of lambda_term * lambda_term
+ type lambda_term = Var of identifier  Abstract of identifier * lambda_term  App of lambda_term * lambda_term
16. Write a function `occurs_free` that has the following type:
@@ 442,7 +442,7 @@ Again, we've left some gaps. (The use of `type` for the first line in Haskell an
That's how OCaml would show it. Haskell would use double colons `::` instead, and would also capitalize all the type names. Your function should tell us whether the supplied identifier ever occurs free in the supplied `lambda_term`.
 HERE IS AN OCAML DEFINITION:
+ HERE IS AN OCAML ANSWER:
let rec occurs_free (ident : identifier) (term : lambda_term) : bool =
match term with
@@ 490,6 +490,16 @@ type `Bool`.
(b) the term `and` that takes two arguments of type `Bool` and computes their conjunction
(c) the term `or` that takes two arguments of type `Bool` and computes their disjunction
+ ANSWERS:
+
+ Bool â¡ âÎ±. Î± > Î± > Î±
+ true â¡ ÎÎ±. Î»y:Î±. Î»n:Î±. y
+ false â¡ ÎÎ±. Î»y:Î±. Î»n:Î±. n
+ not â¡ Î»p:Bool. p [Bool] false true
+ and â¡ Î»p:Bool. Î»q:Bool. p [Bool] (q [Bool]) false
+ or â¡ Î»p:Bool. Î»q:Bool. p [Bool] true (q [Bool])
+
+
The type `Nat` (for "natural number") may be encoded as follows:
Nat â¡ âÎ±. (Î± > Î±) > Î± > Î±
@@ 537,6 +547,27 @@ any type `Î±`, as long as your function is of type `Î± > Î±` and you have a bas
+
+`sysf_bool`, `sysf_true`, `sysf_false`,
+`sysf_nat`, `sysf_zero`, `sysf_iszero`, `sysf_succ`, and `sysf_pred`.
+
+ OCAML ANSWERS:
+
+ type ('a) sysf_bool = 'a > 'a > 'a
+ let sysf_true : ('a) sysf_bool = fun y n > y
+ let sysf_false : ('a) sysf_bool = fun y n > n
+
+ type ('a) sysf_nat = ('a > 'a) > 'a > 'a
+ let sysf_zero : ('a) sysf_nat = fun s z > z
+ let sysf_iszero (n : 'a sysf_nat) : 'b sysf_bool = n (fun _ > sysf_false) sysf_true
+ (* Annoyingly, though, if you just say sysf_iszero sysf_zero, you'll get an answer that isn't fully polymorphic.
+ This is explained in the comments linked below. The way to get a polymorphic result is to say instead
+ `fun next > sysf_iszero sysf_zero next`. *)
+ let sysf_succ (n : 'a sysf_nat) : 'a sysf_nat = fun s z > s (n s z)
+ (* Again, to use this you'll want to call `fun next > sysf_succ sysf_zero next` *)
+ let sysf_pred (n : 'a sysf_nat) : 'a sysf_nat = (* LEFT UNDONE *)
+
+
Consider the following list type, specified using OCaml or Haskell datatypes:
(* OCaml *)
@@ 587,7 +618,6 @@ Be sure to test your proposals with simple lists. (You'll have to `sysf_cons` up

## 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 or Haskell. To get you started, here's one typing for **K**:
@@ 599,7 +629,15 @@ Be sure to test your proposals with simple lists. (You'll have to `sysf_cons` up
If you can't understand how one term can have several types, recall our discussion in this week's notes of "principal types".
+ ANSWER: OCaml shows the principal typing for S as follows:
+
+ # let s = fun f g x > f x (g x);;
+ val s : ('a > 'b > 'c) > ('a > 'b) > 'a > 'c =
+
+ You can get a more specific type by unifying any two or more of the above type variables. Thus, here is one other type that S can have:
+ # let s' = (s : ('a > 'b > 'a) > ('a > 'b) > 'a > 'a);;
+ val s' : ('a > 'b > 'a) > ('a > 'b) > 'a > 'a =
## Evaluation Order ##
@@ 609,14 +647,16 @@ Do these last three problems specifically with OCaml in mind, not Haskell. Analo
23. Which of the following expressions is welltyped 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 ()
+ a. let rec f x = f x
+ b. let rec f x = f f
+ c. let rec f x = f x in f f
+ d. let rec f x = f x in f ()
+ e. let rec f () = f f
+ f. let rec f () = f ()
+ g. let rec f () = f () in f f
+ h. let rec f () = f () in f ()
+
+ ANSWER: All are welltyped except for b, e, and g, which involve selfapplication. d and h are welltyped but enter an infinite loop. Surprisingly, OCaml's typechecker accepts c, and it too enters an infinite loop. Not sure how to explain why OCaml's typechecker accepts that.
24. Throughout this problem, assume that we have:
@@ 625,20 +665,22 @@ Do these last three problems specifically with OCaml in mind, not Haskell. Analo
All of the following are welltyped. Which ones terminate? What generalizations can you make?
 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
+ a. blackhole
+ b. blackhole ()
+ c. fun () > blackhole ()
+ d. (fun () > blackhole ()) ()
+ e. if true then blackhole else blackhole
+ f. if false then blackhole else blackhole
+ g. if true then blackhole else blackhole ()
+ h. if false then blackhole else blackhole ()
+ i. if true then blackhole () else blackhole
+ j. if false then blackhole () else blackhole
+ k. if true then blackhole () else blackhole ()
+ l. if false then blackhole () else blackhole ()
+ m. let _ = blackhole in 2
+ n. let _ = blackhole () in 2
+
+ ANSWERS: These terminate: a,c,e,f,g,j,m; these don't: b,d,h,i,k,l,n. Generalization: blackhole is a suspended infinite loop, that is forced by feeding it an argument. The expressions that feed blackhole an argument (in a context that is not itself an unforced suspension) won't terminate.
25. This problem aims to get you thinking about how to control order of evaluation.
Here is an attempt to make explicit the behavior of `if ... then ... else ...` explored in the previous question.
@@ 690,12 +732,16 @@ and that `bool` is any boolean expression. Then we can try the following:
Here's a [[hintassignment5 hint1]].
Hint: Use thunks!
+ ANSWER:
+
+ let rec blackhole x = blackhole x in
+ let b = true in
+ let y () = blackhole in
+ let n () = blackhole () in
+ (match b with true > y  false > n) ()
Further hint: What does
+ If you said instead, on the last line:
 let x = (fun () > 2) in
 let y = (fun () > 3) in
 match true with true > x  false > y
+ match b with true > y ()  false > n ()
evaluate to?
+ 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. That is 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.