X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=blobdiff_plain;f=exercises%2Fassignment5_answers.mdwn;h=f62f8b4f190fc4a00db8416f6e6c9a96a270db39;hp=fb85ba91e2d007bf42f6b3c305b6ee7ecfcbb3cb;hb=9201e22a70ab4dc37c2d5996d18fa09ef00ea706;hpb=4489d6639a1456736c27278db585af760a116fb5

diff --git a/exercises/assignment5_answers.mdwn b/exercises/assignment5_answers.mdwn
index fb85ba91..f62f8b4f 100644
--- a/exercises/assignment5_answers.mdwn
+++ b/exercises/assignment5_answers.mdwn
@@ -713,7 +713,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 +778,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 ()`.