22.2 Two Views of Type Variables

< Free Open Study >

Suppose that t is a term containing type variables and Г is an associated context (possibly also containing type variables). There are two quite different questions that we can ask about t:

"Are all substitution instances of t well typed?" That is, for every σ, do we have σГ ⊢ σt :T for some T?
"Is some substitution instance of t well typed?" That is, can we find a σ such that σГ ⊢ σt : T for some T?

According to the first view, type variables should be held abstract during typechecking, thus ensuring that a well-typed term will behave properly no matter what concrete types are later substituted for its type variables. For example, the term

   λf:X→X. λa:X. f (f a);

has type (X→X)→X→X, and, whenever we replace X by a concrete type T, the instance

   λf:T→T. λa:T. f (f a);

is well typed. Holding type variables abstract in this way leads us to parametric polymorphism, where type variables are used to encode the fact that a term can be used in many concrete contexts with different concrete types. We will return to parametric polymorphism later in this chapter (in §22.7) and, in more depth, in Chapter 23.

On the second view, the original term t may not even be well typed; what we want to know is whether it can be instantiated to a well typed term by choosing appropriate values for some of its type variables. For example, the term

   λf:Y. λa:X. f (f a);

is not typable as it stands, but if we replace Y by Nat→Nat and X by Nat, we obtain

   λf:Nat→Nat. λa:Nat. f (f a);

of type (Nat→Nat)→Nat→Nat. Or, if we simply replace Y by X→X, we obtain the term

   λf:X→X. λa:X. f (f a);

which is well typed even though it contains variables. Indeed, this term is a most general instance of λf:Y. λa:X. f (f a), in the sense that it makes the smallest commitment about the values of type variables that yields a well-typed term.

Looking for valid instantiations of type variables leads to the idea of type reconstruction (sometimes called type inference), in which the compiler helps fill in type information that has been left out by the programmer. In the limit, we may, as in ML, allow the programmer to leave out all type annotations and write in the syntax of the bare, untyped lambda-calculus. During parsing, we annotate each bare lambda-abstraction λx.t with a type variable, λx:X.t, choosing X to be different from the type variables on all the other abstractions in the program. We then perform type reconstruction to find the most general values for all these variables that make the term typecheck. (This story becomes a little more complicated in the presence of ML's let-polymorphism; we return to this in §22.6 and §22.7.)

To formalize type reconstruction, we will need a concise way of talking about the possible ways that type variables can be substituted by types, in a term and its associated context, to obtain a valid typing statement.^[2]

Figure 22-1: Constraint Typing Rules

22.2.1 Definition

Let Гbe a context and t a term. A solution for (Г,t) is a pair (σ T) such that σГ ⊢ σ t : T.

22.2.2 Example

Let Г = f:X, a:Y and t = f a. Then

     ([X ↦ Y→Nat], Nat)         ([X ↦ Y→Z], Z)     ([X ↦ Y→Z, Z ↦ Nat], Z)    ([X ↦ Y→Nat→Nat], Nat→Nat)     ([X ↦ Nat→Nat, Y ↦ Nat], Nat→Nat)

are all solutions for (Г, t).

22.2.3 Exercise [⋆ ↛]

Find three different solutions for the term

   λx:X. λy:Y. λz:Z. (x z) (y z).

in the empty context.

^[2]There are other ways of setting up these basic definitions. One is to use a general mechanism called existential unificands, due to Kirchner and Jouannaud (1990), instead of all the individual freshness conditions in the constraint generation rules in Figure 22-1. Another possible improvement, employed by Rémy (1992a, 1992b, long version, 1998, Chapter 5), is to treat typing statements themselves as unificands; we begin with a triple (Г, t,T), where all three components may contain type variables, and look for substitutions σ such that σГ ⊢ σ(t) : σ(T), i.e., substitutions that unify the schematic typing statement Г ⊢ t : T.

< Free Open Study >