Mark Lentczner wrote:
I also think I understand that the implicit 'forall' inherent in Haskell falls at different places in various constructs, which also had me confused. For example, while the above two function type declarations are equivalent, these two data declarations aren't:data Fizzle a = Fizzle (b -> (a, b)) a data Fizzle a = forall b. Fizzle (b -> (a, b)) a
They shouldn't. For data declarations there's the mix up that Lennart Augustsson brought up, but that's more of an issue with the implicit forall not being added in the first case.
Basically, the implicit forall is always added at the front. So if I have some type T, then that's implicitly (forall a b c... . T). It's like constructing well-formed formulae in predicate calculus except that we're never allowed to have free variables, just like we can't have free variables in a well-formed expression of the lambda calculus. Since Hindley--Milner type inference can only deal with Rank-1 polymorphism we know all the quantifiers must be at the front, and since we know everything must be quantified we can just leave the quantifiers implicit. In GHC we can have Rank-N quantification but we need to give the signatures to tell the compiler we're using them.
The reason I said "basically" is because Haskell also has some constructs which give type variables a larger scope than just the signature for a single function. Many of these (data, type, newtype, class) introduce a different kind of quantifier. The new quantifier is frequently written with iota and basically means that the variable is bound in the environment. Of course now that means we have to think about passing around an environment instead of just checking each signature in isolation. (There are other reasons why the compiler would have an environment for things, but now the user has to think about them too.)
-- Live well, ~wren _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
