X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?a=blobdiff_plain;f=exercises%2Fassignment5_answers.mdwn;h=9be28e21a5493191a8200d8f902c191878e38720;hb=910830a353b8074d890aa989488e31f1d0888e6f;hp=fb85ba91e2d007bf42f6b3c305b6ee7ecfcbb3cb;hpb=4489d6639a1456736c27278db585af760a116fb5;p=lambda.git
diff --git a/exercises/assignment5_answers.mdwn b/exercises/assignment5_answers.mdwn
index fb85ba91..9be28e21 100644
--- a/exercises/assignment5_answers.mdwn
+++ b/exercises/assignment5_answers.mdwn
@@ -263,7 +263,7 @@ Choose one of these languages and write the following functions.
let rec tree_best_sofar (t : 'a color_tree) (lead : maybe_leader) : maybe_leader * int =
match t with
- | Leaf a -> (None, a)
+ | Leaf a -> (lead, a)
| Branch(l, col, r) ->
let (lead',left_score) = tree_best_sofar l lead in
let (lead'',right_score) = tree_best_sofar r lead' in
@@ -436,6 +436,8 @@ Again, we've left some gaps. (The use of `type` for the first line in Haskell an
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:
occurs_free : identifier -> lambda_term -> bool
@@ -504,7 +506,7 @@ type `Bool`.
also a mistake. What we want is a result whose type _is_ `Bool`, that is, `âα. α -> α -> α`. `(q [Bool])` doesn't have that type, but
rather the type `Bool -> Bool -> Bool`. The first, desired, type has an outermost `â`. The second, wrong type doesn't; it only has `â`s
inside the antecedents and consequents of the various arrows. The last one of those could be promoted to be an outermost `â`, since
- `P -> âα. Q â¡ âα. P -> Q` when `α` is not free in `P`. But that couldn't be done with the others.
+ `P -> âα. Q` is equivalent to `âα. P -> Q` when `α` is not free in `P`. But that couldn't be done with the others.
The type `Nat` (for "natural number") may be encoded as follows:
@@ -557,36 +559,44 @@ any type `α`, as long as your function is of type `α -> α` and you have a bas
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_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
+ 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
+ let sysf_iszero (n : ('a sysf_bool) sysf_nat) : 'a 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 = (* NOT DONE *)
-
-
-
+ (* Again, to get a polymorphic result you'll want to call `fun next -> sysf_succ sysf_zero next` *)
+
+ And here is how to get `sysf_pred`, using a System-F-style encoding of pairs. (For brevity, I'll leave off the `sysf_` prefixes.)
+
+ type 'a natpair = ('a nat -> 'a nat -> 'a nat) -> 'a nat
+ let natpair (x : 'a nat) (y : 'a nat) : 'a natpair = fun f -> f x y
+ let fst x y = x
+ let snd x y = y
+ let shift (p : 'a natpair) : 'a natpair = natpair (succ (p fst)) (p fst)
+ let pred (n : ('a natpair) nat) : 'a nat = n shift (natpair zero zero) snd
+
+ (* As before, to get polymorphic results you need to eta-expand your applications. Witness:
+ # let one = succ zero;;
+ val one : '_a nat =
+ # let one next = succ zero next;;
+ val one : ('a -> 'a) -> 'a -> 'a =
+ # let two = succ one;;
+ val two : '_a nat =
+ # let two next = succ one next;;
+ val two : ('a -> 'a) -> 'a -> 'a =
+ # pred two;;
+ - : '_a nat =
+ # fun next -> pred two next;;
+ - : ('a -> 'a) -> 'a -> 'a =
+ *)
Consider the following list type, specified using OCaml or Haskell datatypes:
@@ -713,7 +723,7 @@ Do these last three problems specifically with OCaml in mind, not Haskell. Analo
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.
+ 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. Also, unselected clauses of `if`-terms aren't ever evaluated.
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.
@@ -778,3 +788,5 @@ and that `bool` is any boolean expression. Then we can try the following:
match b with true -> y () | false -> n ()
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. Your assumption would be 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.
+
+ Question: don't the rhs of all the match clauses in `match b with true -> y | false -> n` have to have the same type? How can they, when one of them is `blackhole` and the other is `blackhole ()`? The answer has two parts. First is that an expression is allowed to have different types when it occurs several times on the same line: consider `let id x = x in (id 5, id true)`, which evaluates just fine. The second is that `blackhole` will get the type `'a -> 'b`, that is, it can have any functional type at all. So the principle types of `y` and `n` end up being `y : unit -> 'a -> 'b` and `n : unit -> 'c`. (The consequent of `n` isn't constrained to use the same type variable as the consequent of `y`.) OCaml can legitimately infer these to be the same type by unifying the types `'c` and `'a -> 'b`; that is, it instantiates `'c` to the functional type had by `y ()`.