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

[Jason Dagit]

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:
http://www.haskell.org/ghc/docs/6.12.2/html/users_guide/data-type-extensions.html

When the forall appears in certain places it behaves differently.  For
example:
  * 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:
http://hackage.haskell.org/trac/haskell-prime/wiki/ExistentialQuantification

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