[Haskell-cafe] What does the `forall` mean ?

[wren ng thornton]

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