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?
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
