Excessive explanation, part twenty-four
We have four kinds of things in Exp: identifiers, function calls, lambdas and lets, and we have four rules in type inference. Finally, the last recursive rule of the type inference algorithm:
(iv) If e is let x = e1 in e2 then let W(A, e1) = (S1, I1) and ____ W(S1 Ax a {x:S1 A(I1), e2) = (S2, I2); then S = S2 S1 and I = I2.Again let's look at an example. Let's say we want to infer a type for
let double_it = Ix.(plus x x) in double_it foo
where we have plus as before, and foo:int in our set of assumptions. We begin by recursing on Ix.(plus x x) with the current set of assumptions. Note that we do not want to remove double_it from our set of assumptions if it is there because the expression might use double_it, meaning some other definition. If it does, then it uses the definition already in the assumptions; the "new" double_it is only in scope after the in.
Type inference tells us that the expression is of type int a' int, so we add an assumption double_it:int a' int to our set of assumptions, and compute the type of double_it foo under the new set of assumptions, which of course says that it is int. Since the type of a let expression is the type of the second expression, we're done.
The reason we need the closure is: suppose type inference tells us that the first expression is of type I^2a'I^2, and I^2 is free in A. (Remember, we always get a type, not a type scheme.) For the purposes of inferring the type of the right side of the in, we want the expression to have type scheme aI^2 I^2a'I^2.
NOTE: When any of the conditions above is not met W fails.
Though this is true, I think it would have been better to call out the two places in the algorithm where the failure can occur. They are in rule (i), which requires that an identifier have a type in the set of assumptions, and in rule (ii) which requires that type unification succeeds. Rules (iii) and (iv) never fail of their own accord; they only fail when the recursive application of W fails.
Next time: more sketch proofs!