9.2 The Typing Relation

< Free Open Study >

In order to assign a type to an abstraction like λx.t, we need to calculate what will happen when the abstraction is applied to some argument. The next question that arises is: how do we know what type of arguments to expect? There are two possible responses: either we can simply annotate the λ-abstraction with the intended type of its arguments, or else we can analyze the body of the abstraction to see how the argument is used and try to deduce, from this, what type it should have. For now, we choose the first alternative. Instead of just λx.t, we will write λx:T₁.t₂, where the annotation on the bound variable tells us to assume that the argument will be of type T₁.

In general, languages in which type annotations in terms are used to help guide the typechecker are called explicitly typed. Languages in which we ask the typechecker to infer or reconstruct this information are called implicitly typed. (In the λ-calculus literature, the term type-assignment systems is also used.) Most of this book will concentrate on explicitly typed languages; implicit typing is explored in Chapter 22.

Once we know the type of the argument to the abstraction, it is clear that the type of the function's result will be just the type of the body t₂, where occurrences of x in t₂ are assumed to denote terms of type T₁. This intuition is captured by the following typing rule:

Since terms may contain nested λ-abstractions, we will need, in general, to talk about several such assumptions. This changes the typing relation from a two-place relation, t : T, to a three-place relation, Г ⊢ t : T, where Г is a set of assumptions about the types of the free variables in t.

Formally, a typing context (also called a type environment) Г is a sequence of variables and their types, and the "comma" operator extends Г by adding a new binding on the right. The empty context is sometimes written /, but usually we just omit it, writing ⊢ t : T for "The closed term t has type T under the empty set of assumptions."

To avoid confusion between the new binding and any bindings that may already appear in Г, we require that the name x be chosen so that it is distinct from the variables bound by Г. Since our convention is that variables bound by λ-abstractions may be renamed whenever convenient, this condition can always be satisfied by renaming the bound variable if necessary. Г can thus be thought of as a finite function from variables to their types. Following this intuition, we write dom(Г) for the set of variables bound by Г.

The rule for typing abstractions has the general form

where the premise adds one more assumption to those in the conclusion.

The typing rule for variables also follows immediately from this discussion: a variable has whatever type we are currently assuming it to have.

The premise x:T Î Г is read "The type assumed for x in Г is T.

Finally, we need a typing rule for applications.

If t₁ evaluates to a function mapping arguments in T₁₁ to results in T₁₂ (under the assumption that the values represented by its free variables have the types assumed for them in Г), and if t₂ evaluates to a result in T₁₁, then the result of applying t₁ to t₂ will be a value of type T₁₂.

The typing rules for the boolean constants and conditional expressions are the same as before (Figure 8-1). Note, though, that the metavariable T in the rule for conditionals

can now be instantiated to any function type, allowing us to type conditionals whose branches are functions:^[2]

   if true then (λx:Bool. x) else (λx:Bool. not x); ▸ (λx:Bool. x) : Bool → Bool

These typing rules are summarized in Figure 9-1 (along with the syntax and evaluation rules, for the sake of completeness). The highlighted regions in the figure indicate material that is new with respect to the untyped lambda-calculus-both new rules and new bits added to old rules. As we did with booleans and numbers, we have split the definition of the full calculus into two pieces: the pure simply typed lambda-calculus with no base types at all, shown in this figure, and a separate set of rules for booleans, which we have already seen in Figure 8-1 (we must add a context Г to every typing statement in that figure, of course).

We often use the symbol λ→ to refer to the simply typed lambda-calculus (we use the same symbol for systems with different sets of base types).

9.2.1 Exercise [⋆]

The pure simply typed lambda-calculus with no base types is actually degenerate, in the sense that it has no well-typed terms at all. Why?

Instances of the typing rules for λ→ can be combined into derivation trees, just as we did for typed arithmetic expressions. For example, here is a derivation demonstrating that the term (λx:Bool.x) true has type Bool in the empty context.

9.2.2 Exercise [⋆ ↛]

Show (by drawing derivation trees) that the following terms have the indicated types:

f:Bool→Bool ⊢ f (if false then true else false) : Bool
f:Bool→Bool ⊢ λx:Bool. f (if x then false else x) : Bool→Bool

9.2.3 Exercise [⋆]

Find a context Г under which the term f x y has type Bool. Can you give a simple description of the set of all such contexts?

^[2]Examples showing sample interactions with an implementation will display both results and their types from now on (when they are obvious, they will be sometimes be elided).

< Free Open Study >