Catch errors that are not caught by parsing (because many constructs are not context-free).

Examples (C):

  1. All identifiers are declared
  2. Types
  3. ...
The set of legal programs is a subset of the parse-able programs.

Scope

Symbol Tables

Types

Type checking formalism

Some rules

i is an integer literal (constant)
----------------------------------  [Int]
     |- i:int
|-e1:int    |-e2:int
----------------------------------  [Add]
     |-e1+e2:int

Type Checking

Subtyping relation between types

Soundness of a static typesystem

Our programming language

Our programming language is a subset of C/C++ with the following exceptions/features:

Type rules for our programming language

------------------  [false]
  |- false : bool
------------------  [true]
  |- true : bool
 s is a character literal
------------------------- [char]
  |- s : char
 s is a string literal
----------------------- [string]
  |- s : char *
    |-b:bool
----------------------- [Not]
  |- !b : bool
  |-x:int  |-y:int
----------------------- [Relational]
  |- x<y : bool
Notice that !i where i:int is not well-typed in our language. Similarly, true<false is not well-typed in our language.

Two expressions (or statements) may be sequenced using the semi-colon operator, such that the type of the compound expression is the same as the type of the second expression. If a new scope is created with an expression in its body, then the type of that new scope is the same as the type of its body.

|- e1:T1    |- e2:T2
-------------------- [Sequence]
  |- e1;e2 : T2
 |- e:T
---------- [Scope]
 |- {e}:T
For, example, the expression { { 2 + 3; 4; }; 5 } evaluates to 5.

Assignment expression

Now let's consider an assignment expression (or statement). Recall that an assignment expression evaluates to the value that has been assigned, and its type is the type of the assigned variable.

 |-x:T0  |-y:T1 T1<:T0
-------------------------- [Assignment]
  |- x := y : T1
This rule seems to be giving a valid type to the following expression: 1 := 2, but this would be incorrect in our language. To support an assignment, we need to distinguish between a reference type and a value type.

For a primitive type T, its corresponding reference type is written T&. A reference type represents an object (region of memory) holding the corresponding value type. By definition, T& is a subtype of T, i.e., T& <: T.

Example: the following subtyping relations can be present in our language: U<:T, T&<:T, U&<:U, U&<:T& (to form a diamond structure).

Thus, the assignment rule now becomes:

 |-e0:T0&  |-e1:T1 T1<:T0
------------------------------- [Assignment]
  |- e0 := e1 : val(T1)
Here val(T1) returns the value type of T1 if T1 is a reference type; else it returns T1 itself. Notice that the conclusion assigns a value type to the assignment expression, which rejects (x := y) := z expressions, but accepts x := (y := z). If we want to admit (x := y) := z, we may want to change the inferred type in the conclusion to T1& (the type of x), but that would be quite non-intuitive, as that would likely mean that we are assigning z to y in the execution semantics.

The assignment rule admits the following code to be well-typed:

class A { ... };
class B : A { int y; ... };
A a = B();
If we replace this rule with a less general version like the following, then the code above does not remain well-typed.
 |-x:T&  |-y:T
------------------- [Assignment]
  |- x := y : T
This above rule is sound but not precise, in the sense it does not admit all the programs that we would like to admit. This is similar to how a previous imprecise rule did not admit (1+2)+3. Notice that the conclusion assigns the more specific type T1, which admits (A a = B()).y as type correct.

While loop

 |-e:TB  |-x:T  TB<:bool
---------------------------- [While]
  |- while (e) x : void
This is a design decision. One could have said that the type of a while loop is the type of the last statement that executes. But then what if the statement didn't execute even once? Hence a type 'void' means that the statement has a type which is not usable.

Address-of

   |-s:T&
----------------------- [address-of]
  |- &s : T *
Notice that the address-of operator is only well-typed when used on a reference type, e.g., it is illegal to say &1.

If-then-else

    |- e1 : bool
    |- e2 : T2
    |- e3 : T3
--------------------------------  [if-then-else]
|- if e1 then e2 else e3 : void
Notice that it is by design that if-then-else always returns type, even when T2=T3.

Ternary

    |- e1 : bool
    |- e2 : T2
    |- e3 : T3
--------------------------------  [if-then-else]
|- e1 ? e2 : e3 : val(lub(T2,T3))
An upper bound U(T2,T3) of types T2 and T3, is defined so that the following hold: T2<:U and T3<U. A least upper bound lub(T2,T3) is defined so that lub is an upper-bound of T2 and T3, and the further, for any other upper bound U(T2,T3), lub <: U holds.

The lub need not be unique for a partially ordered set (poset), even in the presence of a void type. However, for our language, it turns out that lub is unique. If lub is not unique, this rule should be modified appropriately, e.g., to resolve this ambiguity. One option is to have a hypothesis that requires that there must exist a unique lub of T2 and T3 for this expression to be well-typed.

The val operator ensures that this cannot be now used in the LHS of an assignment.

Variable

But what is the type of a variable reference?

   x is a variable
  ----------------  [Var]
      |- x:?
The local, structural rule does not carry enough information to give x a type. We need more information in the rules.

A type environment gives types for free variables

The sentence O |- e:T is read

i is an integer literal (constant)
----------------------------------  [Int]
    O |- i:int
 O |- e1:int    O |- e2:int
----------------------------------  [Add]
    O |- e1+e2:int
Notice that the same assumptions are required in both the hypotheses and the conclusion.

And we can write our first rule that uses type environment O

O(x) = T
-------------  [Var]
O |- x:T&
Notice that we choose to keep the value type in O, and use it to assign the reference type to x --- this is a succinct way of saying that all variables must be of a reference type.

We allow a declaration only at the beginning of a scope; moreover, there can be at most one declaration at the beginning of a scope, and multiple declarations require multiple nested scopes.

  O[T0/x] |- e1:T1
   T0 != void
----------------------------    [Let-No-Init]
 O |- { T0 x; e1 } : T1
O[T/x] represents one function, where
O[T/x](x) = T
O[T/x](y) = O(y)
Notice that we use T0/X instead of T0&/X --- that's because the Var rule only expects the value type of the variable in the type environment, and uses it to assign a reference type to the variable.

When we enter the scope, we add a new assumption in our type environment. When we leave the scope, we remove the assumption.

This terminology reminds us of the symbol table. So the type-environment is stored in the symbol table.

Our language also allows the initialization of a newly-declared variable.
      O[T0/x] |- e1:T1
         O |- e2:T0
         T0 != void
----------------------------    [Let-Init]
 O |- { T0 x = e2; e1 } : T1
Notice that this rule says that the initializer e2 should have the same type T0 as x. This is imprecise, we should ideally allow such assignment as long as e2 is of a subtype of T0.

A better version of [Let-Init] using subtyping:

      O[T/x] |- e1:T1
         O |- e2:T0
       T0 <: T
        T != void
----------------------------    [Let-Init]
 O |- { T x = e2; e1 } : T1
Notice that T0 only needs to be a subtype of T and not a subtype of T&. This allows int x = 3. Notice that we disallow the construction of a term of type void&. Consequently, we also disallow the construction of a term of type void*.

Typing Methods

C++ example
        O |- e1:T1
        ...
        O |- en:Tn
------------------------------ [Dispatch]
   O |- f(e1,e2,...,en):?
Also maintain a mapping for method signatures in O
O(f) = (T1,...,Tn,T(n+1))
means that there is a method f such that
f(x1:T1,x2:T2,x3:T3,...,xn:Tn):T(n+1)
Hence, our dispatch rule becomes:
        O |- e1:T1
        ...
        O |- en:Tn
        O |- f:(T1',..,Tn',T(n+1)')
        T1<=T1',...Tn<=Tn'
---------------------------------------- [Dispatch]
   O |- f(e1,e2,...,en):T(n+1)
Notice that this tackles both call-by-value and call-by reference. For example, T1' could be a reference type. Further, a reference-type can be used as an argument where a value-type was expected; but not vice-versa.

Object-oriented languages also implement encapsulation (e.g., some functions are only visible in certain classes, etc.). To handle them, one can extend O to be a function from a tuple of class-name and the identifier-name, e.g., C.f instead of f.

Example: The following shows an example syntax of a method declaration and dispatch.

class C {
   ....
   ...foo(T1 a1, ..., Tn an) .... //method declaration.
};

C c;
c.foo(....);

The following shows an example syntax of a method declaration and dispatch with inheritance (subtyping) where D<:C.

class C {
   ....
   ...foo(T1 a1, ..., Tn an) .... //method declaration.
};

D c;
c.foo(x1,...,xn);
In this case, we will use scoping rules to resolve "which foo?". For example, in this case, the foo is C's foo. Notice that the scoping rule will need to know the type of c and potentially the types of x1..xn to be able to identify "which foo?", and so scoping and typing work hand-in-hand. Irrespective, once the question has been answered, we annotate each such dispatch with the class name corresponding to the method being dispatched, e.g., the dispatch in the example above becomes:
D c;
c@C.foo(....);
This disambiguation is required to determine the type of the return value, e.g., C.foo may have a different return type than B.foo.

To express inheritance, we will use the subtype-relation for the this object in the method dispatch.

     O |- e0:T0&
     O |- e1:T1
     ...
     O |- en:Tn
     O |- T.f : (T1',..,Tn',T(n+1))
     T0 <: T
     T1<:T1', ...,  Tn<:Tn'
---------------------------------------- [Static-Dispatch]
   O |- e0@T.f(e1,e2,...,en):T(n+1)
Notice that we require e0 to be a reference type. In other words, e0 should represent of a region of memory, also called an object.

Type polymorphism examples

The following definitions can co-exist.
  1. int foo(int)
  2. long foo(long)
  3. string foo(string)
Notice that string foo(int) cannot co-exist with the first foo.

Type resolution in this case is performed by looking at the types of the arguments, and those definitions are enabled where the types of actual arguments are respective subtypes of the formal arguments. If no definitions are enabled, this is a type error. If more than one definitions are enabled, that is usually a type-ambiguity error. (Notice that using resolution rules here like, most closely matching type, etc., are unlikely to be intuitive for the programmer when there are multiple arguments and one argument matches more closely for one candidate while another argument matches more closely for another candidate).

this keyword

For object-oriented languages, to resolve the this keyword, we also need to know the "current class" C in which the expression is sitting. To support this, we change the form of a typing rule (also called a sentence in logic) to:

O,C |- e:T
We use C=null for a context which is free of any "current class".

For example,

 O,C |- e1:int    O,C |- e2:int
----------------------------------  [Add]
    O,C |- e1+e2:int
The rule for the this keyword would be the following:
  C != null
---------------  [This]
O,C : this: C*

Summary

Warning: Type rules are very compact! A lot of information in compact rules and it takes time to interpret them.

Implementing Type Checking

Let's consider the following rule:
 O,C |- e1:int    O,C |- e2:int
----------------------------------  [Add]
    O,C |- e1+e2:int
This says that to type-check e1+e2, then we have to type-check e1 and e2 separately in the same O,C environment.
TypeCheck(Environment, e1+e2) = {
  T1 = TypeCheck(Environment, e1);
  Check T1 == int;
  T2 = TypeCheck(Environment, e2);
  Check T2 == int;
  return int;
}
Let's consider a more complex example:
         O |- e2:T0
      O[T&/x] |- e1:T1
       T0 <: T
        T != void
----------------------------    [Let-Init]
 O |- { T x = e2; e1 } : T1
Let's look at the corresponding type-checking implementation:
TypeCheck(Environment, { T x = e0; e1 }) = {
  T0 = TypeCheck(Environment, e0);
  T1 = TypeCheck(Environment.add(x:T&), e1);
  Check subtype(T0,T1);
  Check T != void;
  return T1;
}

Recall that we claimed that type inference and type checking are similar, in that they use the same typing rules. The typing rules can also be used to implement type inference. We can modify the TypeCheck function, so that along with the Environment, it also passes down the acceptable types for a sub-expression, or more generally type constraints. At the end, these constraints can be solved to identify the types of the leaf nodes of the AST to implement type inference. If the constraints have no solution, it is a type error. If the constraints have more than one solution, either there is a type ambiguity error, or there is a rule to resolve the ambiguity. For example, the most general type may be used when all the candidate types are ordered by the subtyping relation, i.e., the type that is the supertype of all other candidates, e.g., \alpha-list is more general than int-list.

Static vs. Dynamic Typing

Languages with static type checking also have a notion of dynamic types, just that they may or may not implement the dynamic checks. The dynamic type of a term is determined through the execution semantics.

If a typesystem is sound, we do not need to implement dynamic checks for the properties that have been checked statically. For example, we do not need to dynamically check during execution of 1+2 that 1 and 2 are both of type int.

Consider C++ program:

class A { ... }
class B : public A { ... }
void foo() {
  A* foo = new A;
  B* bar = new B;
  ....
  foo =  bar;
}
Static type of foo is "A*", but the dynamic type of foo is "A*" and "B*" at different program points.

Formalizing the relationship, for a sound typesystem: for all expressions E, dynamic_type(E) <: static_type(E)

In all executions, E evaluates to values of the type inferred by the compiler. You have to actually run the program to get the dynamic_type. In the early days of programming languages, equality (instead of subtype relation) was proved for their type systems.

Notice that rejecting all programs is sound. That's why we also care about precision, i.e., how many programs we can willingly accept.

Completeness

All dynamically type-correct programs are accepted by the static typechecker. Consider the following program:
C c;
D d; //where D is a subtype of C
....
D d2 = cond ? c : d;
Let's say that at runtime cond can never be false, and so this program is dynamically type-correct. However, statically figuring out that cond is never false is undecidable.

Show a Venn diagram: statically-type-correct < dynamically-type-correct < parseable. For soundness, statically-type-correct < dynamically-type-correct should hold. For completeness, dynamically-type-correct < statically-type-correct should hold.

All operations that can be used on an object of type C can also be used on an object of type C' <= C.

Subclasses only add attributes or methods (they never remove attributes/methods).

The dynamic type is obtained through the execution semantics of the program, e.g., if we have an expression x++, and the current state of the program determines x to be of type int&, there is a dynamic typing rule that says that the type of the new expression is also int&. Consider the example { T x = e0; x; } where e0:T0 <: T; here the dynamic type of the expression is T0 (not T!). Similarly, the dynamic type of if x then y:T1 else Y:T2 will be either T1 or T2 (not lub(T1,T2) or void).

In other words, soundness states that the static type system will not accept any incorrect program (that will not pass the dynamic type check of equal power). A dynamic type check for array-bounds is not of equal power (it has more checks enabled); a sound static type check for array-bounds would reject all incorrect programs (but it will also reject a few more that will actually pass the dynamic type check).

Soundness of static type system: all dynamically-type-incorrect programs will be rejected. Ensured by ensuring that static_type is a supertype of dynamic_type. A trivial static-type system that rejects all programs is sound (but not useful).

Completeness: all dynamically-type-correct programs will be accepted. Not possible to ensure both soundness and completeness in general.

Example where static type system can be too restrictive

While a static type system may be sound, it may be too restrictive and may disallow certain programs that may be dynamically well-typed.
class Count {
  int i = 0; //default value = 0
  Count inc() { i := i + 1; return *this; }
};
Now consider a subclass Stock of Count:
class Stock : public Count {
  string name; //name of the item
};
And the following use of Stock:
Stock a;
Stock b = a.inc();
... b.name ...
This code does not type-check because the return value of inc is Count which is not a subtype of Stock.

This seems like a major limitation as now the derived classes (subtypes) will be unable to use the inc method.

a.inc() has dynamic type Stock.

So dynamically speaking, it is legitimate to write the following: Stock b := a.inc(); But this is not well-typed as

  • a.inc() has static type Count.

    Common workarounds to the incompleteness of a static type system:

    Error Recovery