Excessive explanation, part twenty-two
All right, at long last, the type inference algorithm itself!
Algorithm W.W(A, e) = (S, I) where
This is just a reminder that what we're doing here is taking a set of assumptions that give types to identifiers, and an expression that might contain some of those identifiers, and from that we deduce a substitution on the identifier types, and a type for the expression.
This reminder however does not remind us that the algorithm can also tell us that there is no type that can be inferred for the expression given those assumptions; properly we ought to be saying that we produce a substitution and a type, or an error.
(i) If e is x and there is an assumption x:aI1, ... ,In I' in A then S = Id and I = [I^2i/Ii]I' where the I^2i are new. Of course this is the identity (empty) substitution, not the set Id of identifiers.
Just a small rant here. First off, we already have a notation for substitutions which is a list of I/I pairs in square brackets. The notation [ ] is a perfectly concise way to describe the identity type substitution. So why did the authors chose to re-use "Id" to mean "the empty substitution" when it already means "the set of identifiers", thereby prompting them to insert a note to the effect that this notation is confusing? In code reviews I tell people to never comment confusing code; fix it so it is not confusing! A two-character fix here would ensure that the clarifying note is unneeded.
I also cannot fathom why we've gone from notating a type scheme with multiple bindings as aI1"In at the beginning of the paper to aI1, " ,In at the end. Before there were no commas; now there are commas. Small things like this are an impediment to understanding. Attention to detail is important in a paper, and in code.
Rant over. More rants next time!
As you might have guessed, this is going to be a recursive algorithm. Therefore we start with the simplest possible base case. If the expression we're trying to deduce is an identifier whose type scheme is given in the assumptions, then we just use that type.
There are a few subtleties to consider carefully though.
If we have expression x and an assumption like x:int then it is easy; x is deduced to be int. Similarly if we have a free type variable; if we have x:I then we simply deduce that x is, of course, I.
The tricky case is where we have an assumption that x is quantified. Maybe we have assumption x:aI1I2 I1a'I2. We do not want to deduce that the type of the expression is the type I1a'I2 because I1 or I2 might appear free elsewhere, and we don't want to confusingly associate the type of x with those free variables. We need to make new free type variables, so we deduce that the type of x is I^21a'I^22 where these are brand new not previously used type variables.
When I joined the C# language design team the major design work for LINQ was done but there were still a few details left. The existing generic method type inference algorithm was insufficient to deal with a world that included lambdas, so we needed to fix it up. Complicating matters was the fact that the existing code that did type inference was difficult to follow and did not bear a very close resemblance to the specification in its action. (Its results were fine, but it was hard to look at the code and see how the specification had been translated into code.)
Given that we were making major changes to the algorithm, I decided to scrap the existing implementation and start fresh with an implementation that was (1) very clearly implementing exactly what was in the specification, so that as we tweaked the spec during the design it would be clear what needed to change in the implementation, and (2) written in a style similar to how I would want to write the same algorithm in C#; I was anticipating the future existence of Roslyn and I wanted to make that transition smooth.
And I really did start from scratch, including rewriting the type unification and substitution algorithms from scratch as well.
The first major mistake that got caught after I checked it in was:
void M<T, U>(T t, U u, bool flag) { if (flag) M(flag, t, false);}What types should be inferred on the recursive call? Plainly this should be the same as M<bool, T>(flag, t, false);. My first implementation deduced that this was M<bool, bool>. You can probably guess why. The type inferencer deduced that T is bool and U is T, and the substituter said OK, if T is bool and U is T then U is also bool!
The T that is being substituted in for U is the T of the outer invocation of M. The T of the inner invocation of M is a different T entirely, but I used the same object to represent both! When you are implementing these algorithms you have to be super careful about not granting referential identity to things that look the same but are in fact just placeholders for different activations.
Fortunately we had a massive set of test cases which found my bug in short order.
Next time we'll look at the non-base cases, and some irritating typos.