Last time we gave the base case of our recursive algorithm. Today, two of the three non-base cases.

But before we get to them, another annoyance.

The first time I read this algorithm carefully I got to the second step of the inference algorithm and said to myself wait, that cannot possibly be right. I stared at that thing for probably fifteen minutes trying to make sense of it before realizing that there is a footnote at the bottom of the page that says

There are obvious typographic errors in parts (ii) and (iv)
which are in the original publication. I have left the correction
of these as an easy exercise for the reader.

Now, I am hardly one to talk as I leave stuff as exercises for the reader all the time on Stack Overflow. But really? There’s a typo in the paper, you know about it, and you leave the typo in the paper as a challenge? VEXING.

I will remove the typos in my presentation of the algorithm. Anyone who wants the frankly rather dubious challenge of attempting to fix the typos themselves can go read the original paper.

Onwards!

(ii) 
If e is e1 e2 then let W(A, e1) = (S1, τ1) and W(S1 A, e2) = (S2, τ2) 
and U(S2 τ1, τ2 → β) = V where β is new; then S = V S2 S1 and τ = V β.

Let’s unpack this, starting with just the types.

We have a function application e1 e2. We recursively determine that e1 is some function type τ1 and e2 is its argument of type τ2.

Therefore τ1 had better be a function type that takes a τ2 and returns something of some type; call it β. Whatever β is must be the type of the function invocation expression. To find it, we unify τ1 with τ2 → β and we get a substitution that tells us what type to substitute for β. That’s our resulting type.

Let’s take a look at a trivial example. Suppose our assumptions are x:int and i:∀α α→α, and our expression to be inferred is i x. We recursively apply type inference to determine that τ1 is β → β — remember, we need a new type variable for the type τ1 — and τ2 is of course int. Substitutions S1 and S2 are empty substitutions. We unify β → β with int → γ — again we need a new type variable used nowhere else — and get the subtitution V = [β/int, γ/int]. Our result type is V γ which is obviously int.

We can deduce that passing an int to an identity function returns int; awesome.

(iii) 
If e is λx.e1 then let β be a new type variable and
W(Ax ∪ {x:β}, e1) = (S1, τ1); then S = S1 and τ = S1 β → τ1. 

Let’s think of an example. Suppose we have an assumption plus:int → int → int and the expression λx.(plus x x). So we make a new assumption x:β, and run algorithm W on plus x x. That tells us that the expression is of type int, and also returns a substitution [int/β].

The type of the lambda is therefore [int/β](β → int), which obviously is int → int.

Next time: inferring the type of a “let” expression.