Excessive explanation, part sixteen

All right, so far we've mostly been talking about jargon and background information. Now we're actually going to get into the meat of the thing here. What we want is (1) a formal definition of what logical steps we are justified in using to determine what the type scheme of an expression is, when evaluated in a particular environment, and (2) an algorithm that produces a valid sequence of logical steps that ends in a type scheme for the expression.

How are we going to do that? First things first:

5 Type inferenceFrom now on we shall assume that A contains at most one assumptionabout each identifier x. Ax stands for removing any assumption aboutx from A. 

That notation is a bit vexing, but I hope it is clear.

For assumptions A, expression e and type-scheme If we write A a e:Ifif this instance may be derived from the following inference rules:

Note that this is a single turnstile. Last time we used the double turnstile to mean "from a collection of typed identifiers A, we can logically deduce that an expression e has type scheme If". It appears that we mean the same thing by the single turnstile, but does it?

The subtle difference is "may be derived from the following inference rules". The single turnstile means that we actually could produce a valid sequence of particular logical rules that get us to the type judgment.

But we're getting ahead of ourselves.

I started this series because I get the question quite frequently "I tried to read this paper and I couldn't understand the notation". In particular, people who have no experience with the standard notation for logical deductions have a bad reaction to this notation, but really it is very straightforward. The syntax is:

 KNOWN FACTSRULE: ------------ ( ADDITIONAL NOTES ) DEDUCTIONS 

So, stuff you know already goes on top. The name of the deduction rule goes on the left. The deduction that this rule allows you to make goes below the line, and any additional notes about the rule go in parens beside it.

The deductions of course are themselves just facts, so we can put a line below the deductions, and make even more deductions, and so on.

In our particular deductive system, all facts and deductions will be of the form A a e:If where again, A is a set of identifiers with types, e is an expression, and If is a type scheme. Remember, the turnstile means "there exists a sequence of logical deductions that justifies this typing judgment".

We call a sequence of logical deductions of this form a "derivation" of the result.

Let's start with the easiest rule; a rule so easy you might think it isn't necessary:

TAUT: ---------- ( x:If a A ) A a x:If

A "tautology" is a statement that is necessarily true by its form. "All X that are Y are Y" is a true statement no matter what we substitute for X and Y.

This rule has no facts at all above the line; tautologies are necessarily true irrespective of any particular facts. The notes on the side say that for this rule to apply, identifier x must have type scheme If in assumptions A. Given that, we logically deduce that, surprise, from assumptions A we can deduce that the expression x is an expression of type If.

So why do we need this rule? Because remember what the single turnstile means. The single turnstile means that we can deduce the type scheme of an identifier by producing a derivation: a sequence of logical deductions drawn from a specific set of rules. It's not enough to say that obviously, if an assumption is true then it is true. We have to have a rule that says that so that we can use that rule in a valid sequence of rules.

Let's look at a very slightly harder one.

 A a e:If INST: ---------- ( If > If' ) A a e:If'

The "instance" rule is: if we can logically deduce from assumptions A that e is of type If, then we can also logically deduce from assumptions A that e is of a smaller type If'.

For example, suppose we already know that A a x:aI(I a' I). Then with this rule we can deduce further that A a x:(int a' int). If we have enough evidence to deduce that x is a function from I to I for any type I then we have enough evidence to deduce that it a function from integers to integers.

This might seem a bit weird to you. Isn't this backwards?

If in C# we deduced that x was of type Mammal, we would not consider that to be evidence for a deduction that it was of a smaller type, Giraffe. We'd consider it to be of a larger type, Animal. However, there's another way to think of it: in C# if we deduced that x was of type Mammal, we would know that any Giraffe was a valid value for x, but not necessarily any Animal. That's the kind of inference we're doing here.

Next time we'll look at some more of the rules of this deductive system.