From 032eed9c0f02ad8b36cb921735496f6d20ea3d65 Mon Sep 17 00:00:00 2001 From: jim Date: Sat, 21 Mar 2015 10:01:12 -0400 Subject: [PATCH 1/1] tweak --- exercises/assignment5_answers.mdwn | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/exercises/assignment5_answers.mdwn b/exercises/assignment5_answers.mdwn index de916184..a1dfae79 100644 --- a/exercises/assignment5_answers.mdwn +++ b/exercises/assignment5_answers.mdwn @@ -500,8 +500,8 @@ type `Bool`. 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 of that type. 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 + 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. -- 2.11.0