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:
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
(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 ≡ ∀α. (α -> α) -> α -> α
+-----
+`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 *)
-
## 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**:
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 = <fun>
+
+ 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 = <fun>
## Evaluation Order ##
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 ()
+ 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 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. Not sure how to explain why OCaml's type-checker accepts that.
24. Throughout this problem, assume that we have:
<!-- Haskell could say: `let blackhole = \x -> fix (\f -> f)` -->
All of the following are well-typed. 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.
Here's a [[hint|assignment5 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.