I’m currently reading Heeren, B., Hage, J., & Swiestra, D. (2002). Generalizing Hindley-Milner Type Inference Algorithms in an attempt to understand Hindley-Milner-style type inference.
I'm struggling with two concepts early in the paper, the first is generalization of a type. From the article:
Generalizing a type $\tau$ with respect to a type environment $\Gamma$ entails the quantification of the type variables that are free in $\tau$ but do not occur in $\Gamma$:
$$generalize(\Gamma,\tau) =_{def}\;\forall\vec{\alpha}.\tau \;\;\text{ where } \vec{\alpha} = freevars(\tau)-freevars(\Gamma)$$
In the literature, generalization is sometimes referred to as determining the closure of a type. In fact, these different notations, e.g. $\Gamma$($\tau$) in [DM82] and Clos$\Gamma$($\tau$) in [LY98], all express the same.
Another explanation is that generalize “abstracts a type over all type variables which are free in the type but not free in the given type environment.”
However, I fail to see what this accomplishes and when you want to do this, and would be very grateful if someone can point me in the right direction.
Another concept is instantiation, explained in the following manner:
An instantiation of a type scheme is obtained by the replacement of the quantified type variables by fresh type variables: $$instantiate(\forall \alpha_1\ldots\alpha_n.\tau =_{def}\; [\alpha_1 := \beta_1,\ldots,\alpha_n := \beta_n]\tau \;\;\text{ where } \beta_1,\ldots,\beta_n \text{ are fresh}$$ A type $\tau_1$ is a generic instance of a type scheme $\sigma = \forall\vec{\alpha}.\tau_2$ if there exists a substitution S with S$\beta$ = $\beta$ for all $\beta \in freevars(\sigma)$ such that $\tau_1$ and S$\tau_2$ are syntactically equal.
Does this simply mean that you replace all bound type variables with globally unique variables in order to avoid accidental collisions, or is there more to it?
