How to read inference rules

The notation used is probably one of the largest barriers of entry to type inference papers, but it is rarely explained explicitly, so… I’m going to do just that!

For starters, inference rules are really nothing more than implications. The inference rule

$$\frac{A}{B}(\text{Name})$$

really just means “if A then B”. These are usually given a name (in this case, creatively, $\text{Name}$) to make it easier to refer to them in the rest of the paper.

Now, even though these are technically just implications, it’s usually not a great idea to read them from top to bottom. Inference rules denote relations, but it usually usually makes more sense to read them as (possibly non-deterministic) functions. For example, a judgement for typing function application might look like this. (where $\mathrm{\Gamma }⊢e:\tau$ means “In a context $\mathrm{\Gamma }$, the type of an expression $e$ is infered to $\tau$”)

$$\frac{\mathrm{\Gamma }⊢e_1\hspace{0.25em} :\hspace{0.25em} {\tau }_1\to {\tau }_2\hspace{0.25em} \hspace{0.25em} \hspace{0.25em} \mathrm{\Gamma }⊢e_2\hspace{0.25em} :\hspace{0.25em} {\tau }_1}{\mathrm{\Gamma }⊢e_1(e_2)\hspace{0.25em} :\hspace{0.25em} {\tau }_2}(\text{App})$$

If $e_1$ has type ${\tau }_1\to {\tau }_2$ in a context $\mathrm{\Gamma }$ and $e_2$ has type ${\tau }_1$ in $\mathrm{\Gamma }$, then $e_1(e_2)$ has type ${\tau }_2$ in $\mathrm{\Gamma }$

In order to infer a type for $e_1(e_2)$ in a context $\mathrm{\Gamma }$, one first needs to infer a type for $e_1$ with shape ${\tau }_1\to {\tau }_2$ in $\mathrm{\Gamma }$. Now $e_2$ also needs to infer to type ${\tau }_1$ in $\mathrm{\Gamma }$, so that the result (i.e. the type of $e_1(e_2)$) is ${\tau }_2$.

Read this way, the inference rule maps very closely onto an actual implementation! Seriously, compare the corresponding pseudocode to that second description

infer Γ (App e1 e2) =
    let (τ1 -> τ2) = infer Γ e1
    let τ3 = infer Γ e2
    unify τ1 τ3
    return τ2

The only major difference between this code (which skips error handling, just like inference rules) and the inference rule is that the fact that the type of $e_2$ needs to be equal to ${\tau }_1$ is explicit in the code (unify τ1 τ3).

Reading off the algorithm like this is possible if the inference rules are syntax directed, i.e. if there is only ever a single rule that might match on a given expression. This is not always the case, so sometimes it’s better to imagine non-deterministically choosing the correct rule to apply, rather than just pattern matching.

And that’s… pretty much all you need to know to read inference rules!

There are a few common conventions in type systems that might be a bit surprising, so let’s go over those as well

Environments and extension

Type inference needs an environment to keep track of the types of variables. This is usually called $\mathrm{\Gamma }$ and extended as $\mathrm{\Gamma },x\hspace{0.25em} :\hspace{0.25em} \tau$.

For example, this inference rule for (annotated) let bindings checks $e_2$ under the environment Γ, extended with the binding $x\hspace{0.25em} :\hspace{0.25em} {\tau }_1$.

$$\frac{\mathrm{\Gamma }⊢e_1\hspace{0.25em} :\hspace{0.25em} {\tau }_1\hspace{0.25em} \hspace{0.25em} \hspace{0.25em} \mathrm{\Gamma },x\hspace{0.25em} :\hspace{0.25em} {\tau }_1⊢e_2\hspace{0.25em} :\hspace{0.25em} {\tau }_2}{\mathrm{\Gamma }⊢\mathbf{\text{let}}x\hspace{0.25em} :\hspace{0.25em} {\tau }_1=e_1\mathbf{\text{in}}{e}_2\hspace{0.25em} :\hspace{0.25em} {\tau }_2}\text{Let}$$

Extracting information from the environment is achieved through “pattern matching” on the environment, for example in this inference rule for variables.

$$\frac{}{\mathrm{\Gamma },x\hspace{0.25em} :\hspace{0.25em} \tau ⊢x\hspace{0.25em} :\hspace{0.25em} \tau }\text{Var}$$

Unification variables

Unification variables don’t exist in theoretical type systems, but they still map very directly onto a similar concept. Instead of generating a fresh unification variable, inference rules just “guess” a new type (they’re relations, remember?).

For example, this typing rule for (unannotated) lambdas just pulls the type $\tau$ out of thin air.

$$\frac{\mathrm{\Gamma },x\hspace{0.25em} :\hspace{0.25em} \tau ⊢e\hspace{0.25em} :\hspace{0.25em} {\tau }_1}{\mathrm{\Gamma }⊢\lambda x\to e\hspace{0.25em} :\hspace{0.25em} \tau \to {\tau }_1}\text{Lambda}$$

Lists

Something you will see pretty often in papers by Simon Peyton Jones are lists that are represented by an overline. E.g. the syntax for uncurried function application might be $e_1(\bar{e})$, where $\bar{e}$ consists of 0 or more expressions.

Skolems

Similarly, skolems don’t exist as a separate concept. Instead, “unbound” type variables are treated as skolems, although these obviously cannot conflict with any other type variables in scope! In an implementation, this would be achieved by generating a fresh skolem, but in inference rules, this is expressed by the side condition that the type variable should not occur “free in the environment”, written $a\mathrm{\notin }\text{ftv}(\mathrm{\Gamma })$, where ftv denotes the set of free type variables (= skolems) in $\mathrm{\Gamma }$.

For example, a rule for let bindings with polymorphic types (that need to be skolemized) might look like this

$$\frac{\mathrm{\Gamma }⊢e_1\hspace{0.25em} :\hspace{0.25em} {\tau }_1\hspace{0.25em} \hspace{0.25em} \hspace{0.25em} \bar{a}\mathrm{\notin }\text{ftv}(\mathrm{\Gamma })\hspace{0.25em} \hspace{0.25em} \hspace{0.25em} \mathrm{\Gamma },x\hspace{0.25em} :\hspace{0.25em} \mathrm{\forall }\bar{a}\mathrm{.}{\tau }_1⊢e_2\hspace{0.25em} :\hspace{0.25em} {\tau }_2}{\mathrm{\Gamma }⊢\mathbf{\text{let}}x\hspace{0.25em} :\hspace{0.25em} \mathrm{\forall }\bar{a}\mathrm{.}{\tau }_1=e_1\mathbf{\text{in}}{e}_2\hspace{0.25em} :\hspace{0.25em} {\tau }_2}$$

Where to go from here

Great, with a little practice, you should be able to read inference rules now! I would recommend you read Practical type inference for higher rank types, which is a great, relatively beginner friendly paper about type inference that even contains a full implementation at the end! (And despite the name, is not just about higher rank types).