Jens Palsberg Sep 24 1999 Lecture Note Types Contents 1 Introduction 2 2 Simple Types 3 3 Type Soundness 6 4 Recursive Types 12 5 Subtyping 17 6 Decision Procedure for Subtyping 19 7 First Order Unification 21 8 Typed Assembly Language 25 1 1 Introduction What is a Type A type is an invariant For example the Java declaration int v specifies that v may only contain integer values in a certain range Why Types An untyped program may be Unreadable Types provide documentation Well typed programs are more readable Unreliable Types provide a safety guarantee Well typed programs cannot go wrong Inefficient Types enable optimizations Well typed programs are faster 2 2 Simple Types Our example language is a calculus where the only two kinds of data are functions and integers The language is generated by the following grammar e Expression e x x e e1 e2 c succ e x V ar infinite set of variables c IntegerConstant We will use the standard convention that when writing x e then e is everything until the next or until the end of the whole term The slogan is the body of a extends as long as possible We will also use the standard convention that e1 e2 e3 should be grouped as e1 e2 e3 An expression is closed if it does not contain free variables We need two kinds of type function types and an integer type Types are generated from the grammar t t1 t2 Int Such types are called simple types The basic idea is that we can assign natural types to expressions for example 0 Int x succ x Int Int Notice that there are infinitely many types Notice also that each type can be viewed as a tree the syntax tree of the type A type environment is a partial function with finite domain which maps elements of V ar to types We use A to range over type environments We use to denote the type environment with empty domain We use A x t to denote a partial function which maps x to t and maps y where y 6 x to A y Let us now consider a formal system for assigning types to terms If e is a term t is a type and A is a type environment then the judgment A e t means that e has the type t in the environment A Formally this holds when the judgment is derivable by a finite derivation tree using the following five rules 3 A x t A x t 1 A x s e t A x e s t 2 A e1 s t A e2 s A e1 e2 t 3 A 0 Int 4 A e Int A succ e Int 5 An expression e is well typed if there exist A t such that A e t is derivable Notice that there is one rule for each of the five constructs in the language The hypotheses if any are written above the line and the conclusion is written below the line Two of the rules have no hypotheses so we call them axioms We can now use these rules to derive the typings of 0 and x succ x from above The first case is easy 0 Int The judgment is indeed an instance of the axiom for 0 The second case requires the use of the rules for abstraction succ and variable x Int x Int x Int succ x Int x succ x Int Int Here are some more examples of the use of the five rules The identity function x Int x Int x x Int Int The apply function f s t x s f s t f s t x s x s f s t x s f x t f s t x f x s t f x f x s t s t 4 The K combinator x s y t x s x s y x t s x y x s t s The following term does not have a simple type succ x e The problem is that x e is not an integer If we try to build a type derivation then may start with Rule 5 x e Int succ x e Int There is no rule with which we can derive the hypothesis x e Int so we conclude that succ x e does not have a simple type 5 3 Type Soundness A type system for a programming language is sound if well typed programs cannot cause type errors A program is a closed expression A value is either a abstraction x e or an integer constant c We use v to range over values We use dce to denote the integer represented by an integer constant c A small step call by value operational semantics for the language is given by the reflexive transitive closure of the relation V V Expression Expression x e v V e x v 6 e1 V e01 e1 e2 V e01 e2 7 e2 V e02 v e2 V v e02 8 succ c1 V c2 dc2 e dc1 e 1 e1 V e2 succ e1 V succ e2 9 10 The notation e x M denotes e with M substituted for every free occurrence of x x x M y x M x e1 x M y e1 x M e1 e2 x M c x M succ e1 x M M y x 6 y x e1 z e1 y z x M x 6 y and z fresh e1 x M e2 x M c succ e1 x M An expression e is stuck if it is not a value and there is no expression e0 such that e V e0 Intuitively a stuck expression is just about to produce a 0 0 run time error A program e goes wrong if e V e and e is stuck 6 Examples of stuck expressions include cv and succ x e Intuitively these expressions are stuck because c is not a function and succ cannot be applied to functions We will now prove that well typed programs cannot go wrong Corollary 3 7 The proof technique is standard For example several research groups have produced a similar theorem and proof for a considerable subset of Java for example Flatt Krishnamurthi and Felleisen A Programmer s Reduction Semantics for Classes and Mixins Rice University Department of Computer Science TR 97 293 revised June 1999 Many such big type soundness proofs have been checked by automatic proof checkers Lemma 3 1 Useless Assumption If A x s e t and x does not occur free in e then A e t Proof Left to the reader 2 Lemma 3 2 Substitution If A x s e t and A M s then A e x M t Proof We proceed by induction on the structure of the size of e There are now five subcases depending on which one of Rules 1 5 was the last one used in the derivation of A x s e t Rule 1 We have …