How do I understand the Hindley-Milner rules?
Hindley-Milner is a set of rules in the form of sequent calculus (not natural deduction) that demonstrates that we can deduce the (most general) type of a program from the construction of the program without explicit type declarations.
The symbols and notation
First, let's explain the symbols, and discuss operator precedence
𝑥 is an identifier (informally, a variable name).
: means is a type of (informally, an instance of, or "is-a").
𝜎 (sigma) is an expression that is either a variable or function.
thus 𝑥:𝜎 is read "𝑥 is-a 𝜎"
∈ means "is an element of"
𝚪 (Gamma) is an environment.
⊦ (the assertion sign) means asserts (or proves, but contextually "asserts" reads better.)
𝚪 ⊦ 𝑥 : 𝜎 is thus read "𝚪 asserts that 𝑥, is-a 𝜎"
𝑒 is an actual instance (element) of type 𝜎.
𝜏 (tau) is a type: either basic, variable (𝛼), functional 𝜏→𝜏', or product 𝜏×𝜏' (product is not used here)
𝜏→𝜏' is a functional type where 𝜏 and 𝜏' are potentially different types.
𝜆𝑥.𝑒 means 𝜆 (lambda) is an anonymous function that takes an argument, 𝑥, and returns an expression, 𝑒.
let 𝑥 = 𝑒₀ in 𝑒₁ means in expression, 𝑒₁, substitute 𝑒₀ wherever 𝑥 appears.
⊑ means the prior element is a subtype (informally - subclass) of the latter element.
𝛼 is a type variable.
∀ 𝛼.𝜎 is a type, ∀ (for all) argument variables, 𝛼, returning 𝜎 expression
∉ free(𝚪) means not an element of the free type variables of 𝚪 defined in the outer context. (Bound variables are substitutable.)
Everything above the line is the premise, everything below is the conclusion (Per Martin-Löf)
Precedence, by example
I have taken some of the more complex examples from the rules and inserted redundant parentheses that show precedence:
𝑥 : 𝜎 ∈ 𝚪 could be written (𝑥 : 𝜎) ∈ 𝚪
𝚪 ⊦ 𝑥 : 𝜎 could be written 𝚪 ⊦ (𝑥 : 𝜎)
𝚪 ⊦ let 𝑥 = 𝑒₀ in 𝑒₁ : 𝜏
is equivalently
𝚪 ⊦ ((let (𝑥 = 𝑒₀) in 𝑒₁) : 𝜏)
𝚪 ⊦ 𝜆𝑥.𝑒 : 𝜏→𝜏' is equivalently 𝚪 ⊦ ((𝜆𝑥.𝑒) : (𝜏→𝜏'))
Then, large spaces separating assertion statements and other preconditions indicates a set of such preconditions, and finally the horizontal line separating premise from conclusion brings up the end of the precedence order.
The Rules
What follows here are English interpretations of the rules, each followed by a loose restatement and an explanation.
Variable
Given 𝑥 is a type of 𝜎 (sigma), an element of 𝚪 (Gamma),
conclude 𝚪 asserts 𝑥 is a 𝜎.
Put another way, in 𝚪, we know 𝑥 is of type 𝜎 because 𝑥 is of type 𝜎 in 𝚪.
This is basically a tautology. An identifier name is a variable or a function.
Function Application
Given 𝚪 asserts 𝑒₀ is a functional type and 𝚪 asserts 𝑒₁ is a 𝜏
conclude 𝚪 asserts applying function 𝑒₀ to 𝑒₁ is a type 𝜏'
To restate the rule, we know that function application returns type 𝜏' because the function has type 𝜏→𝜏' and gets an argument of type 𝜏.
This means that if we know that a function returns a type, and we apply it to an argument, the result will be an instance of the type we know it returns.
Function Abstraction
Given 𝚪 and 𝑥 of type 𝜏 asserts 𝑒 is a type, 𝜏'
conclude 𝚪 asserts an anonymous function, 𝜆 of 𝑥 returning expression, 𝑒 is of type 𝜏→𝜏'.
Again, when we see a function that takes 𝑥 and returns an expression 𝑒, we know it's of type 𝜏→𝜏' because 𝑥 (a 𝜏) asserts that 𝑒 is a 𝜏'.
If we know 𝑥 is of type 𝜏 and thus an expression 𝑒 is of type 𝜏', then a function of 𝑥 returning expression 𝑒 is of type 𝜏→𝜏'.
Let variable declaration
Given 𝚪 asserts 𝑒₀, of type 𝜎, and 𝚪 and 𝑥, of type 𝜎, asserts 𝑒₁ of type 𝜏
conclude 𝚪 asserts let
𝑥=𝑒₀ in
𝑒₁ of type 𝜏
Loosely, 𝑥 is bound to 𝑒₀ in 𝑒₁ (a 𝜏) because 𝑒₀ is a 𝜎, and 𝑥 is a 𝜎 that asserts 𝑒₁ is a 𝜏.
This means if we have an expression 𝑒₀ that is a 𝜎 (being a variable or a function), and some name, 𝑥, also a 𝜎, and an expression 𝑒₁ of type 𝜏, then we can substitute 𝑒₀ for 𝑥 wherever it appears inside of 𝑒₁.
Instantiation
Given 𝚪 asserts 𝑒 of type 𝜎' and 𝜎' is a subtype of 𝜎
conclude 𝚪 asserts 𝑒 is of type 𝜎
An expression, 𝑒 is of parent type 𝜎 because the expression 𝑒 is subtype 𝜎', and 𝜎 is the parent type of 𝜎'.
If an instance is of a type that is a subtype of another type, then it is also an instance of that super-type - the more general type.
Generalization
Given 𝚪 asserts 𝑒 is a 𝜎 and 𝛼 is not an element of the free variables of 𝚪,
conclude 𝚪 asserts 𝑒, type for all argument expressions 𝛼 returning a 𝜎 expression
So in general, 𝑒 is typed 𝜎 for all argument variables (𝛼) returning 𝜎, because we know that 𝑒 is a 𝜎 and 𝛼 is not a free variable.
This means we can generalize a program to accept all types for arguments not already bound in the containing scope (variables that are not non-local). These bound variables are substitutable.
Putting it all together
Given certain assumptions (such as no free/undefined variables, a known environment, ) we know the types of:
- atomic elements of our programs (Variable),
- values returned by functions (Function Application),
- functional constructs (Function Abstraction),
- let bindings (Let Variable Declarations),
- parent types of instances (Instantiation), and
- all expressions (Generalization).
Conclusion
These rules combined allow us to prove the most general type of an asserted program, without requiring type annotations.