Type Checking in Compiler Design | Type Systems

A type system is a collection of rules that assign types to program constructs (more constraints added to checking the validity of the programs, violation of such constraints indicate errors).
A languages type system specifies which operations are valid for which types.
Type systems provide a concise formalization of the semantic checking rules.
Type rules are defined on the structure of expressions.
Type rules are language specific.

Type Expressions

A type expression is either a basic type or is formed by applying an operator called a type constructor to a type expression. The sets of basic types and constructors depend on the language to be checked.

The following are some of type expressions:

A basic type is a type expression. Typical basic types for a language include boolean, char, integer, float, and void(the absence of a value). type_error is a special basic type.
A type constructor applied to type expressions. Constructors include:

Arrays : If T is a type expression, then array(I, T) is a type expression denoting the type of an array with elements of type T and index set I. I is often a range of integers. Ex. int a[25] ;
Products : If T₁ and T₂ are type expressions, then their Cartesian product T₁ x T₂ is a type expression. x associates to the left and that it has higher precedence. Products are introduced for completeness; they can be used to represent a list or tuple of types (e.g., for function parameters).
Records : A record is a data structure with named fields. A type expression can be formed by applying the record type constructor to the field names and their types.
Pointers : If T is a type expression, then pointer (T) is a type expression denoting the type "pointer to an object of type T". For example: int a; int *p=&a;
Functions : Mathematically, a function maps depends on one set (domain) to another set(range). Function F : D -> R.A type expression can be formed by using the type constructor -> for function types. We write s -> t for "function from type s to type t".

Type expressions may contain variables whose values are themselves type expressions.

The array type int [2][3] can be written as a type expression array(2, array(3, integer)). This type is represented by the tree. The operator array takes two parameters, a number and a type.

Type Expression

Type checking is the process of verifying and applying the constraints of types, and it can occur either at compile time (i.e. statically) or at runtime (i.e. dynamically).
A language is statically-typed if the type of a variable is known at compile time instead of at runtime. Common examples of statically-typed languages such as Ada, C, C++, C#, JADE, Java, Fortran, Haskell, ML, Pascal, and Scala.
Dynamic type checking is the process of verifying the type safety of a program at runtime. Dynamically-typed languages include Groovy, JavaScript, Lisp, Lua, Objective-C, PHP, Prolog, Python, Ruby, Smalltalk and Tcl.
A language is strongly typed, if its compiler can guarantee that the programs it accepts will execute without type errors. Eg. For integers int array[255];.

Since type checking has the potential for catching errors in programs. It is important for a type checker to do something reasonable when an error is discovered.
At the very least, the compiler must report the nature and location of the error.
It is desirable for the type checker to recover from errors, so it can check the rest of the input.

PDF