Andrew Coppin wrote:
So, after an entire day of boggling my mind over this, I have brought it
down to one simple example:
(id 'J', id True) -- Works perfectly.
\f -> (f 'J', f True) -- Fails miserably.
Both expressions are obviously perfectly type-safe, and yet the type
checker stubbornly rejects the second example. Clearly this is a flaw in
the type checker.
So what is the type of that second expression? You would think that
(x -> x) -> (Char, Bool)
as a valid type for it. But alas, this is not correct. The CALLER is
allowed to choose ANY type for x - and most of possible choices wouldn't
be type-safe. So that's no good at all!
All possible choices wouldn't be type-safe, so its even worse.
In a nutshell, the function being passed MAY accept any type - but we
want a function that MUST accept any type. This excusiatingly subtle
distinction appears to be the source of all the trouble.
Interestingly, if you throw in the undocumented "forall" keyword,
everything magically works:
(forall x. x -> x) -> (Char, Bool)
But you have to do it right.
forall x . (x -> x) -> (Char, Bool)
is equivalent to the version without forall, and does you no good. (Note
the parentheses to see why these two types are different). So there lies
no magic in mentioning forall, but art in putting it in the correct
position.
The key problem seems to be that the GHC manual assumes that anybody
reading it will know what "universal quantification" actually means.
Unfortunately, neither I nor any other human being I'm aware of has the
slightest clue what that means. A quick search on that infallable
reference [sic] Wikipedia yields several articles full of dense logic
theory. Trying to learn brand new concepts from an encyclopedia is more
or less doomed from the start. As far as I can comprehend it, we have
existential quantification = "this is true for SOMETHING"
universal quantification = "this is true for EVERYTHING"
Quite how that is relevant to the current discussion eludes me.
Your "MUST accept any type" is related to universal quantification, and
your "MAY accept any type" is related to existential quantification:
This works for EVERYTHING, so it MUST accept any type.
This works for SOMETHING, so it accepts some unknown type.
Quantification is the logic word for "abstracting by introducing a name
to filled with content later". For example, in your above paragraph you
wanted to tell us that no human being you are aware of has the slightest
clue what "universal quantification" means. You could have done so by
enumerating all human beings you are aware of. Instead, you used
universal quantification:
for all HUMAN BEING, HUMAN BEING has no clue.
(shortened to not overcomplicate things, HUMAN BEING is the name here).
Tillmann
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
