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

Jason Dagit dagit at codersbase.com
Tue Jun 1 16:33:46 EDT 2010

On Tue, Jun 1, 2010 at 12:40 PM, Cory Knapp <cory.m.knapp at gmail.com> wrote:

> Thanks! That was exactly the sort of response I was looking for.
> This explains why you need to double up for your current definitions. To
>> choose between two booleans (which will in turn allow you to choose
>> between
>> 'a's), you need a CB (CB a). You can eliminate the asymmetric type,
>> though,
>> like so:
>>  cand :: CB a -> CB a -> CB a
>>   cand p q t f = p (q t f) f
>> Right. When he was working on it, I thought of that, and seemed to have
> completely forgotten when I reworked it.
>> You can probably always do this, but it will become more tedious the more
>> complex your functions get.
>> > >type CB a = forall a . a -> a -> a
>> Note: this is universal quantification, not existential.
>> As I would assume. But I always see the "forall" keyword used when
> discussing "existential quantification". I don't know if I've ever seen an
> "exists" keyword. Is there one? How would it be used?

There is no exists keyword, in GHC at least.  See for example this page:

When the forall appears in certain places it behaves differently.  For
  * In a function signature it is universal, but where it appears matters.
Putting it on the left side of function arrows increases the rank of the
type.  This leads to Rank N types.
  * In the case of data constructors it can behave as existential
quantification when it introduces a type variable on the right-hand side of
the equal sign in the data declaration.

At least, that's my understanding.

Also, haskell prime has a proposal for an exists keyword:

-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://www.haskell.org/pipermail/haskell-cafe/attachments/20100601/959493b7/attachment.html

More information about the Haskell-Cafe mailing list