Hi Keith,
| Type inference for Haskell (as described in Mark Jones' paper _Typing
| Haskell In Haskell_ and as performed by GHC) requires first splitting
| groups of let bindings into strongly-connected components. It then
| assumes that all binders in such a component will be generalised over
| the same vector of type variables.
It isn't strictly necessary to quantify all types in the same binding
group over the same vector of type variables. And, in fact, I'd disagree
with your claim: the type checker in my paper does not quantify each type
over the same set of variables. It is true that a single set of type
variables is passed to the quantify call in each case, but these are only
"candidates" for quantification. Look more closely at the definition of
quantify and you'll see that it selects only a subset of those variables
(and potentially in a different order) when it builds the quantified type.
| What is the justification for this assumption? Is it always the case
| that in a strongly-connected component
|
| let x1 = e1
| x2 = e2
| ...
| xn = en
| in
| e
|
| if xi has the type forall a b c . ti for some monotype ti then xj must
| have type forall a b c . tj for some monotype tj? (modulo
| permutations, of course)
No, here's a simple counterexample:
m x y = n y -- inferred type: a -> b -> c
n y = m undefined y -- inferred type: b -> c
Of course, nothing stops you from quantifying over extra type vars if you
want. Haskell doesn't provide this syntax, but you could treat n as a
function of type (forall a. forall b. forall c. b -> c). The extra
forall a quantifier doesn't do anything useful here, but it doesn't hurt
either. In fact you can do this with any pair of types. If A and B are
sets of type variables, then you can rewrite types (forall A. ta) and
(forall B. tb) in the form (forall C. ta) and (forall C. tb), respectively,
for any set of type variables C that includes the union of A and B.
Adding redundant quantifiers like this has some implications in an
implementation that translates to a System F style, type-passing
intermediate language ... which includes GHC and some ML compilers:
An extra quantified variable means an extra parameter in the
translation.
All the best,
Mark
----------------------------------------------------------------------------
[EMAIL PROTECTED] Pacific Software Research Center, Oregon Graduate Institute
Looking for a PhD or PostDoc? Interested in joining PacSoft? Let us know!
