Proposal: Deprecate ExistentialQuantification

[Niklas Broberg]

Hi all,

Following the discussion on the use of 'forall' and extensions that
use it [1], I would hereby like to propose that the
ExistentialQuantification extension is deprecated.

My rationale is as follows. With the introduction of GADTs, we now
have two ways to write datatype declarations, the old simple way and
the GADTs way. The GADTs way fits better syntactically with Haskell's
other syntactic constructs, in all ways. The general style is
(somewhat simplified) "keyword type 'where' decls", where keyword can
in Haskell 98 be class or instance, but with GADTs also data. The old
simple way of defining data types is the odd one out. It certainly has
its uses though, in particular when defining some simple (but possibly
large) enum-like datatype (like cabal's Extension type incidentally),
then it obviously becomes tedious to have to restate the trivial type
signature for each constructor.

Using GADTs style syntax it is possible to allow constructors with
existentially quantified arguments with *no additional syntax needed*.
It follows nicely from the standard syntax for type signature
declarations (assuming explicit foralls), e.g. the following "normal"
datatype declaration

  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

which is syntactically just a normal type signature.

The upside of deprecating ExistentialQuantification is thus that we
keep the syntax cleaner, and we keep the old style of datatype
declarations simple (as it should be, IMO). Anything fancier can use
the GADTs syntax, which anyone that uses something fancier should be
acquainted with anyway.

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.

My own take on that is that what we have now is a wart that should be
removed, and that if we think that the latter is a problem then the
way to go would be to split the monolithic GADTs extension into
several semantic levels. There is of course also the downside that we
break existing code, but that's a standard problem with improvement
through deprecation which I will pay no mind.


Discussion period: 2 weeks

Cheers,

/Niklas

[1] http://www.haskell.org/pipermail/glasgow-haskell-users/2009-June/017432.html