Proposal: Deprecate ExistentialQuantification

John Meacham john at
Sun Jun 28 04:35:06 EDT 2009

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 Meacham - ⑆⑆john⑈ -

More information about the Haskell-prime mailing list