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
_______________________________________________
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

Reply via email to