<p>I found a good explanation and example in a paper called &quot;<a href="https://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/tldi10-vytiniotis.pdf" rel="nofollow noreferrer">Let Should not be Generalised</a>&quot;:</p>
<blockquote>
<p>A central feature of the Hindley-Milner system is that let-bound definitions are generalised. For example, consider the slightly artificial definition:</p>
</blockquote>
<blockquote>
<p><code>let f x = let g y = (x,y) in ...</code></p>
</blockquote>
<blockquote>
<p>The definition for <code>g</code> is typed in an environment in which <code>x :: a</code>, and the inferred type for <code>g</code> is <code>∀b.b → (a, b)</code>. This type is
polymorphic in <code>b</code>, but not in <code>a</code>, because the latter is free in the
type environment at the definition of <code>g</code>. This side condition, that <code>g</code>
should be <strong>generalised only over variables that are not free in the
type environment</strong>, is the only tricky point in the entire Hindley-Milner type system.</p>
</blockquote>

CC BY-SA 4.0
2023-01-25T19:24:51.063Z
2023-01-25T19:24:51.063Z
Brian Berns
<p>I'm trying to understand how generalization works in H-M type inference. In order to generalize a function, we:</p>
<ul>
<li>Collect all the free type variables in the type of the function body,</li>
<li>Subtract away any type variables that appear free in the type environment,</li>
<li>And whatever is leftover can be generalized into a type scheme</li>
</ul>
<p>The middle bullet is the one I'm having trouble with. In particular, I don't understand how it's possible for there to be any free type variables in the type environment. When we create a type scheme, we close over its free type variables, so the resulting scheme shouldn't have any free type variables. Thus, since none of the schemes in a type environment should have free type variables, how could the type environment itself have any free type variables?</p>
<p>Perhaps someone could give me a simple example program in OCaml or Haskell in which the type environment has a free type variable during type inference?</p>

CC BY-SA 4.0
2023-01-25T15:36:53.617Z
I am not sure what you're asking, but perhaps it would help to think about nested functions: `fun x -> .... (fun y -> e) ....`. If the type of `x` appears in `e`, will you generalize over it?
Andrej Bauer
CC BY-SA 4.0
2023-01-25T15:52:36.650Z
Generalization only occurs for `let` expressions, but I think you're probably right that inference of a nested `let` could encounter free type variables in the type environment. I will investigate that. Thank you.
Brian Berns
CC BY-SA 4.0
2023-01-25T15:56:46.850Z
Yes, `let` is the thing to look at, not functions. You lead me astray when you wrote "In order to generalize a function, we ..." :-)
Andrej Bauer
<type-theory><type-systems><type-inference>
Free type variables in Hindley-Milner type inference
Brian Berns
# Free type variables in Hindley-Milner type inference

(Asked by: username_0 on 2023-01-25)

I'm trying to understand how generalization works in H-M type inference. In order to generalize a function, we:

* Collect all the free type variables in the type of the function body,
* Subtract away any type variables that appear free in the type environment,
* And whatever is leftover can be generalized into a type scheme

The middle bullet is the one I'm having trouble with. In particular, I don't understand how it's possible for there to be any free type variables in the type environment. When we create a type scheme, we close over its free type variables, so the resulting scheme shouldn't have any free type variables. Thus, since none of the schemes in a type environment should have free type variables, how could the type environment itself have any free type variables?

Perhaps someone could give me a simple example program in OCaml or Haskell in which the type environment has a free type variable during type inference?

**Tags:** type-theory, type-systems, type-inference

> **Comments:**
> **username_1**: I am not sure what you're asking, but perhaps it would help to think about nested functions: `fun x -> .... (fun y -> e) ....`. If the type of `x` appears in `e`, will you generalize over it?  
> **username_0**: Generalization only occurs for `let` expressions, but I think you're probably right that inference of a nested `let` could encounter free type variables in the type environment. I will investigate that. Thank you.  
> **username_1**: Yes, `let` is the thing to look at, not functions. You lead me astray when you wrote "In order to generalize a function, we ..." :-)  

---

## 1 answers

### Answer by username_0 on 2023-01-25. Score: 2

I found a good explanation and example in a paper called "[Let Should not be Generalised](https://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/tldi10-vytiniotis.pdf)":

> A central feature of the Hindley-Milner system is that let-bound definitions are generalised. For example, consider the slightly artificial definition:

> `let f x = let g y = (x,y) in ...`

> The definition for `g` is typed in an environment in which `x :: a`, and the inferred type for `g` is `∀b.b → (a, b)`. This type is
> polymorphic in `b`, but not in `a`, because the latter is free in the
> type environment at the definition of `g`. This side condition, that `g`
> should be **generalised only over variables that are not free in the
> type environment**, is the only tricky point in the entire Hindley-Milner type system.


---

