8.2 The Typing Relation

 < Free Open Study > 



8.2 The Typing Relation

The typing relation for arithmetic expressions, written[2] "t : T", is defined by a set of inference rules assigning types to terms, summarized in Figures 8-1 and 8-2. As in Chapter 3, we give the rules for booleans and those for numbers in two different figures, since later on we will sometimes want to refer to them separately.


Figure 8-1: Typing Rules for Booleans (B)


Figure 8-2: Typing Rules for Numbers (NB)

The rules T-TRUE and T-FALSE in Figure 8-1 assign the type Bool to the boolean constants true and false. Rule T-IF assigns a type to a conditional expression based on the types of its subexpressions: the guard t1 must evaluate to a boolean, while t2 and t3 must both evaluate to values of the same type. The two uses of the single metavariable T express the constraint that the result of the if is the type of the then- and else- branches, and that this may be any type (either Nat or Bool or, when we get to calculi with more interesting sets of types, any other type).

The rules for numbers in Figure 8-2 have a similar form. T-ZERO gives the type Nat to the constant 0. T-SUCC gives a term of the form succ t1 the type Nat, as long as t1 has type Nat. Likewise, T-PRED and T-ISZERO say that pred yields a Nat when its argument has type Nat and iszero yields a Bool when its argument has type Nat.

8.2.1 Definition

Formally, the typing relation for arithmetic expressions is the smallest binary relation between terms and types satisfying all instances of the rules in Figures 8-1 and 8-2. A term t is typable (or well typed) if there is some T such that t : T.

When reasoning about the typing relation, we will often make statements like "If a term of the form succ t1 has any type at all, then it has type Nat. The following lemma gives us a compendium of basic statements of this form, each following immediately from the shape of the corresponding typing rule.

8.2.2 Lemma [Inversion of the Typing Relation]

  1. If true : R, then R = Bool.

  2. If false : R, then R = Bool.

  3. If if t1 then t2 else t3 : R, then t1 : Bool, t2 : R, and t3 : R.

  4. If 0 : R, then R = Nat.

  5. If succ t1 : R, then R = Nat and t1 : Nat.

  6. If pred t1 : R, then R = Nat and t1 : Nat.

  7. If iszero t1 : R, then R = Bool and t1 : Nat.

Proof: Immediate from the definition of the typing relation.

The inversion lemma is sometimes called the generation lemma for the typing relation, since, given a valid typing statement, it shows how a proof of this statement could have been generated. The inversion lemma leads directly to a recursive algorithm for calculating the types of terms, since it tells us, for a term of each syntactic form, how to calculate its type (if it has one) from the types of its subterms. We will return to this point in detail in Chapter 9.

8.2.3 Exercise [ ]

Prove that every subterm of a well-typed term is well typed.

In §3.5 we introduced the concept of evaluation derivations. Similarly, a typing derivation is a tree of instances of the typing rules. Each pair (t, T) in the typing relation is justified by a typing derivation with conclusion t : T. For example, here is the derivation tree for the typing statement "if iszero 0 then 0 else pred 0 : Nat":

click to expand

In other words, statements are formal assertions about the typing of programs, typing rules are implications between statements, and derivations are deductions based on typing rules.

8.2.4 Theorem [Uniqueness of Types]

Each term t has at most one type. That is, if t is typable, then its type is unique. Moreover, there is just one derivation of this typing built from the inference rules in Figures 8-1 and 8-2.

Proof: Straightforward structural induction on t, using the appropriate clause of the inversion lemma (plus the induction hypothesis) for each case.

In the simple type system we are dealing with in this chapter, every term has a single type (if it has any type at all), and there is always just one derivation tree witnessing this fact. Later one.g., when we get to type systems with subtyping in Chapter 15both of these properties will be relaxed: a single term may have many types, and there may in general be many ways of deriving the statement that a given term has a given type.

Properties of the typing relation will often be proved by induction on derivation trees, just as properties of the evaluation relation are typically proved by induction on evaluation derivations. We will see many examples of induction on typing derivations, beginning in the next section.

[2]The symbol Î is often used instead of :.



 < Free Open Study > 



Types and Programming Languages
Types and Programming Languages
ISBN: 0262162091
EAN: 2147483647
Year: 2002
Pages: 262

flylib.com © 2008-2017.
If you may any questions please contact us: flylib@qtcs.net