4
$\begingroup$

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?

$\endgroup$
3
  • $\begingroup$ 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? $\endgroup$ Jan 25 at 15:36
  • $\begingroup$ 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. $\endgroup$ Jan 25 at 15:52
  • $\begingroup$ Yes, let is the thing to look at, not functions. You lead me astray when you wrote "In order to generalize a function, we ..." :-) $\endgroup$ Jan 25 at 15:56

1 Answer 1

2
$\begingroup$

I found a good explanation and example in a paper called "Let Should not be Generalised":

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.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Not the answer you're looking for? Browse other questions tagged or ask your own question.