On Thu, 15 Jan 2009, Andrew Coppin wrote:
I was especially amused by the assertion that "existential quantification" is a more precise term than "type variable hiding". (The former doesn't even tell you that the feature in question is related to the type system! Even the few people in my poll who knew of the term couldn't figure out how it might be related to Haskell. And one guy argued that "forall" should denote universal rather than existential quantification...)
This one's a particularly awkward special case. The original syntax for writing existential quantifications had looking like existing datatype declarations as a major goal, and this turned out to be just the wrong thing - GADTs made this rather more clear, and with the new syntax it should be much easier to explain why the forall keyword ends up meaning that. The first word that comes to mind for the old syntax... well, starts with an F. These things happen when you use research concepts though, and I can't see how at the time anyone could have been expected to do any better. As for "what's it got to do with types?" - well, that's a Curry-Howard thing. If I ever find myself in the situation of documenting a typed FPL for ordinary programmers, briefly explaining the relationship between type systems and logics is going to happen very early on indeed! -- flippa@flippac.org There is no magic bullet. There are, however, plenty of bullets that magically home in on feet when not used in exactly the right circumstances.