The fundamental purpose of a type system is to prevent the occurrence of type errors during the execution of a program. This informal statement motivates the study of type systems, but requires clarification. Its accuracy depends, first of all, on the rather subtle issue of what constitutes a type error. Even when that is settled, the type soundness of a programming language (the absence of type errors in all program runs) is a non-trivial property. A fair amount of careful analysis is required to avoid false and embarrassing claims of type soundness; as a consequence, the classification, description, and study of type systems has emerged as a formal discipline.
The formal framework of type systems has practical applicability; it provides conceptual tools with which to judge the adequacy of important aspects of language definitions. Informal language descriptions often fail to specify a type system in sufficient detail to allow unambiguous implementation: different compilers for the same language may implement slightly different type systems. Moreover, many language definitions have been found to be type-unsound, allowing a program to crash even though it is judged acceptable by a typechecker. Formal techniques need not be applied in full to be useful; a knowledge of the main principles of type systems can help avoiding obvious and not-so-obvious pitfalls, and can inspire regularity and orthogonality in language design.
For the great majority of programming languages, type systems have not been formally specified and type soundness has not been formally established. Adequate technology, however, is now available. It involves defining the notion of type error for a given language, formalizing the type system by a set of type rules, and verifying that program execution of well-typed programs cannot produce type errors. This process, if successful, guarantees the type-soundness of a language as a whole. Type checking algorithms can then be developed as a separate concern, and their correctness can be verified with respect to a given type system; this process guarantees that typecheckers satisfy the language definition.
A type system describes the types that can be used to annotate programs, and the relationship between programs and types; common program types include Booleans, Integers, Reals, Records, Unions, Arrays, Objects, and Procedures. Annotations about the behavior of programs can, in general, range from informal comments to formal specifications subject to theorem proving. Type systems sit in the middle of this spectrum: they are more precise than comments, and more easily mechanizable than full specifications.
Type systems are designed to be decidably verifiable: there should be an algorithm (called a typechecking algorithm) that can tell whether or not a program is type-correct. (cf.: general specifications do not have correctness algorithms.) Type systems should be transparent: a programmer should be able to predict easily whether a program will typecheck. If it fails to typecheck, the reason for the failure should be self-evident. (cf.: automatic theorem proving may fail in mysterious ways.) Type systems should be enforceable: type declarations should be statically checked as much as possible, and otherwise dynamically checked. The consistency between type declarations and their associated programs should be routinely verified. (cf.: program comments and conventions are not checked.)
These considerations dictate the kind of constructions that are appropriate for typing programs. For example, they explain why many ordinary set-theoretical constructions are inappropriate, since they are not easily manipulated by a typechecker. Type systems for programming languages take inspiration, instead, from type theory, which is a branch of constructive logic separate from set theory.
Type systems are normally described via a particular formalism based on assertions called judgments. The most important judgment is the typing judgment, which asserts that a program fragment M has a type A with respect to a typing environment for the free variables of M. This judgment is written in the form:
E |- M : A (that is, program M has type A in environment E)
For example:
nil |- true : Bool (that is, true has type Bool in the empty environment)
nil, x:Int |- x+1 : Int (that is, x+1 has type Int, provided that x has type Int)
Any given judgment can be regarded as valid (e.g. E |- true : Bool) or invalid (e.g. E |- true : Int). The collection of valid judgments is described via type rules, which assert the validity of certain judgments on the basis of other valid judgments. In contrast to monolithic typechecking algorithms, type rules are highly modular: rules for different program constructs can be written separately. Therefore, type rules are comparatively easy to read, understand, analyze, and reuse.
A collection of type rules is called a (formal) type system. A program fragment M is well-typed if there is a type A such that E |- M : A is a valid judgment for some E; that is, if the program fragment M can be given some type. If there is no possible type for a given program, the program is not typeable (it has a type error). Thus, type errors are formalized independently of any particular typechecking algorithm.
Type systems are not explicitly algorithmic: the discovery of a type for a term in a given type system is called the type inference problem. Its solution requires the construction of appropriate typechecking algorithms, which is in itself an important and sometimes complex endeavor.
A large variety of formal type systems have been developed, with corresponding typechecking algorithms. They cover imperative, functional, and concurrent languages. They can handle simple and structured types, data abstraction, polymorphism, object-orientation, and modularization.
At the moment, some advanced constructions used in programming escape proper type-theoretical foundations. This could be either because the programming constructions are ill-conceived, or because our type theories are not yet sufficiently expressive: only the future will tell. Examples of active research areas are the typing of advanced object-orientation and modularization constructs, and the typing of concurrency and distribution.
Luca Cardelli. Type systems. The Handbook of Computer Science and Engineering, Chapter 103, 2208-2236, CRC Press, 1997.