[Haskell-cafe] Re: Aren't type system extensions fun? [Further analysis]

[Tillmann Rendel]

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