| 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