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

[Ben Rudiak-Gould]

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)

would cause any more problems than

    data Foo = forall t. InputStream t => Foo t
    openInputStream :: FilePath -> IO Foo

What am I missing?


While looking through old posts for insight, I came across a thread from
last April started by Simon P-J, who wrote:

>
> Many of you have grown to love existential data types, which we current
> write like this:
>
> 	data T = forall a. Foo a (a -> Int)
> 
> Mark and I chose 'forall' rather than 'exists' to save grabbing another
> keyword from the programmer.  And indeed, the type of the constructor
> Foo is
> 	Foo :: forall a. a -> (a->Int) -> T
>
> But every single time I explain this to someone, I find I have to make
> excuses for using the term 'forall'.  I say "it really means 'exists',
> but we didn't want to lose another keyword".
>
> I have gradually concluded that our decision was a mistake.  (In
> fairness to Mark, I think I was the primary advocate for it.)  I reckon
> that we should
>
> 	Allow 'exists'
> 	Deprecate 'forall' (for defining existentials, that is)
> 	Eventually allow only 'exists'
>

But I think the use of "forall" in this context is correct, and "exists"
incorrect. I find it easy to explain: you're creating many different "Foo"
constructors, one for every possible type a, so when you extract a value
from a Foo you're getting some type a, but you don't know which. Using
"exists" here would express something different, namely that there's only
one Foo, but you don't know (and it mustn't matter) what type it expects
to be bound to a, and therefore you can't apply Foo to a value unless that
value is general enough to encompass all possible types for a. This gives
the constructor function a rank-2 type, or equivalently an
existentially-quantified variable at the top level. When you match against
the value you're getting something which has to be able to stand in for
any type.

I think the source of confusion is not the use of forall, but the term
"existential types". There is nothing existential about them! The type
variables involved can be either existentially or universally quantified,
depending on the context. They use exists in exactly the contexts where
"ordinary" type variables use forall, and vice versa.

Instead of changing the forall, I think we should change the name
"existential types" to something which approximately reflects what they
actually are, like "inaccessible types" or "hidden types". "Abstract
types" would also be a possibility, but I think it would be confused with
the separate concept of using module scope to hide value constructors. My
other suggestions might also cause that kind of confusion, but I still
think they're better than "existential types", which seems to have no more
to do with the concept being expressed than "left-handed types" or "male
types" would have.


-- Ben