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