tweak untyped_evaluators, add symlink
[lambda.git] / exercises / assignment5_answers.mdwn
index a1dfae7..0cdfa61 100644 (file)
@@ -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
 
+<a id="occurs_free"></a>
+
 16. Write a function `occurs_free` that has the following type:
 
         occurs_free : identifier -> lambda_term -> bool
@@ -537,7 +539,9 @@ any type `α`, as long as your function is of type `α -> α` and you have a bas
         -- Or this:
         let sysf_true = (\y n -> y) :: Sysf_bool a
 
-            :set -XExplicitForAll
+    Note that in both OCaml and Haskell code, the generalization `∀α` on the free type variable `α` is implicit. If you really want to, you can supply it explicitly in Haskell by saying:
+
+        :set -XExplicitForAll
         let { sysf_true :: forall a. Sysf_bool a; ... }
         -- or
         let { sysf_true :: forall a. a -> a -> a; ... }
@@ -555,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 *)
-
-<!--
-        (* Using a System F-style encoding of pairs, rather than native OCaml pairs ... *)
-          let pair a b = fun f -> f a b in
-          let snd x y next = y next in
-          let shift p next = p (fun x y -> pair (sysf_succ x) x) next in (* eta-expanded as in previous definitions *)
-          fun next -> n shift (pair sysf_zero sysf_zero) snd next
-
-    let pair = \a b. \f. f a b in
-    let snd = \x y. y in
-    let shift = \p. p (\x y. pair (succ x) x) in
-    let pred = \n. n shift (pair 0 err) snd in
--->
-
+        (* 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 = <fun>
+          # let one next = succ zero next;;
+          val one : ('a -> 'a) -> 'a -> 'a = <fun>
+          # let two = succ one;;
+          val two : '_a nat = <fun>
+          # let two next = succ one next;;
+          val two : ('a -> 'a) -> 'a -> 'a = <fun>
+          # pred two;;
+          - : '_a nat = <fun>
+          # fun next -> pred two next;;
+          - : ('a -> 'a) -> 'a -> 'a = <fun>
+        *)
 
 Consider the following list type, specified using OCaml or Haskell datatypes:
 
@@ -684,9 +696,9 @@ Do these last three problems specifically with OCaml in mind, not Haskell. Analo
 
         type 'a notok = 'a -> 'a notok
 
-    (In the technical jargon, OCaml has isorecursive not equirecursive types.) In any case, the reason that OCaml rejects b, e, and g is not the mere fact that they involve self-application, but the fact that typing them would require constructing one of the kinds of infinite chains of unbroken arrows that OCaml forbids. In case c, we can already see that the type of `f` is acceptable (it was ok in case a), and the self-application doesn't impose any new typing constraints because it never returns, so it can have any result type at all.
+    (In the technical jargon, OCaml has isorecursive not equirecursive types.) In any case, the reason that OCaml rejects b is not the mere fact that it involves self-application, but the fact that typing it would require constructing one of the kinds of infinite chains of unbroken arrows that OCaml forbids. In case c, we can already see that the type of `f` is acceptable (it was ok in case a), and the self-application doesn't impose any new typing constraints because it never returns, so it can have any result type at all.
 
-    In case g, the typing fails not specifically because of a self-application, but because OCaml has already determined that `f` has to take a `()` argument, and even before settling on `f`'s final type, one thing it knows about `f` is that it isn't `()`. So `let rec f () = f () in f f` fails for the same reason that `let rec f () = f () in f id` would.
+    In cases e and g, the typing fails not specifically because of a self-application, but because OCaml has already determined that `f` has to take a `()` argument, and even before settling on `f`'s final type, one thing it knows about `f` is that it isn't `()`. So `let rec f () = f () in f f` fails for the same reason that `let rec f () = f () in f id` would.
     
 
 24.  Throughout this problem, assume that we have:
@@ -711,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.
@@ -776,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 ()`.