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

[Andrew Coppin]

Luke Palmer wrote:
> When you're reasoning about this, I think it would help you greatly to
> explicitly put in *all* the foralls.  In haskell, when you write, say:
>
>    map :: (a -> b) -> [a] -> [b]
>
> All the free variables are *implicitly* quantified at the top level.
> That is, when you write the above, the compiler sees:
>
>    map :: forall a b. (a -> b) -> [a] -> [b]
>
> And the type you mention above for the strange expression is:
>
>    forall x. (x -> x) -> (Char, Bool)
>
> Which indicates that the caller gets to choose.  That is, if a caller
> sees a 'forall' at the top level, it is allowed to instantiate it with
> whatever type it likes.   Whereas the type you want has the forall in
> a different place than the implicit quantifiaction:
>
>    (forall x. x -> x) -> (Char, Bool)
>
> Here the caller does not have a forall at the top level, it is hidden
> inside a function type so the caller cannot instantiate the type.
> However, when implementing this function, the argument will now have
> type
>
>     forall x. x -> x
>
> And the implementation can instantiate x to be whatever type it likes.
>   

Hmm. Right. So you're saying that the exact position of the "forall" 
indicates the exact time when the variable(s) get specific types 
assigned to them?

So... the deeper you nest the foralls, the longer those variables stay 
unbound? [And the higher the "rank" of the type?]

Finally, that seems to make actual sense. I have one final question though:

  forall x, y. x -> y -> Z
  forall x. x -> (forall y. y -> Z)

Are these two types the same or different? [Ignoring for a moment the 
obvious fact that you'll have one hell of a job writing a total function 
with such a type!] After all, ignoring the quantification, we have

  x -> y -> Z
  x -> (y -> Z)

which are both the same type. So does that mean you can move the forall 
to the left but not to the right? Or are the types actually different?