Excessive explanation, part eighteen
Over the last two episodes we gave the rules of the deductive system. The paper now gives an example of using that deductive system to derive the type of a complicated expression. The way it is laid out on the page makes it difficult to reproduce here and to annotate, so I'll take some small editorial liberties and "linearize" it a bit.
The following example of a derivation is organised as a tree, in which each node follows from those immediately above it by an inference rule.TAUT: -------------------- x:I a x:IABS: -------------------- a (Ix.x):I a' IGEN: -------------------- a (Ix.x):aI(I a' I) (1)
The (1) indicates that I'm going to use this fact that we've derived later.
Let's go through this carefully.
We start with a tautology, and therefore need no facts. We logically deduce that if we make the assumption that x:I we can logically deduce that x:I, unsurprisingly.
Now this becomes the fact that is fed into the next rule, ABS. Notice that below the second line we just have a turnstile with nothing to the left of it. This means that we can derive this conclusion from no assumptions whatsoever. Read the ABS rule carefully to make sure that you understand why this is.
This conclusion should make sense: we don't need any assumptions about the types of any variables to know that the identity lambda is a function from I to I.
And now perhaps you understand why I said last time that the GEN rule is a bit subtle. Here we have I free in the type, but not free in the set of assumptions. (The set of assumptions is empty, so plainly there are no free type variables in it!) It is perfectly valid for us to turn the free type variable into a quantified type variable, and deduce that yes, the identity function is a function from I to I for any I you care to name.
All right, let's start over. We won't use any of the facts we've just deduced in this next derivation. We'll start over from scratch.
TAUT: ----------------------------------- i:aI(I a' I) a i:aI(I a' I) INST: ----------------------------------- i:aI(I a' I) a i:(I a' I) a' (I a' I) (2)
The tautology says that if i is a function from I to I, then i is a function from I to I. I hope we agree that is true!
Now we can make that more specific if we want to by using the INST rule. Since that is true for any I, it is in particular true for the type (I a' I). These are different alphas than the alphas in aI(I a' I)! We could have just as easily said i:(I^2 a' I^2) a' (I^2 a' I^2), and it would have been more clear.
This is one of the things that is most confusing about academic papers: that they seem to deliberately use the same symbols to mean different things on the same line, like symbols are really expensive or something. I push back in code review when people do that in programming languages, and I wish they would not do it in papers either.
All right, so far we've deduced (1) (Ix.x) is aI(I a' I), and (2) if we have a proof that i is aI(I a' I) then we can use i somewhere that an (I a' I) a' (I a' I) is needed. Now let's make a third deduction starting again from nothing:
TAUT: ----------------------------------- i:aI(I a' I) a i:aI(I a' I) INST: ----------------------------------- i:aI(I a' I) a i:I a' I (3)
Wait, isn't that the derivation we just made over again?
Not quite. It's subtly different. Here we're saying that i:aI(I a' I) implies that i:I a' I. Again these are different alphas!
Now we can apply the COMB rule to facts (2) and (3). Go back and read the COMB rule and make sure you understand why facts (2) and (3) can be used here.
(2) (3)COMB: -------------------------- i:aI(I a' I) a i i:I a' I (4)
This says that if i is a function from I to I, then so is (i i).
Finally, we can put facts (1) and (4) together using the LET rule to derive the type of a complicated expression:
(1) (4)LET: --------------------------------- a (let i = (Ix.x) in i i):I a' I
Here we have an expression that combines the four kinds of expression in Exp: let, lambda, application and identifier. And we derive that from no assumptions whatsoever, we can figure out the type of this complex expression; it's a function from I to I.
This should not be a surprise: if you pass an identity function to itself, you get an identity function, and an identity function is of type I a' I. But it is pretty neat that we can make a set of logical deductions that gets us starting from nothing, and ending with this correct conclusion.
But how, you might ask, did we even come up with that derivation? What we need is an algorithm that takes an expression and produces a derivation that the expression is of a particular type; such an algorithm is a type inference algorithm!
Next time we'll discuss the "semantic soundness" of the algorithm, and give a sketch proof.