29.2 Definitions

 < Free Open Study > 



29.2 Definitions

Figure 29-1 presents the complete definition of a core lambda-calculus with type operators. At the term level, this calculus includes just the variables, abstraction, and application of the simply typed lambda-calculus (for this reason, it is called the simply typed lambda-calculus with type operators). The type level includes the usual arrow types and type variables, plus operator abstraction and application. Quantified types like "X.T are omitted from this system; we return to them in detail in Chapter 30.

The presentation of the system extends the framework of the simply typed lambda-calculus in three ways. First, we add a collection of rules of kinding, which specify how type expressions can be combined to yield new type expressions. We write Г T :: K for "type T has kind K in context Г." Note the similarity between these kinding rules and the typing rules of the original simply typed lambda-calculus (Figure 9-1).

Second, whenever a type T appears in a term (as in λx:T.t), we must check that T is well formed. This involves adding a new premise to the old T-ABS rule that checks Г T :: *. Note that T must have exactly kind *i.e., it must be a proper typesince it is being used to describe the values that the term-variable x may range over. The typing rules maintain the invariant that, whenever we can derive a statement Г t : T, the statement Г T :: * is also derivable (as long as all the types appearing in the context are well kinded). This point is discussed in more detail in §30-3.

Third, we add a collection of rules for the definitional equivalence relation between types. We write S T for "types S and T are definitionally equivalent." This relation is quite similar to the reduction relation at the level of terms. The effect of definitional equivalence on typing is captured by the new T-EQ rule. The kinding premise (which was elided when we discussed the rule in the previous section) maintains the invariant mentioned above, that "typable terms always have kindable types." Note the similarity of this rule to the rule of subsumption (T-Sub) i n systems with subtyping.

The basic metatheoretic properties of this system require a little work to develop, since the type equivalence relation introduces significant flexibility in the "shapes" of the types assigned to terms. We postpone the development of this theory to Chapter 30.



 < 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