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

[Ryan Ingram]

>> 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

On Tue, Jun 1, 2010 at 12:40 PM, Cory Knapp <cory.m.knapp at gmail.com> wrote:
> Ah! That makes sense. Which raises a new question: Is this type "too
> general"? Are there functions which are semantically non-boolean which fit
> in that type

Actually, this type is *less* general, in that it has less members.

Consider, what boolean is represented by this?
q :: CB Int
q = (+)

Whereas the (forall a. a -> a -> a) must work on *any* type, so it has
far less freedom to decide what to do, and therefore there are less
possible implementations.  In fact, if we treat all bottoms as equal,
I believe these are all of the distinguishible implementations of this
function:

t a _ = a
f _ a = a

a1 = undefined
a2 _ = undefined
a3 _ _ = undefined
a4 a b = seq b a
a5 a b = seq a b
a6 a = seq a (\_ -> a)
a7 a = seq a (\b -> b)

Without allowing bottoms, "t" and "f" are the only implementations.

Here's some discriminators that are bottom if the passed in function
is the first and not in the group of second:

disc_t_f b = b undefined ()
disc_f_t b = b () undefined
disc_6_t b = seq (b undefined) ()

disc_1_any b = seq b ()
disc_2_34567tf b = seq (b ()) ()
disc_3_4567tf b = seq (b () ()) ()
disc_4_6t b = b () undefined
disc_5_f b = b undefined ()
disc_7_6 b = b () undefined
disc_6_5 = seq (b undefined) ()

  -- ryan