Proposal: Deprecate ExistentialQuantification

[John Meacham]

On Sat, Jun 27, 2009 at 10:51:12AM -0400, Isaac Dupree wrote:
> Niklas Broberg wrote:
>>   data Foo =
>>     forall a . Show a => Foo a
>>
>> which uses ExistentialQuantification syntax, could be written as
>>
>>   data Foo where
>>     Foo :: forall a . Show a => a -> Foo
>
>> The downside is that we lose one level of granularity in the type
>> system. GADTs enables a lot more semantic possibilities for
>> constructors than ExistentialQuantification does, and baking the
>> latter into the former means we have no way of specifying that we
>> *only* want to use the capabilities of ExistentialQuantification.
>
> Is it easy algorithmically to look at a GADT and decide whether it has  
> only ExistentialQuantification features?  After all, IIRC, hugs and nhc  
> support ExistentialQuantification but their type systems might not be up  
> to the full generality of GADTs.  (GHC's wasn't even quite up to it for  
> quite a long time until around 6.8, when we finally got it right.)

Jhc also supports ExistentialQuantification but not full GADTs.

        John

-- 
John Meacham - ⑆repetae.net⑆john⑈ - http://notanumber.net/