On Tue, Jun 1, 2010 at 3:40 PM, Cory Knapp
In the new type, the parameter 'a' is misleading. It has no connection to the 'a's on the right of the equals sign. You might as well write:
type CB = forall a. a -> a -> a
Ah! That makes sense. Which raises a new question: Is this type "too general"? Are there functiosn which are semantically non-boolean which fit in that type, and would this still be the case with your other suggestion (i.e. "cand p q = p (q t f) f" )?
Because the type is universally quantified, any function with that signature can only manipulate the values it's given, having no way of creating new values of that type, or inspecting them in any way. It receives two values and returns one, so (ignoring _|_) only two implementations are possible: (\x _ -> x) and (\_ x -> x), which are the Church booleans. Intuitively, observe that the function must, and may only, make a decision between two options--thus providing exactly one bit of information, no more and no less. - C.