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 e_{1}e_{2}then let W(A, e_{1}) = (S_{1}, τ_{1}) and W(S_{1}A, e_{2}) = (S_{2}, τ_{2}) and U(S_{2}τ_{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 `e`

. We recursively determine that _{1} e_{2}`e`

is some function type _{1}`τ`

and _{1}`e`

is its argument of type _{2}`τ`

. _{2}

Therefore `τ`

had better be a function type that takes a _{1}`τ`

and returns something of some type; call it β. Whatever β is must be the type of the function invocation expression. To find it, we unify _{2}`τ`

with _{1}`τ`

and we get a substitution that tells us what type to substitute for β. That’s our resulting type._{2} → β

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 `τ`

is _{1}`β → β`

— remember, we need a new type variable for the type `τ`

— and _{1}`τ`

is of course _{2}`int`

. Substitutions `S`

and _{1}`S`

are empty substitutions. We unify _{2}`β → β`

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.e_{1}then let β be a new type variable and W(A_{x}∪ {x:β}, e_{1}) = (S_{1}, τ_{1}); then S = S_{1}and τ = S_{1}β → τ_{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.

I really want to have a chat with you. I would be glad to get a better platform to chat you. thank you.