Generalization and instantiation of types in Hindley-Milner type inference I’m currently reading Heeren, B., Hage, J., &amp; 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?
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.


When you define the function x -> x and first apply it to an integer you don't want the type of that identity function to be specialized to int -> int. That's why you generalize it. Note that this is done at let bindings.