<blockquote>
  <p>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.</p>
</blockquote>

<p>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 <code>generalize</code> it. Note that this is done at <code>let</code> bindings.</p>

CC BY-SA 4.0
2018-09-19T23:25:06.563Z
2018-09-19T23:25:06.563Z
J D
<p>I’m currently reading <a href="http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.18.9348" rel="nofollow">Heeren, B., Hage, J., &amp; Swiestra, D. (2002). <em>Generalizing Hindley-Milner Type Inference Algorithms</em></a> in an attempt to understand Hindley-Milner-style type inference.</p>

<p>I'm struggling with two concepts early in the paper, the first is
<em>generalization</em> of a type. From the article:</p>

<blockquote>
  <p>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$:</p>
  
  <p>$$generalize(\Gamma,\tau) =_{def}\;\forall\vec{\alpha}.\tau 
 \;\;\text{ where } \vec{\alpha} = freevars(\tau)-freevars(\Gamma)$$</p>
  
  <p>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.</p>
</blockquote>

<p>Another explanation is that <em>generalize</em> “abstracts a type over all type variables which are free in the type but not free in the given type environment.”</p>

<p>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.</p>

<p>Another concept is <em>instantiation</em>, explained in the following manner:</p>

<blockquote>
  <p>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.</p>
</blockquote>

<p>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?</p>

CC BY-SA 3.0
2014-05-15T20:55:39.770Z
The first question would answer itself if you implemented Hindley-Milner polymorphism, I think.
Andrej Bauer
<type-theory><type-inference>
Generalization and instantiation of types in Hindley-Milner type inference
beta
# Generalization and instantiation of types in Hindley-Milner type inference

(Asked by: username_0 on 2014-05-15)

I’m currently reading [Heeren, B., Hage, J., & Swiestra, D. (2002). *Generalizing Hindley-Milner Type Inference Algorithms*](http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.18.9348) 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?

**Tags:** type-theory, type-inference
> **Comments:**
> **username_1**: The first question would answer itself if you implemented Hindley-Milner polymorphism, I think.  

---

## 1 answers

### Answer by username_2 on 2018-09-19. Score: 4

> 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.


---

