[Haskell-cafe] Comments from OCaml Hacker Brian Hurt

[Philippa Cowderoy]

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 at 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.