In
computer science, a
type system may be defined as "a tractable syntactic method for proving the absence of certain program behaviors by classifying phrases according to the kinds of values they compute."
[1]. Loosely, a type system associates one (or more) type(s) with each program value; by examining the relation between types and expressions, a type system attempts to prove that no "type errors" can occur. The type system in question determines what constitutes a "type error", but type systems in common use generally seek to guarantee that operations expecting a certain kind of value are not used with values for which that operation makes no sense.
A
compiler may 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 accordance with the
IEEE specification for single-precision floating point numbers. C thus uses floating-point-specific operations on those values (floating-point addition, multiplication, etc.).
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 varying concrete algorithms on each type in the case of
type polymorphism.
Type theory is the study of type systems, although the concrete type systems of programming languages originate from practical issues of computer architecture, compiler implementation, and language design.
Fundamentals
Assigning data types (
typing) gives meaning to collections of
bits. Types usually have associations either with values in
memory or with
objects such as
variables. Because any value simply consists of a sequence of bits in a
computer, hardware makes no distinction even between
memory addresses,
instruction code,
characters,
integers and
floating-point numbers. Assignment to a type informs programs and programmers how those bit collections should be treated.
Major functions provided by type systems include:
- Safety - Use of types may allow a compiler to detect meaningless or probably invalid code. For example, we can identify an expression
3 / "Hello, World" as invalid because the rules of arithmetic do not specify how to divide an integer by a string. As discussed below, strong typing offers more safety, but generally does not guarantee complete safety (see type-safety for more information).
- Optimization - Static type-checking may provide useful compile-time information. For example, if a type requires that a value must align in memory at a multiple of 4 bytes, the compiler may be able to use more efficient machine instructions.
- Documentation - In more expressive type systems, types can serve as a form of documentation, since they can illustrate the intent of the programmer. For instance, timestamps may be represented as integers—but if a programmer declares a function as returning a timestamp type rather than merely an integer type, this documents part of the meaning of the function.
- Abstraction (or modularity) - Types allow programmers to think about programs at a higher level than the bit or byte, not bothering with low-level implementation. For example, programmers can think of a string as a collection of character values instead of as a mere array of bytes. Or, types can allow programmers to express the interface between two subsystems. This helps localize the definitions required for interoperability of the subsystems and prevents inconsistencies when those subsystems communicate.
Type safety contributes to
program correctness, but cannot guarantee it lest the type checking itself becomes an
undecidable problem. Depending on the specific type system, a program may give the wrong result and be safely typed, producing no compiler errors. For instance,
division by zero is not caught by the type checker in most programming languages; instead it is a
runtime error. To prove the absence of more general defects, other kinds of
formal methods, collectively known as
program analyses, are in common use, as well as
software testing—a widely used
empirical method for finding errors that the type checker cannot detect.
A program typically associates each value with one particular type (although a type may have more than one
subtype). Other entities, such as
objects,
modules, communication channels,
dependencies, or even types themselves, can become associated with a type. Some implementations might make the following identifications (though these are technically different concepts):
A
type system, specified in for each programming language, controls the ways typed programs may behave, and makes behavior outside these rules illegal. An
effect system typically provides more fine-grained control than does a type system.
Formally,
type theory studies type systems. More elaborate type systems (such as
dependent types) allow for more correct programs to be well-typed, but this comes at a price, as type inference and other properties generally become
undecidable, and type checking itself is dependent on user-supplied proofs. It is challenging to find a sufficiently expressive type system that satisfies all programming practices in
type safe manner. As
Mark Manasse concisely put it:
[2]
| “ | The fundamental problem addressed by a type theory is to insure that programs have meaning. The fundamental problem caused by a type theory is that meaningful programs may not have meanings ascribed to them. The quest for richer type systems results from this tension. | ” |
Type checking
The process of verifying and enforcing the constraints of types –
type checking – may occur either at
compile-time (a static check) or
run-time (a dynamic check). If a language specification requires its typing rules strongly (ie, more or less allowing only those automatic type conversions which do not lose information), one can refer to the process as
strongly typed, if not, as
weakly typed. The terms are not used in a strict sense.
Static typing
A programming language is said to use static typing when type checking is performed during compile-time as opposed to run-time. In static typing, types are associated with variables not values. Statically typed languages include
Ada,
C,
C++,
C#,
JADE,
Java,
Fortran,
Haskell,
ML,
Pascal,
Perl (with respect to distinguishing scalars, arrays, hashes and subroutines) and
Scala. Static typing is a limited form of
program verification (see
type safety): accordingly, it allows many type errors to be
caught early in the development cycle. Static type checkers evaluate only the type information that can be determined at compile time, but are able to verify that the checked conditions hold for all possible executions of the program, which eliminates the need to repeat type checks every time the program is executed. Program execution may also be made more efficient (i.e. faster or taking reduced memory) by omitting runtime type checks and enabling other optimizations.
Because they evaluate type information during compilation, and therefore lack type information that is only available at run-time, static type checkers are conservative. They will reject some programs that may be well-behaved at run-time, but that cannot be statically determined to be well-typed. For example, even if an expression
<complex test> always evaluates to
true at run-time, a program containing the code
if <complex test> then 42 else <type error>
will be rejected as ill-typed, because a static analysis cannot determine that the
else branch won't be taken.
[1] The conservative behaviour of static type checkers is advantageous when
<complex test> evaluates to
false infrequently: A static type checker can detect type errors in rarely used code paths. Without static type checking, even
code coverage tests with 100% code coverage may be unable to find such type errors. Code coverage 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.
The most widely
used statically typed languages are not formally
type safe. They have "
loopholes" in the
programming language specification enabling programmers to write code that circumvents the verification performed by a static type checker and so address a wider range of problems. For example, Java and most C-style languages have
type punning, and Haskell has such features as
unsafePerformIO: such operations may be unsafe at runtime, in that they can cause unwanted behaviour due to incorrect typing of values when the program runs.
Dynamic typing
A programming language is said to be dynamically typed, or just '
dynamic', when the majority of its type checking is performed at run-time as opposed to at compile-time. In dynamic typing, types are associated with values not variables. Dynamically typed languages include
Groovy,
JavaScript,
Lisp,
Lua,
Objective-C,
Perl (with respect to user-defined types but not built-in types),
PHP,
Prolog,
Python,
Ruby,
Smalltalk and
Tcl. Compared to static typing, dynamic typing can be more flexible (e.g. by allowing programs to generate types and functionality based on run-time data), though at the expense of fewer a priori guarantees. This is because a dynamically typed language accepts and attempts to execute some programs which may be ruled as invalid by a static type checker.
Dynamic typing may result in runtime type errors—that is, at runtime, a value may have an unexpected type, and an operation nonsensical for that type is applied. This operation may occur long after the place where the programming mistake was made—that is, the place where the wrong type of data passed into a place it should not have. This makes the bug difficult to locate.
Dynamically typed language systems, compared to their statically typed cousins, make fewer "compile-time" checks on the source code (but will check, for example, that the program is syntactically correct). Run-time checks can potentially be more sophisticated, since they can use dynamic information as well as any information that was present during compilation. On the other hand, runtime checks only assert that conditions hold in a particular execution of the program, and these checks are repeated for every execution of the program.
Development in dynamically typed languages is often supported by programming practices such as
unit testing. Testing is a key practice in professional software development, and is particularly important in dynamically typed languages. In practice, the testing done to ensure correct program operation can detect a much wider range of errors than static type-checking, but conversely cannot search as comprehensively for the errors that both testing and static type checking are able to detect. Testing can be incorporated into the
software build cycle, in which case it can be thought of as a "compile-time" check, in that the program user will not have to manually run such tests.
Combinations of dynamic and static typing
The presence of static typing in a programming language does not necessarily imply the absence of all dynamic typing mechanisms. For example, Java, and various other object-oriented languages, while using static typing, require for certain operations (
downcasting) the support of runtime type tests, a form of dynamic typing. See
programming language for more discussion of the interactions between static and dynamic typing.
Static and dynamic type checking in practice
The choice between static and dynamic typing requires
trade-offs.
Static typing can find type errors reliably at compile time. This should increase the reliability of the delivered program. However, programmers disagree over how commonly type errors occur, and thus what proportion of those bugs which are written would be caught by static typing. Static typing advocates believe programs are more reliable when they have been well type-checked, while 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
dependently typed 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.
[3]
Static typing usually results in compiled code that executes more quickly. When the compiler knows the exact data types that are in use, it can produce optimized machine code. Further, compilers for statically typed languages can find assembler shortcuts more easily. Some dynamically typed languages such as
Common Lisp allow optional type declarations for optimization for this very reason. Static typing makes this pervasive. See
optimization.
By contrast, dynamic typing may allow compilers to run more quickly and allow interpreters to dynamically load new code, since 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 which lack
type inference (such as Java and C) require that programmers declare the types they intend a method or function to use. This can serve as additional documentation for the program, which the compiler will not permit the programmer to ignore or permit to drift out of synchronization. However, a language can be statically typed without requiring type declarations (examples include
Haskell,
Scala and
C#3.0), so this is not a necessary consequence of static typing.
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 (however, the typing within that evaluated code might remain static). Furthermore, dynamic typing better accommodates transitional code and prototyping, such as allowing a placeholder data structure (
mock object) to be transparently used in place of a full-fledged data structure (usually for the purposes of experimentation and testing). Recent enhancements to statically typed languages (e.g. Haskell
Generalized algebraic data types) have allowed eval functions to be written in a statically type checked way.
[4]
Dynamic typing typically makes
metaprogramming more effective and easier to use. For example,
C++ templates are typically more cumbersome to write than the equivalent
Ruby or
Python code.
[citation needed] More advanced run-time constructs such as
metaclasses and
introspection are often more difficult to use in statically typed languages.
Static typing expands the possibilities for programmatic refactoring. For example, in a statically typed language, analysis of the source code can reveal all callers of a method, and hence a tool can consistently rename the method throughout all of its uses. In dynamic languages, this kind of analysis is either impossible or more difficult because the reference of a name (e.g. a method name) cannot surely be determined until runtime.
Strong and weak typing
One definition of
strongly typed involves preventing success for an operation on arguments which have the wrong type. A
C cast gone wrong exemplifies the problem of absent strong typing; if a programmer casts a value from one type to another in C, not only must the compiler allow the code at compile time, but the runtime must allow it as well. This may permit more compact and faster C code, but it can make
debugging more difficult.
Some observers use the term
memory-safe language (or just
safe language) to describe languages that do not allow undefined operations to occur. For example, a memory-safe language will
check array bounds, or else statically guarantee (i.e., at compile time before execution) that array accesses out of the array boundaries will cause compile-time and perhaps runtime errors.
Weak typing means that a language implicitly converts (or casts) types when used. Revisiting the previous example, we have:
var x := 5; // (1) (x is an integer)
var y := "37"; // (2) (y is a string)
x + y; // (3) (?)
In a weakly typed language, the result of this operation is not clear. Some languages, such as
Visual Basic, would produce runnable code producing the result 42: the system would convert the string "37" into the number 37 to forcibly make sense of the operation. Other languages like
JavaScript would produce the result "537": the system would convert the number 5 to the string "5" and then concatenate the two. In both Visual Basic and JavaScript, the resulting type is determined by rules that take both
operands into consideration. In some languages, such as
AppleScript, the type of the resulting value is determined by the type of the left-most operand only.
Safely and unsafely typed systems
Main article:
Type safetyA third way of categorizing the type system of a programming language uses the safety of typed operations and conversions. Computer scientists consider a language "type-safe" if it does not allow operations or conversions which lead to erroneous conditions.
var x := 5; // (1)
var y := "37"; // (2)
var z := x + y; // (3)
In languages like
Visual Basic variable z in the example acquires the value 42. While the programmer may or may not have intended this, the language defines the result specifically, and the program does not crash or assign an ill-defined value to z. In this respect, such languages are type-safe; however, if the value of y was a string that could not be converted to a number (eg "hello world"), the results would be undefined. Such languages are type-safe (in that they will not crash) but can easily produce undesirable results.
Now let us look at the same example in C:
int x = 5;
char y[] = "37";
char* z = x + y;
In this example z will point to a memory address five characters beyond y, equivalent to three characters after the terminating zero character of the string pointed to by y. The content of that location is undefined, and might lie outside addressable memory. The mere computation of such a pointer may result in undefined behavior (including the program crashing) according to C standards, and in typical systems
dereferencing z at this point could cause the program to crash. We have a well-typed, but not memory-safe program — a condition that cannot occur in a type-safe language.
Polymorphism and types
The term "polymorphism" refers to the ability of code (in particular, methods or classes) 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 (in some cases)
subtyping.
Duck typing
Main article:
Duck typingIn "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 implement the method called. One way of looking at this is that in "duck" typing systems the type of an object is intrinsic to the object and is determined by what methods it implements, and hence that a "duck" typing system is by definition type-safe since one can only invoke operations an object actually implements. Another way of looking at this is that the object is a member of
several types, including a type that describes the fact that it "has a method
m." Type checking however occurs only on demand at runtime, every time the method
m needs to be executed, not at compile-time or load-time.
Duck typing differs from
structural typing in that, if the
part (of the whole module structure) 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 (as contrasted to compile-time) 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.
Initially coined by
Alex Martelli in the
Python community, duck typing uses the premise that (referring to a value) "if it walks like a duck, and quacks like a duck, then it is a duck".
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.
Dependent types
Dependent types are based on the idea of using scalars or values to more precisely describe the type of some other value. For example, "matrix(3,3)" might be the type of a 3×3 matrix. We can then define typing rules such as the following rule for matrix multiplication:
- matrix_multiply : matrix(k,m) × matrix(m,n) → matrix(k,n)
where
k,
m,
n are arbitrary positive integer values. A variant of
ML called
Dependent ML has been created based on this type system, but because type-checking conventional dependent types is
undecidable, not all programs using them can be type-checked without some kind of limitations. 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, it is also possible to make the language Turing complete at the price of undecidable type checking like in
Cayenne .
Linear types
Linear types, 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 strings, files, and so on, because any operation that simultaneously destroys a linear object and creates a similar object (such as '
str = str + "a"') can be optimized "under the hood" into an in-place mutation. Normally this is not possible because 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 (a
Haskell-like language) uses this type system in order to gain a lot of speed while remaining safe.
Intersection types
Intersection types 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 "int → int" is the type of functions taking an integer argument and returning an integer, and "float → float" 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 "int → int" function safely; it simply would not use the "float → float" functionality.
In a subclassing hierarchy, the intersection of a type and an ancestor type (such as its parent) 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
Union types are types describing values that belong to
either of two types. For example, in C, the signed char has range -128 to 127, and the unsigned char has range 0 to 255, so the union of these two types would have range -128 to 255. 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 because 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 (eg, value or type) is not known.
In a subclassing hierarchy, the union of a type and an ancestor type (such as its parent) is the ancestor type. The union of sibling types is a subtype of their common ancestor (that is, all operations permitted on their common ancestor are permitted on the union type, but they may also have other valid operations in common).
Existential types
Existential types are frequently used to represent
modules and
abstract data types because of their ability to separate implementation from interface. For example, in C pseudocode, the type "T = ∃X { X a; int f(X); }" describes a module interface that has a data member of type
X and a function that takes a parameter of the
same type
X and returns an integer. This could be implemented in different ways; for example:
- intT = { int a; int f(int); }
- floatT = { float a; int f(float); }
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(t.a)" 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 { int a; int f(int); } could also have the type ∃X { X a; int f(int); }. The simplest solution is to annotate every module with its intended type, e.g. (we depart from C-style syntax of writing the type first to make the example clear)
- intT = { int a; int f(int); } as ∃X { X a; int f(X); }
Although abstract data types and modules had been implemented in programming languages for quite some time, it wasn't unitl 1988 that
John C. Mitchell and
Gordon Plotkin established the formal theory under the slogan: "Abstract [data] types have existential type".
[5] The theory is a second-order
typed lambda calculus similar to
System F, but with existential instead of universal quantification. Existential types are implemented in
Haskell98.
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 particular 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
f(x,y) which adds
x and
y together, the compiler can infer that
x and
y must be numbers – since addition is only defined for numbers. Therefore, any call to
f elsewhere in the program that specifies a non-numeric type (such as a string or list) 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
3.14 might imply a type of
floating-point, while
[1, 2, 3] might imply a list of integers – typically an
array.
Type inference is in general possible if it is
decidable in the type theory in question. Moreover, even if inference is undecidable in general for a given type theory, 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 decidable. Most Haskell compilers allow arbitrary-rank polymorphism as an extension, but this makes type inference undecidable. (Type checking is decidable, however, and rank-1 programs still have type inference; higher rank polymorphic programs are rejected unless given explicit type annotations.)
Types of types
A
type of types is a
kind. Kinds appear explicitly in
typeful programming, such as a
type constructor in the
Haskell programming language.
Types fall into several broad categories:
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 instance, 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. In the simplest type systems, therefore, the question of whether two types are compatible reduces to that of whether they are
equal (or
equivalent). 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 are equivalent that describe values with the same structure, and
nominative type systems, in which no two syntactically distinct type expressions denote the same type (
i.e., types must have the same "name" in order to be equal).
In languages with
subtyping, the compatibility relation is more complex. In particular, if
A is a subtype of
B, then a value of type
A can be used in a context where one of type
B 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.
Controversy
There are often conflicts between those who prefer statically typed languages and those who prefer dynamically typed languages. The first group advocates for the early detection of type errors during compilation and increased runtime performance, while the latter group advocates for rapid prototyping that is possible with a more dynamic typing system and that type errors are only a small subset of errors in a program.
[6][7] Related to this is the consideration that often there is no need to manually declare all types in statically typed programming languages with type inference; thus, the need for the programmer to explicitly specify types of variables is automatically lowered for such languages; and some dynamic languages have run-time optimisers
[8][9] that can generate fast code approaching the speed of static language compilers, often by using partial type inference.
