Proposal: Deprecate ExistentialQuantification

Isaac Dupree ml at isaac.cedarswampstudios.org
Sat Jun 27 10:51:12 EDT 2009


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.)

-Isaac


More information about the Haskell-prime mailing list