X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?a=blobdiff_plain;ds=sidebyside;f=exercises%2Fassignment5_answers.mdwn;h=7ef5a0bcc7a34401910800cc715d7b47133c1da6;hb=05e2be56f9d3216fb8bcc74a9ba72d8b50ef611c;hp=05752763e12a7de10b8e45498a65748121b72c71;hpb=6069fa51d80df8905405413cb6beaf38fd4129d0;p=lambda.git

diff --git a/exercises/assignment5_answers.mdwn b/exercises/assignment5_answers.mdwn
index 05752763..7ef5a0bc 100644
--- a/exercises/assignment5_answers.mdwn
+++ b/exercises/assignment5_answers.mdwn
@@ -496,8 +496,15 @@ type `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])
+        and ≡ λp:Bool. λq:Bool. p [Bool] q false
+        or ≡ λp:Bool. λq:Bool. p [Bool] true q
+
+    When I first wrote up these answers, I had put `(q [Bool])` where I now have just `q` in the body of `and` and `or`. On reflection,
+    this isn't necessary, because `q` is already a `Bool`. But as I learned by checking these answers with Pierce's evaluator, it's
+    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.
 
 
 The type `Nat` (for "natural number") may be encoded as follows:
@@ -530,7 +537,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; ... }