Type checking

Posted on February 27, 2012 by Bilbo

Why type checker?
– determine the types of all expressions
– check that values and variables are used correctly
– resolve certain ambiguities by transforming the program

A type defines a set of possible values. Type annotation int x; specify an invariant on run-time behavior that x will always contain an integer value.

A program is type correct if the type annotations are valid invariants. TM(j) simulates the jth Turing machine on empty input. The program is type correct if and only if TM(j) doesn’t halt on empty input.

A program is statically type correct if it satisfies some type rules.

Type judgement for statements L,C,M,V\vdash S means that S is statically type correct with: class library L, current class C, current method M and variable V. For instance, L,C,M,V \vdash E:\tau means that E is statically type correct and has type \tau. Note that L,C,M,V is an abstraction of the symbol table.

Kinds of rules:
– Declarations: when a variable is introduced.
– Propagation: when an expression’s type is used to determine the type of an enclosing expression.
– Restrictions: when the type of an expression is constrained by its usage context.
– Axioms (given facts): L,C,M,V \vdash this:C
– Predicates (boolean tests on type vars): \tau := \tau^\prime
– Inferences (given x we can conclude y): \frac{L,C,M,V\vdash E_1:int\ \ L,C,M,V \vdash E_2:int}{L,C,M,V\vdash E_1-E_2:int}

Type proofs:
– A type checker constructs a proof of the type correctness of a given program.
– A type proofs is a tree in which 1) nodes are inferences; 2) leaves are axioms or true predicates.
– A program is statically type correct iff it is the root of a type proof tree. (A type proof is a trace of a successful run of the type checker)

A coercion is a conversion function that is inserted automatically by the compiler. For instance, "abc" + 17 + x is transformed into "abc" + (new Integer(17).toString()) + x.toString().

This entry was posted in Compiler. Bookmark the permalink.

Leave a comment