The component of a programming language that associates each expression of the language (variables, functions, operators, etc.) with a data type. A type system consists of a collection of types and type constructors, together with rules (called type rules) that determine the consistency of an expression with a given type. The violation of a type rule constitutes a type error, and the testing for type errors in a given program is called type checking. Type checking is very important for determining the semantics of a program with regard to a type system; it can be performed either at compilation time (i.e. by the compiler) or at run time (i.e. during program execution). Compilation-time type checking is in general more desirable because run-time type checking is expensive, but a mixture of both is possible.

A language is a typed language if there exists a type system for it: otherwise, it is an untyped language (i.e. it has no type or, equivalently, has a single universal type for all expressions). Whether it is expedient to provide a type system for a particular programming language will depend on importance of types in the description of the behaviour of the programs that can be written in that language.