Excessive explanation, part seventeen

Last time we discussed the syntax for logical deductions that is common in academia: facts above, deductions below, a line between them. We discussed the tautology rule and the instance rule. Today: more rules.

 A a e:If GEN: ------------ ( I not free in A ) A a e:aIIf 

This is the "generic" rule: if you have some fact about an expression, then that fact is also true when quantified over all types. For example, if we know that A a e:inta'int then we also know that we can make up a type variable I, and no matter what value we give the type variable, the expression is still of that type.

Exercise: Do you see why I must not be free? Suppose I is free in A; can you find an example of how the GEN rule produces an invalid conclusion if we were to allow this?

Now, you might say that it is obvious that if something is true, then it is also true even when we give any old value to a type variable that is not even involved. And yes, that's obvious. It's good that it is obvious! All these rules should be obviously correct.

What I just said was a bit of an "intuition pump", because it is actually a bit subtle. Do you see why? Just because I is not free in A does not imply that I is not free in If! So why is it legal to make this quantification over a variable free in If only if it is not free in A? Ponder that briefly.

If after pondering it was not clear, don't worry. It is a lot easier to understand these subtleties by looking at a realistic example, which we will do next time on FAIC.

In our next rule we have two facts above the line, which we have not yet seen:

 A a e:I' a' I A a e':I' COMB: ---------------------------- A a (e e'):I

If we have a function from I' to I, and an expression of type I', then the expression "pass the value to the function" is of type I.

Just like in C#: if we have a function F that takes a string and returns an int, and e is an expression of type string, then F(e) is an expression of type int. Easy peasy.

If you think we need to have at least one rule for every possible kind of expression in Exp, you're right! Fortunately there are only four kinds of expressions: identifiers, function calls, lambdas, and let expressions. We've already seen the first two, so it should be no surprise that the next rule is for lambdas.

This rule is a little more complicated:

 Ax a { x:I' } a e:IABS: --------------------- A a (Ix.e):I' a' I

Let's sort this one out carefully.

Suppose we have a set of assumptions A that might or might not contain a judgment for identifier x. If it does, remove it. To that, add a judgment that says that x is of type I'. And suppose from that set of assumptions we can deduce that expression e is of type I.

That implies that from assumptions A, we can deduce that Ix.e is a function from I' to I.

Why do we need to say A_x a { x:I' } instead of simply A a { x:I' }? Because we said at the beginning of this chapter that all sets of assumptions would contain at most one judgment for any identifier. But A a { x:I' } might contain two judgments for x, if A already contains a judgment for x.

Leaving aside the mechanisms of adding and removing judgments from a set of assumptions, I hope the rule is sensible. If knowing that x is of type I' allows us to deduce that e is of type I, then Ix.e can be used anywhere we need a function from I' to I.

Notice that it does not matter whether A contains a judgment for x or not. If it does not, fine. If it does, then who cares? Ix.e defines a new variable x that shadows any existing x in the environment.

We've seen rules for identifiers, function applications and lambdas. There is only one rule left, which describes how typing works for let expressions. Again, it takes two facts and produces a third.

 A a e:If Ax a { x:If } a e':ILET: ----------------------------------- A a (let x = e in e'):I

This is very similar to the rule for lambdas. If e is of type scheme If, and identifier x being of type scheme If implies that e' is of type I, then the type of the corresponding let expression is I. Again, we need to do a little scut work to make sure that the identifier x is treated properly, but I hope the rule is clear.

These are the only rules of the deductive system. Next time we'll go through an example of how to use the rules to start with nothing, and from that deduce some facts about identity functions.