Excessive explanation, part eleven

Posted on by

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
[τ1/α1, ... ,τn/αn] or [τi/αi] and σ is a type-scheme, then S σ 
is the type-scheme obtained by replacing each free occurrence of 
αi in σ by τi, renaming the generic variables of σ 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 σ = ∀α α → (β → β), and the substitution S = [int/β]. β is free in σ, so S σ is ∀α α → (int → 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 necessary”? Well suppose we had σ as before but the substitution S = [α/β] and we intended that α to be a different (that is, free) α than the (bound) α in σ. We cannot in this case say that S σ is ∀α α → (α → α) because now every α is bound, which is not what we want. But we can say, hey, we’ll just trivially rename the bound α to γ and now the result of the substitution is ∀γ γ → (α → α) and all is well.

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

Notice that since S σ 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.

2 thoughts on “Excessive explanation, part eleven”

  1. Well, making substitutions on bound variables will generally look like this: Here’s a type scheme σ = ∀α α → (β → β), now let’s make substitution [α1/α] in α → (β → β) to obtain α1 → (β → β), and not quantify over any free type variable in σ; and so we obtain σ’ = α1 → (β → β), which is a generic instance of σ.

    The only thing we will need it for is to take a type scheme of a variable bound in a let-expression, and at every place it’s used inside the body of the let-expression, to substitute all bound variables for some fresh ones, and drop all quantifiers.

    Example:

    let f = λx. squareInt in (f 42) 3 + (f true) 4

    would evaluate to (squareInt 3) + (squareInt 4) = 25, but would it typecheck? If we assign type scheme σ to f (we can), we then type check application (f 42) with f having type scheme α1 → (β → β), 42 having type scheme α1 — α1 then will be substituted away for int, — and type check (f true) with f having type scheme α2 → (β → β), true having type scheme α2 — similarly, α2 will be then substituted for bool.

    So that’s where the let-polymorphism comes from: if we had α → (β → β) as a typescheme for f, then both 42 and true would both have to have the same type scheme α, but this requirement can’t be satisfied.

    Reply ↓

Leave a comment