[Haskell-cafe] A question on existential types and Church encoding

[C. McCann]

On Tue, Jun 1, 2010 at 3:40 PM, Cory Knapp <cory.m.knapp at gmail.com> wrote:
>> 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.