[Haskell-cafe] A question on existential types and Church
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
>> 'a's), you need a CB (CB a). You can eliminate the asymmetric type,
>> 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...
More information about the Haskell-Cafe