[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:
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
More information about the Haskell-Cafe
mailing list