[Haskell] "exists" keyword and "existential" types

[Simon Peyton-Jones]

| I find myself confused by the lack of an "exists" quantifier to
complement
| "forall". It imposes seemingly arbitrary restrictions on the ways in
which
| types can be expressed, and makes some seemingly harmless (and useful)
| types entirely inexpressible.
| 
| For example, it seems as though runST could just as well be given the
type
| 
|     runST :: forall a. exists s. ST s a -> a
| 
| This isn't necessarily better than the usual type, but why can't it be
| expressed? And it might actually be better: introducing exists would
make
| it possible to hoist quantifiers from both sides of the function
arrow,
| rather than just the RHS as GHC does now.
| 
| And it would be nice to be able to pass around values of type
| (exists t. Interface t => t), which behave just like OOP interface
| pointers. I don't see how
| 
|     openInputStream :: FilePath -> IO (exists t. InputStream t => t)

It's easier to suggest extensions to an already complicated type system
than it is to give a watertight specification of the extension, still
less to implement them.  Mark Shields and I (mainly Mark) did go through
the exercise of specifying a type system for Haskell with first-class
existentials.   It was extremely complicated, so much so that I cannot
even explain *why* it was extremely complicated, though Mark may be able
to.  In my mind, it stands as an un-met challenge: can one add
first-class existentials to Haskell (along with first-class universal
quantification, of course).  I know the Utrecht guys are thinking about
doing this in (some version of) Helium.  

Once you have a good specification, there remains the challenges of (a)
giving a reasonably simple type inference algorithm, and (b)
implementing it.

If anyone feels like running with this one, I'd like to suggest as a
baseline the paper that Mark and I wrote about first-class universals
"Practical type inference for higher-rank polymorphism".  It's on my
home page.
http://research.microsoft.com/%7Esimonpj/papers/putting/index.htm  The
reason it makes a good starting point is that it gives a complete,
executable type-inference engine for first-class universal polymorphism,
well suited for extension with first-class existentials.  And, of
course, it comes with a very detailed tutorial (the paper).


| > True, but why is this? Is there a deep reason why we can use nested
| > foralls as the arguments to (->), but not as the arguments to any
other
| > type constructor?
| 
| Apparently it makes type-checking Very Very Hard. Simon PJ may have
| explained it to me ("impredicative", he called it), but I don't
remember
| offhand.

This question, too, is discussed at some length in the paper.   It is
possible to do type inference in an impredicative system, but it's much
harder.  Le Botlan and Remy have an excellent paper, about a language
called MLF, that describes such a system, but it's not for the faint
hearted.

Simon