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.
- 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 ;
- Products : If T1 and T2 are type expressions, then their Cartesian product T1 x T2 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  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.
Static and Dynamic Type Checking
- 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.
- 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;.
- 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.