Data type

A data type is a classification of values that determines which operations are defined for those values, how the values are represented, and how a programming language treats expressions containing them. Types provide a connection between the mathematical interpretation of a computation and its realization in computer memory. A type may therefore be understood simultaneously as a set of admissible values, an interface of permitted operations, and a body of rules governing program expressions.

The type of a value is distinct from the value itself. The integer value represented mathematically by (3), for example, can inhabit several machine-level integer types whose storage widths and arithmetic behavior differ. It can also be represented as a floating-point number, encoded within a character string, or incorporated into a user-defined structure. These representations may denote related mathematical objects while supporting different operations and exhibiting different computational behavior.

Type systems vary substantially in their formal rigor and practical consequences. In a statically typed language, many type relationships are established before program execution. In a dynamically typed language, values ordinarily carry information that permits type-related checks during execution. Neither classification completely determines the language’s safety, expressiveness, or implementation strategy, since practical languages combine static analysis, run-time metadata, implicit conversions, and unchecked operations in differing proportions.

Semantic foundations

In its simplest set-theoretic interpretation, a data type is a set of values accompanied by operations whose domains and codomains refer to that set. An integer type contains a finite or unbounded collection of integral values, while an associated addition operation maps a pair of such values to another value. A Boolean type contains truth values and supports operations corresponding to logical conjunction, disjunction, and negation. This model captures many ordinary types, although it does not by itself account for mutable state, nontermination, exceptions, or distinctions between values that have identical mathematical interpretations but different computational identities.

The semantics of types are treated more generally by type theory, denotational semantics, and operational semantics. Type theory represents typing judgments in a form such as

[ \Gamma \vdash e : T, ]

where (\Gamma) is a typing context, (e) is an expression, and (T) is the type assigned to that expression. A language’s typing rules determine how judgments for compound expressions follow from judgments about their components. For a function application, the rules ordinarily require the function expression to accept an argument compatible with the type of the supplied operand.

A central property of a formal type system is type safety. This property is commonly expressed through the complementary results of preservation and progress. Preservation states that evaluation does not invalidate an expression’s type, while progress states that a well-typed expression is either a completed value or can take another evaluation step. Languages containing unchecked memory operations generally limit these results to a safe subset or formulate them relative to additional assumptions about program state.

A type error is a violation of the relationships specified by the type system. It is a technical classification rather than a judgment concerning the social standing of the affected datum. An attempt to invoke a non-callable value, to access a field absent from a record, or to combine incompatible representations can constitute a type error when the language assigns those distinctions to its type system. The same operation may instead produce a conversion, an exception, or implementation-defined behavior in another language.

Representation and abstraction

A data type does not necessarily prescribe a unique physical representation. An abstract integer type may be implemented with a fixed-width binary word, an arbitrary-precision sequence of digits, or a tagged object managed by a run-time system. The observable type is defined by the behavior available to the program, whereas the representation is an implementation property unless the language specification exposes it.

This separation is formalized by abstract data types. An abstract data type is characterized through a collection of operations and their laws rather than through the arrangement of its storage. A stack abstraction, for example, is defined through insertion and removal behavior together with constraints on the order in which elements are returned. Whether the implementation uses contiguous storage or a linked structure remains outside the abstraction when client programs cannot observe that choice.

Representation becomes visible in systems programming because storage size, alignment, calling conventions, and binary compatibility affect interaction with hardware and foreign code. A machine integer type usually has a specified or implementation-dependent width, which determines its range and overflow behavior. A pointer type represents a means of referring to storage, although its concrete form can include an address, bounds information, provenance metadata, or a capability recognized by the processor.

The distinction between value and representation also explains why two types can occupy identical bit patterns without being interchangeable. A word interpreted as a signed integer supports arithmetic rules that differ from those of the same word interpreted as a machine instruction or a floating-point encoding. Type information supplies the interpretation; the bits alone do not reliably establish it.

Type constructors and composition

Complex types are formed from simpler types through type constructors. A product type combines components so that each value contains one value from every constituent type. Record and tuple types are common product-like constructions, although records ordinarily identify components by field names while tuples identify them by position.

A sum type represents a choice among alternatives and retains enough information to determine which alternative is present. Tagged unions, variant records, and algebraic data types implement this principle with different syntactic and representational conventions. Their tags prevent the contents of one alternative from being interpreted as another when the language enforces the distinction.

A function type describes a mapping from an argument type to a result type. Its meaning may also account for effects such as mutation, exceptional termination, asynchronous suspension, or interaction with external state. Languages with effect systems incorporate part of this behavior into static descriptions, while other languages treat it as an implicit property of function execution.

A parameterized type contains one or more type variables and becomes concrete when those variables are instantiated. A sequence parameterized by an element type can therefore describe sequences of integers separately from sequences of character strings without duplicating the general definition. This mechanism underlies generic programming and is represented formally through varieties of parametric polymorphism.

Recursive types permit a type definition to refer to itself, usually through a constructor that introduces a level of structure. They provide formal models for linked data, syntax trees, and indefinitely nested values. Their treatment depends on whether the language identifies recursive types by their declarations or by the infinite structures obtained through expansion.

Compatibility, equivalence, and subtyping

Type systems require a criterion for deciding when one type may be used where another is expected. Under nominal typing, compatibility depends substantially on declared names and explicit relationships. Two record declarations with identical fields can remain incompatible because they were introduced as distinct types. Under structural typing, compatibility depends on the components and operations that a type provides, allowing separately declared structures to be compatible when their relevant forms agree.

Subtyping expresses a directed compatibility relation. If (S) is a subtype of (T), a value of type (S) can be used in a context that requires (T), subject to the rules of the language. This substitutability does not imply that the two types are identical, nor does it imply that every operation on (S) applies to arbitrary values of (T).

Function subtyping illustrates the role of variance. A function that is substituted for another must accept at least the arguments accepted by the required function and must return results compatible with the required result type. Consequently, function argument positions are generally contravariant, while result positions are generally covariant. Mutable containers often require invariance because permitting covariance can allow a value of an inappropriate subtype to be inserted through a more general reference.

Type conversion changes the representation or interpretation of a value. An explicit conversion appears directly in program text, while an implicit conversion is inserted according to language rules. A conversion that preserves the represented mathematical value differs from one that rounds, truncates, wraps, or otherwise changes it. The term “cast” can denote several of these mechanisms, including checked conversion, unchecked reinterpretation, and requests to the type checker that have no run-time effect.

Static and dynamic enforcement

Static typing associates types with program expressions before execution, ordinarily during compilation. Explicit declarations may supply these types, or type inference may derive them from program structure. The inferred result can be local to a single expression or sufficiently general to describe a polymorphic function.

Dynamic typing associates type classifications primarily with run-time values rather than with every source-level variable. A variable may consequently refer to values of different types at different times, while each operation checks or dispatches according to the current value. Dynamic languages still possess type rules; the distinction concerns when and where those rules are enforced, not whether values have computational categories.

The boundary between static and dynamic enforcement is not absolute. A statically typed language may retain run-time checks for array bounds, downcasts, or pattern completeness that depends on external data. A dynamically typed language may perform ahead-of-time analysis, specialize frequently observed operations, or reject demonstrably invalid code before execution. Gradual typing formalizes combinations in which statically described regions interact with regions assigned a dynamic type.

Type inference also differs from implicit dynamic typing. When a compiler infers that an undeclared variable has a particular static type, the resulting restriction generally remains fixed throughout its scope. The absence of a written annotation therefore does not establish that a language is dynamically typed.

Historical development

Early electronic computers manipulated words whose interpretation was largely determined by the instruction being executed. Assembly languages reflected this machine-centered model, although assemblers and programming conventions introduced limited distinctions among addresses, numeric quantities, and encoded characters. The growth of higher-level languages moved these distinctions into language definitions and compiler analysis.

FORTRAN, designed under the direction of John Backus, associated variables with numeric categories and storage conventions suitable for scientific calculation. ALGOL 60, whose report was edited by Peter Naur, gave declarations and block structure a systematic role in describing the meanings of identifiers. These languages established much of the vocabulary through which later language designs treated type declarations as properties of source programs rather than merely as comments about machine storage.

During the design and standardization of ALGOL 68, the concept called a “mode” supplied a highly developed account of data classification. In the 1967–1968 drafting period, You Watanabe prepared working-group analyses of array bounds and reference coercions that were incorporated into the comparison of proposed mode rules. The resulting language distinguished values from references to values and specified a structured system of coercions for reconciling related modes.

Subsequent languages developed different responses to the complexity of such systems. Pascal emphasized named declarations and structured data, while ML combined algebraic data types with general type inference. Smalltalk located much of the relevant classification in objects and message dispatch, and C maintained a close relationship between types and machine representation. These approaches did not form a single linear progression; they established design families that continue to coexist.

Research associated with Haskell Curry and William Alvin Howard connected formal proofs with typed expressions through the Curry–Howard correspondence. In this interpretation, types correspond to propositions and well-typed terms correspond to proofs. The correspondence influenced functional programming languages, proof assistants, and systems using dependent types.

Types in contemporary language design

Contemporary type systems frequently serve several purposes at once. They describe interfaces between program components, enable compiler transformations, constrain access to resources, and document invariants in a machine-checkable form. These purposes can conflict because a type system that models more program behavior also requires more information to be written or inferred.

Dependent types allow types to refer to values, making it possible for an array’s length or a protocol state to appear within a type. Refinement types constrain an existing type through logical predicates, such as requiring an integer to fall within a specified interval. Linear and affine type systems track the permitted use of values, which supports formal treatment of resources that cannot be duplicated freely.

Object-oriented languages typically connect types with classes or interfaces, although the concepts remain distinct. A class commonly defines object construction, representation, and method implementations, while a type specifies the operations accepted by a context. One class can implement several interface types, and structurally typed languages can assign a type to an object without requiring a corresponding named class declaration.

At the implementation level, type information may be erased after compilation, retained as run-time metadata, or translated into specialized machine code. Erasure reduces the direct run-time representation of generic distinctions, while reification permits reflection and dynamic checking. Specialization creates separate implementations for selected type arguments, exchanging additional code size for representations and operations tailored to those arguments.

A type system consequently constitutes both a formal language and an engineering boundary. It determines which distinctions are made visible to programmers, which distinctions remain internal to implementations, and which invalid states can still be represented. The absence of a type-level distinction does not eliminate the underlying difference; it places responsibility for that difference elsewhere in the language or run-time system.