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

[Cory Knapp]

Hello,

A professor of mine was recently playing around during a lecture with Church
booleans (I.e., true = \x y -> x; false = \x y -> y) in Scala and OCaml. I
missed what he did, so I reworked it in Haskell and got this:

>type CB a = a -> a -> a

>ct :: CB aC
>ct x y = x

>cf :: CB a
>cf x y = y

>cand :: CB (CB a) -> CB a -> CB a
>cand p q = p q cf

>cor :: CB (CB a) -> CB a -> CB a
>cor p q = p ct q

I found the lack of type symmetry (the fact that the predicate arguments
don't have the same time) somewhat disturbing, so I tried to find a way to
fix it. I remembered reading about existential types being used for similar
type-hackery, so I added quantification to the CB type and got

>type CB a = forall a . a -> a -> a

>ctrue :: CB a
>ctrue x y = x

>cfalse :: CB a
>cfalse x y = y

>cand :: CB a -> CB a -> CB a
>cand p q = p q cfalse

>cor :: CB a -> CB a -> CB a
>cor p q = p ctrue q

which works. But I haven't the faintest idea why that "forall" in the type
makes things work... I just don't fully understand existential type
quantification. Could anyone explain to me what's going on that makes the
second code work?

Thanks,
Cory
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://www.haskell.org/pipermail/haskell-cafe/attachments/20100529/c4c83d96/attachment.html