Type system

In programming languages, a type system is a logical system comprising a set of rules that assigns a property called a type to the various constructs of a computer program, such as variables, expressions, functions or modules. These types formalize and enforce the otherwise implicit categories the programmer uses for algebraic data types, data structures, or other components. The main purpose of a type system is to reduce possibilities for bugs in computer programs by defining interfaces between different parts of a computer program, and then checking that the parts have been connected in a consistent way. This checking can happen statically, dynamically, or as a combination of both. Type systems have other purposes as well, such as expressing business rules, enabling certain compiler optimizations, allowing for multiple dispatch, providing a form of documentation, etc.
A type system associates a type with each computed value and, by examining the flow of these values, attempts to ensure or prove that no type errors can occur. The given type system in question determines what constitutes a type error, but in general the aim is to prevent operations expecting a certain kind of value from being used with values for which that operation does not make sense. Type systems are often specified as part of programming languages and built into interpreters and compilers, although the type system of a language can be extended by optional tools that perform added checks using the language's original type syntax and grammar.

Usage overview

An example of a simple type system is that of the C language. The portions of a C program are the function definitions. One function is invoked by another function. The interface of a function states the name of the function and a list of values that are passed to the function's code. The code of an invoking function states the name of the invoked, along with the names of variables that hold values to pass to it. During execution, the values are placed into temporary storage, then execution jumps to the code of the invoked function. The invoked function's code accesses the values and makes use of them. If the instructions inside the function are written with the assumption of receiving an integer value, but the calling code passed a floating-point value, then the wrong result will be computed by the invoked function. The C compiler checks the type declared for each variable sent, against the type declared for each variable in the interface of the invoked function. If the types do not match, the compiler throws a compile-time error.
A compiler may also use the static type of a value to optimize the storage it needs and the choice of algorithms for operations on the value. In many C compilers the float data type, for example, is represented in 32 bits, in accord with the IEEE specification for single-precision floating point numbers. They will thus use floating-point-specific microprocessor operations on those values.
The depth of type constraints and the manner of their evaluation affect the typing of the language. A programming language may further associate an operation with various resolutions for each type, in the case of type polymorphism. Type theory is the study of type systems. The concrete types of some programming languages, such as integers and strings, depend on practical issues of computer architecture, compiler implementation, and language design.


Formally, type theory studies type systems. A programming language must have occurrence to type check using the type system whether at compile time or runtime, manually annotated or automatically inferred. As Mark Manasse concisely put it:
Assigning a data type, termed typing, gives meaning to a sequence of bits such as a value in memory or some object such as a variable. The hardware of a general purpose computer is unable to discriminate between for example a memory address and an instruction code, or between a character, an integer, or a floating-point number, because it makes no intrinsic distinction between any of the possible values that a sequence of bits might mean. Associating a sequence of bits with a type conveys that to the programmable hardware to form a symbolic system composed of that hardware and some program.
A program associates each value with at least one specific type, but it also can occur that one value is associated with many subtypes. Other entities, such as objects, modules, communication channels, and dependencies can become associated with a type. Even a type can become associated with a type. An implementation of a type system could in theory associate identifications called data type, class, and kind. These are the abstractions that typing can go through, on a hierarchy of levels contained in a system.
When a programming language evolves a more elaborate type system, it gains a more finely grained rule set than basic type checking, but this comes at a price when the type inferences become undecidable, and when more attention must be paid by the programmer to annotate code or to consider computer-related operations and functioning. It is challenging to find a sufficiently expressive type system that satisfies all programming practices in a type safe manner.
The more type restrictions that are imposed by the compiler, the more strongly typed a programming language is. Strongly typed languages often require the programmer to make explicit conversions in contexts where an implicit conversion would cause no harm. Pascal's type system has been described as "too strong" because, for example, the size of an array or string is part of its type, making some programming tasks difficult. Haskell is also strongly typed but its types are automatically inferred so that explicit conversions are often unnecessary.
A programming language compiler can also implement a dependent type or an effect system, which enables even more program specifications to be verified by a type checker. Beyond simple value-type pairs, a virtual "region" of code is associated with an "effect" component describing what is being done with what, and enabling for example to "throw" an error report. Thus the symbolic system may be a type and effect system, which endows it with more safety checking than type checking alone.
Whether automated by the compiler or specified by a programmer, a type system makes program behavior illegal if outside the type-system rules. Advantages provided by programmer-specified type systems include:
Advantages provided by compiler-specified type systems include:
A type error is an unintended condition which might manifest in multiple stages of a program's development. Thus a facility for detection of the error is needed in the type system. In some languages, such as Haskell, for which type inference is automated, lint might be available to its compiler to aid in the detection of error.
Type safety contributes to program correctness, but might only guarantee correctness at the cost of making the type checking itself an undecidable problem. In a type system with automated type checking a program may prove to run incorrectly yet be safely typed, and produce no compiler errors. Division by zero is an unsafe and incorrect operation, but a type checker running at compile time only does not scan for division by zero in most languages, and then it is left as a runtime error. To prove the absence of these more-general-than-types defects, other kinds of formal methods, collectively known as program analyses, are in common use. Alternatively, a sufficiently expressive type system, such as in dependently typed languages, can prevent these kinds of errors. In addition software testing is an empirical method for finding errors that the type checker cannot detect.

Type checking

The process of verifying and enforcing the constraints of types—type checking—may occur either at compile time or at run-time. If a language specification requires its typing rules strongly, one can refer to the process as strongly typed, if not, as weakly typed. The terms are not usually used in a strict sense.

Static type checking

Static type checking is the process of verifying the type safety of a program based on analysis of a program's text. If a program passes a static type checker, then the program is guaranteed to satisfy some set of type safety properties for all possible inputs.
Static type checking can be considered a limited form of program verification, and in a type-safe language, can be considered also an optimization. If a compiler can prove that a program is well-typed, then it does not need to emit dynamic safety checks, allowing the resulting compiled binary to run faster and to be smaller.
Static type checking for Turing-complete languages is inherently conservative. That is, if a type system is both sound and decidable, then it must be incomplete. For example, consider a program containing the code:
Even if the expression always evaluates to true at run-time, most type checkers will reject the program as ill-typed, because it is difficult for a static analyzer to determine that the else branch will not be taken. Conversely, a static type checker will quickly detect type errors in rarely used code paths. Without static type checking, even code coverage tests with 100% coverage may be unable to find such type errors. The tests may fail to detect such type errors, because the combination of all places where values are created and all places where a certain value is used must be taken into account.
A number of useful and common programming language features cannot be checked statically, such as downcasting. Thus, many languages will have both static and dynamic type checking; the static type checker verifies what it can, and dynamic checks verify the rest.
Many languages with static type checking provide a way to bypass the type checker. Some languages allow programmers to choose between static and dynamic type safety. For example, C# distinguishes between statically-typed and dynamically-typed variables. Uses of the former are checked statically, whereas uses of the latter are checked dynamically. Other languages allow writing code that is not type-safe; for example, in C, programmers can freely cast a value between any two types that have the same size, effectively subverting the type concept.
For a list of languages with static type checking, see :Category:Statically typed programming languages|the category for statically typed languages.

Dynamic type checking and runtime type information

Dynamic type checking is the process of verifying the type safety of a program at runtime. Implementations of dynamically type-checked languages generally associate each runtime object with a type tag containing its type information. This runtime type information can also be used to implement dynamic dispatch, late binding, downcasting, reflection, and similar features.
Most type-safe languages include some form of dynamic type checking, even if they also have a static type checker. The reason for this is that many useful features or properties are difficult or impossible to verify statically. For example, suppose that a program defines two types, A and B, where B is a subtype of A. If the program tries to convert a value of type A to type B, which is known as downcasting, then the operation is legal only if the value being converted is actually a value of type B. Thus, a dynamic check is needed to verify that the operation is safe. This requirement is one of the criticisms of downcasting.
By definition, dynamic type checking may cause a program to fail at runtime. In some programming languages, it is possible to anticipate and recover from these failures. In others, type-checking errors are considered fatal.
Programming languages that include dynamic type checking but not static type checking are often called "dynamically typed programming languages". For a list of such languages, see :Category:Dynamically typed programming languages|the category for dynamically typed programming languages.

Combining static and dynamic type checking

Some languages allow both static and dynamic typing. For example, Java and some other ostensibly statically typed languages support downcasting types to their subtypes, querying an object to discover its dynamic type, and other type operations that depend on runtime type information. Another example is C++ RTTI. More generally, most programming languages include mechanisms for dispatching over different 'kinds' of data, such as disjoint unions, runtime polymorphism, and variant types. Even when not interacting with type annotations or type checking, such mechanisms are materially similar to dynamic typing implementations. See programming language for more discussion of the interactions between static and dynamic typing.
Objects in object-oriented languages are usually accessed by a reference whose static target type is equal to either the object's run-time type or a supertype thereof. This is conformant with the Liskov substitution principle, which states that all operations performed on an instance of a given type can also be performed on an instance of a subtype. This concept is also known as subsumption or subtype polymorphism. In some languages subtypes may also possess covariant or contravariant return types and argument types respectively.
Certain languages, for example Clojure, Common Lisp, or Cython are dynamically type-checked by default, but allow programs to opt into static type checking by providing optional annotations. One reason to use such hints would be to optimize the performance of critical sections of a program. This is formalized by gradual typing. The programming environment DrRacket, a pedagogic environment based on Lisp, and a precursor of the language Racket is also soft-typed.
Conversely, as of version 4.0, the C# language provides a way to indicate that a variable should not be statically type-checked. A variable whose type is dynamic will not be subject to static type checking. Instead, the program relies on runtime type information to determine how the variable may be used.

Static and dynamic type checking in practice

The choice between static and dynamic typing requires certain trade-offs.
Static typing can find type errors reliably at compile time, which should increase the reliability of the delivered program. However, programmers disagree over how commonly type errors occur, resulting in further disagreements over the proportion of those bugs that are coded that would be caught by appropriately representing the designed types in code. Static typing advocates believe programs are more reliable when they have been well type-checked, whereas dynamic-typing advocates point to distributed code that has proven reliable and to small bug databases. The value of static typing, then, presumably increases as the strength of the type system is increased. Advocates of dependent typing, implemented in languages such as Dependent ML and Epigram, have suggested that almost all bugs can be considered type errors, if the types used in a program are properly declared by the programmer or correctly inferred by the compiler.
Static typing usually results in compiled code that executes faster. When the compiler knows the exact data types that are in use it can produce optimized machine code. Some dynamically typed languages such as Common Lisp allow optional type declarations for optimization for this reason.
By contrast, dynamic typing may allow compilers to run faster and interpreters to dynamically load new code, because changes to source code in dynamically typed languages may result in less checking to perform and less code to revisit. This too may reduce the edit-compile-test-debug cycle.
Statically typed languages that lack type inference require that programmers declare the types that a method or function must use. This can serve as added program documentation, that is active and dynamic, instead of static. This allows a compiler to prevent it from drifting out of synchrony, and from being ignored by programmers. However, a language can be statically typed without requiring type declarations, so explicit type declaration is not a necessary requirement for static typing in all languages.
Dynamic typing allows constructs that some static type checking would reject as illegal. For example, eval functions, which execute arbitrary data as code, become possible. An eval function is possible with static typing, but requires advanced uses of algebraic data types. Further, dynamic typing better accommodates transitional code and prototyping, such as allowing a placeholder data structure to be transparently used in place of a full data structure.
Dynamic typing typically allows duck typing. Many languages with static typing also feature duck typing or other mechanisms like generic programming that also enable easier code reuse.
Dynamic typing typically makes metaprogramming easier to use. For example, C++ templates are typically more cumbersome to write than the equivalent Ruby or Python code since C++ has stronger rules regarding type definitions. This forces a developer to write more boilerplate code for a template than a Python developer would need to. More advanced run-time constructs such as metaclasses and introspection are often harder to use in statically typed languages. In some languages, such features may also be used e.g. to generate new types and behaviors on the fly, based on run-time data. Such advanced constructs are often provided by dynamic programming languages; many of these are dynamically typed, although dynamic typing need not be related to dynamic programming languages.

Strong and weak type systems

Languages are often colloquially referred to as strongly typed or weakly typed. In fact, there is no universally accepted definition of what these terms mean. In general, there are more precise terms to represent the differences between type systems that lead people to call them "strong" or "weak".

Type safety and memory safety

A third way of categorizing the type system of a programming language is by the safety of typed operations and conversions. Computer scientists use the term type-safe language to describe languages that do not allow operations or conversions that violate the rules of the type system.
Computer scientists use the term memory-safe language to describe languages that do not allow programs to access memory that has not been assigned for their use. For example, a memory-safe language will check array bounds, or else statically guarantee that array accesses out of the array boundaries will cause compile-time and perhaps runtime errors.
Consider the following program of a language that is both type-safe and memory-safe:

var x := 5;
var y := "37";
var z := x + y;

In this example, the variable will have the value 42. Although this may not be what the programmer anticipated, it is a well-defined result. If were a different string, one that could not be converted to a number, the result would be well-defined as well. Note that a program can be type-safe or memory-safe and still crash on an invalid operation; in fact, if a program encounters an operation that is not type-safe, terminating the program is often the only option.
Now consider a similar example in C:

int x = 5;
char y = "37";
char* z = x + y;

In this example will point to a memory address five characters beyond, equivalent to three characters after the terminating zero character of the string pointed to by. This is memory that the program is not expected to access. It may contain garbage data, and it certainly doesn't contain anything useful. As this example shows, C is neither a memory-safe nor a type-safe language.
In general, type-safety and memory-safety go hand in hand. For example, a language that supports pointer arithmetic and number-to-pointer conversions is neither memory-safe nor type-safe, because it allows arbitrary memory to be accessed as if it were valid memory of any type.
For more information, see memory safety.

Variable levels of type checking

Some languages allow different levels of checking to apply to different regions of code. Examples include:
Additional tools such as lint and IBM Rational Purify can also be used to achieve a higher level of strictness.

Optional type systems

It has been proposed, chiefly by Gilad Bracha, that the choice of type system be made independent of choice of language; that a type system should be a module that can be plugged into a language as needed. He believes this is advantageous, because what he calls mandatory type systems make languages less expressive and code more fragile. The requirement that types do not affect the semantics of the language is difficult to fulfill.
Optional typing is related to, but distinct from, gradual typing. While both typing disciplines can be used to perform static analysis of code, optional type systems do not enforce type safety at runtime.

Polymorphism and types

The term polymorphism refers to the ability of code to act on values of multiple types, or to the ability of different instances of the same data structure to contain elements of different types. Type systems that allow polymorphism generally do so in order to improve the potential for code re-use: in a language with polymorphism, programmers need only implement a data structure such as a list or an associative array once, rather than once for each type of element with which they plan to use it. For this reason computer scientists sometimes call the use of certain forms of polymorphism generic programming. The type-theoretic foundations of polymorphism are closely related to those of abstraction, modularity and subtyping.

Duck typing

In duck typing, a statement calling a method m on an object does not rely on the declared type of the object; only that the object, of whatever type, must supply an implementation of the method called, when called, at run-time.
Duck typing differs from structural typing in that, if the part needed for a given local computation is present at runtime, the duck type system is satisfied in its type identity analysis. On the other hand, a structural type system would require the analysis of the whole module structure at compile time to determine type identity or type dependence.
Duck typing differs from a nominative type system in a number of aspects. The most prominent ones are that for duck typing, type information is determined at runtime, and the name of the type is irrelevant to determine type identity or type dependence; only partial structure information is required for that for a given point in the program execution.
Duck typing uses the premise that "if it walks like a duck, and quacks like a duck, then it is a duck". The term may have been coined by Alex Martelli in a 2000 message to the comp.lang.python newsgroup.
While one controlled experiment showed an increase in developer productivity for duck typing in single developer projects, other controlled experiments on API usability show the opposite.

Specialized type systems

Many type systems have been created that are specialized for use in certain environments with certain types of data, or for out-of-band static program analysis. Frequently, these are based on ideas from formal type theory and are only available as part of prototype research systems.
The following table gives an overview over type theoretic concepts that are used in specialized type systems.
The names range over terms and the names range over types.
The notation describes the type which results from replacing all occurrences of the type variable in by the type .
Type notionNotationMeaning
FunctionIf has type and has type, then the application has type.
ProductIf has type, then is a pair such that has type and has type.
SumIf has type, then either is the first injection such that has type, or
is the second injection such that has type.
IntersectionIf has type, then has type and has type.
UnionIf has type, then has type or has type.
RecordIf has type, then has a member that has type.
PolymorphicIf has type, then has type for any type.
ExistentialIf has type, then has type for some type.
RecursiveIf has type, then has type.
Dependent functionIf has type and has type, then the application has type.
Dependent productIf has type, then is a pair such that has type and has type.
Dependent intersectionIf has type, then has type and has type.
Familial intersectionIf has type, then has type for any term of type.
Familial unionIf has type, then has type for some term of type.

Dependent types

s are based on the idea of using scalars or values to more precisely describe the type of some other value. For example, might be the type of a matrix. We can then define typing rules such as the following rule for matrix multiplication:
where,, are arbitrary positive integer values. A variant of ML called Dependent ML has been created based on this type system, but because type checking for conventional dependent types is undecidable, not all programs using them can be type-checked without some kind of limits. Dependent ML limits the sort of equality it can decide to Presburger arithmetic.
Other languages such as Epigram make the value of all expressions in the language decidable so that type checking can be decidable. However, in general proof of decidability is undecidable, so many programs require hand-written annotations that may be very non-trivial. As this impedes the development process, many language implementations provide an easy way out in the form of an option to disable this condition. This, however, comes at the cost of making the type-checker run in an infinite loop when fed programs that do not type-check, causing the compilation to fail.

Linear types

s, based on the theory of linear logic, and closely related to uniqueness types, are types assigned to values having the property that they have one and only one reference to them at all times. These are valuable for describing large immutable values such as files, strings, and so on, because any operation that simultaneously destroys a linear object and creates a similar object can be optimized "under the hood" into an in-place mutation. Normally this is not possible, as such mutations could cause side effects on parts of the program holding other references to the object, violating referential transparency. They are also used in the prototype operating system Singularity for interprocess communication, statically ensuring that processes cannot share objects in shared memory in order to prevent race conditions. The Clean language uses this type system in order to gain a lot of speed while remaining safe.

Intersection types

s are types describing values that belong to both of two other given types with overlapping value sets. For example, in most implementations of C the signed char has range -128 to 127 and the unsigned char has range 0 to 255, so the intersection type of these two types would have range 0 to 127. Such an intersection type could be safely passed into functions expecting either signed or unsigned chars, because it is compatible with both types.
Intersection types are useful for describing overloaded function types: for example, if " → " is the type of functions taking an integer argument and returning an integer, and " → " is the type of functions taking a float argument and returning a float, then the intersection of these two types can be used to describe functions that do one or the other, based on what type of input they are given. Such a function could be passed into another function expecting an " → " function safely; it simply would not use the " → " functionality.
In a subclassing hierarchy, the intersection of a type and an ancestor type is the most derived type. The intersection of sibling types is empty.
The Forsythe language includes a general implementation of intersection types. A restricted form is refinement types.

Union types

s are types describing values that belong to either of two types. For example, in C, the signed char has a -128 to 127 range, and the unsigned char has a 0 to 255 range, so the union of these two types would have an overall "virtual" range of -128 to 255 that may be used partially depending on which union member is accessed. Any function handling this union type would have to deal with integers in this complete range. More generally, the only valid operations on a union type are operations that are valid on both types being unioned. C's "union" concept is similar to union types, but is not typesafe, as it permits operations that are valid on either type, rather than both. Union types are important in program analysis, where they are used to represent symbolic values whose exact nature is not known.
In a subclassing hierarchy, the union of a type and an ancestor type is the ancestor type. The union of sibling types is a subtype of their common ancestor.

Existential types

types are frequently used in connection with record types to represent modules and abstract data types, due to their ability to separate implementation from interface. For example, the type "T = ∃X " describes a module interface that has a data member named a of type X and a function named f that takes a parameter of the same type X and returns an integer. This could be implemented in different ways; for example:
These types are both subtypes of the more general existential type T and correspond to concrete implementation types, so any value of one of these types is a value of type T. Given a value "t" of type "T", we know that "t.f" is well-typed, regardless of what the abstract type X is. This gives flexibility for choosing types suited to a particular implementation while clients that use only values of the interface type—the existential type—are isolated from these choices.
In general it's impossible for the typechecker to infer which existential type a given module belongs to. In the above example intT could also have the type ∃X. The simplest solution is to annotate every module with its intended type, e.g.:
Although abstract data types and modules had been implemented in programming languages for quite some time, it wasn't until 1988 that John C. Mitchell and Gordon Plotkin established the formal theory under the slogan: "Abstract types have existential type". The theory is a second-order typed lambda calculus similar to System F, but with existential instead of universal quantification.

Gradual typing

is a type system in which variables may be assigned a type either at compile-time or at run-time, allowing software developers to choose either type paradigm as appropriate, from within a single language. In particular, gradual typing uses a special type named dynamic to represent statically-unknown types, and gradual typing replaces the notion of type equality with a new relation called consistency that relates the dynamic type to every other type. The consistency relation is symmetric but not transitive.

Explicit or implicit declaration and inference

Many static type systems, such as those of C and Java, require type declarations: the programmer must explicitly associate each variable with a specific type. Others, such as Haskell's, perform type inference: the compiler draws conclusions about the types of variables based on how programmers use those variables. For example, given a function that adds and together, the compiler can infer that and must be numbers—since addition is only defined for numbers. Thus, any call to elsewhere in the program that specifies a non-numeric type as an argument would signal an error.
Numerical and string constants and expressions in code can and often do imply type in a particular context. For example, an expression might imply a type of floating-point, while might imply a list of integers—typically an array.
Type inference is in general possible, if it is computable in the type system in question. Moreover, even if inference is not computable in general for a given type system, inference is often possible for a large subset of real-world programs. Haskell's type system, a version of Hindley–Milner, is a restriction of System Fω to so-called rank-1 polymorphic types, in which type inference is computable. Most Haskell compilers allow arbitrary-rank polymorphism as an extension, but this makes type inference not computable.

Decision problems

A type system that assigns types to terms in type environments using type rules is naturally associated with the decision problems of type checking, typability, and type inhabitation.

Type checking

The decision problem of type checking is:
Decidability of type checking means that type safety of any given program text can be verified.


The decision problem of typability is:
A variant of typability is typability wrt. a type environment, for which a type environment is part of the input.
If the given term does not contain external references, then typability coincides with typability wrt. the empty type environment.
Typability is closely related to type inference. Whereas typability addresses the existence of a type for a given term, type inference requires an actual type to be computed.

Type inhabitation

The decision problem of type inhabitation is:
Type inhabitation often plays an auxiliary role in program development.
For example, intelligent program text completion may rely on existing type information to suggest type-safe code fragments to add to the current program text.
In programming languages, such as Scala, implicit conversions synthesize program text converting objects of one type into objects of a different type based on type information.
More generally, in program synthesis type inhabitation can be used to construct programs from specification given in form of type information.

Unified type system

Some languages like C# or Scala have a unified type system. This means that all C# types including primitive types inherit from a single root object. Every type in C# inherits from the Object class. Some languages, like Java and Raku, have a root type but also have primitive types that are not objects. Java provides wrapper object types that exist together with the primitive types so developers can use either the wrapper object types or the simpler non-object primitive types. Raku automatically converts primitive types to objects when their methods are accessed.

Compatibility: equivalence and subtyping

A type checker for a statically typed language must verify that the type of any expression is consistent with the type expected by the context in which that expression appears. For example, in an assignment statement of the form x := e,
the inferred type of the expression e must be consistent with the declared or inferred type of the variable x. This notion of consistency, called compatibility, is specific to each programming language.
If the type of e and the type of x are the same, and assignment is allowed for that type, then this is a valid expression. Thus, in the simplest type systems, the question of whether two types are compatible reduces to that of whether they are equal. Different languages, however, have different criteria for when two type expressions are understood to denote the same type. These different equational theories of types vary widely, two extreme cases being structural type systems, in which any two types that describe values with the same structure are equivalent, and nominative type systems, in which no two syntactically distinct type expressions denote the same type.
In languages with subtyping, the compatibility relation is more complex. In particular, if B is a subtype of A, then a value of type B can be used in a context where one of type A is expected, even if the reverse is not true. Like equivalence, the subtype relation is defined differently for each programming language, with many variations possible. The presence of parametric or ad hoc polymorphism in a language may also have implications for type compatibility.