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