[Haskell-cafe] What does the `forall` mean ?
wren ng thornton
wren at freegeek.org
Mon Nov 16 02:56:05 EST 2009
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
More information about the Haskell-Cafe
mailing list