Excessive explanation, part twenty-three

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 correctionof 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, I1) and W(S1 A, e2) = (S2, I2) and U(S2 I1, I2 a' I^2) = V where I^2 is new; then S = V S2 S1 and I = V I^2.

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

We have a function application e₁ e₂. We recursively determine that e₁ is some function type I₁ and e₂ is its argument of type I₂.

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

Let's take a look at a trivial example. Suppose our assumptions are x:int and i:aI Ia'I, and our expression to be inferred is i x. We recursively apply type inference to determine that I₁ is I^2 a' I^2 - remember, we need a new type variable for the type I₁ - and I₂ is of course int. Substitutions S₁ and S₂ are empty substitutions. We unify I^2 a' I^2 with int a' I^3 - again we need a new type variable used nowhere else - and get the subtitution V = [I^2/int, I^3/int]. Our result type is V I^3 which is obviously int.

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

(iii) If e is Ix.e1 then let I^2 be a new type variable andW(Ax a {x:I^2}, e1) = (S1, I1); then S = S1 and I = S1 I^2 a' I1. 

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

The type of the lambda is therefore [int/I^2](I^2 a' int), which obviously is int a' int.

Next time: inferring the type of a "let" expression.