Excessive explanation, part eleven

Last time we learned what is meant by "free" and "bound" variables both in the context of the Exp language and the type scheme language. So, substitutions:

If S is a substitution of types for type variables, often written[I1/I1, ... ,In/In] or [Ii/Ii] and If is a type-scheme, then S If is the type-scheme obtained by replacing each free occurrence of Ii in If by Ii, renaming the generic variables of If if necessary.

OK, syntactic concerns first. A substitution is written as a bracketed list of pairs, where the first element of the pair is a type (possibly a type variable, but definitely not a type scheme!) and the second is a type variable. We can think of a substitution as a function that takes a type scheme and produces a new type scheme, so (possibly confusingly) we use the same notation as we do for applying a function to an argument in the Exp language.

Let's look at an example. Suppose we have the type scheme If = aI I a' (I^2 a' I^2), and the substitution S = [int/I^2]. I^2 is free in If, so S If is aI I a' (int a' int).

Remember that we said last time that the free type variables were essentially type variables whose values were going to be provided by an outer context. Substitution of types for free variables is essentially a mechanism by which we can supply the value of the type variable.

Why "renaming the generic variables of If if necessary"? Well suppose we had If as before but the substitution S = [I/I^2] and we intended that I to be a different (that is, free) I than the (bound) I in If. We cannot in this case say that S If is aI I a' (I a' I) because now every I is bound, which is not what we want. But we can say, hey, we'll just trivially rename the bound I to I^3 and now the result of the substitution is aI^3 I^3 a' (I a' I) and all is well.

Then S If is called an "instance" of If;

Notice that since S If is itself a type scheme, we are saying that "instance of" is a relation on type schemes: given any two type schemes, we should be able to tell if one is an instance of another, by checking to see if there is any substitution on free variables of one that produces the other, modulo renaming of bound variables.

the notions of substitution and instance extend naturally to larger syntactic constructs containing type-schemes.

In later episodes we're going to have things that contain some number of type schemes, and we want to be able to say "apply this substitution to all of them" and produce a collection of instance type schemes.

Next time: we've seen that we can substitute any type for a free variable to get an instance of a schema. But this is insufficiently powerful; we need to be able to make substitutions on bound variables as well, eliminating the bound variable. Next time we'll see how to do that.