Type Checking in Compiler Design | Type Systems

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 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 [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 Expression

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.
  • 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];.

Error Recovery

  • 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.

Related Searches to Type Checking in Compiler Design | Type Systems