Type system
lastmod 2022-08-18created 2017-10-313 edits
In computer science, a type system is a set of rules that classifies values, expressions, functions, modules, and so on. More formally, it is defined as "a tractable method for proving the absence of certain kinds of program errors by classifying the values to be computed."
In a type system, each computed value has a type. The type system examines the flow of values within a program and prevents values that do not match their type from being assigned. Assigning a value that does not match its type is called a type error. Operations between logically incompatible types and access to invalid memory fall into this category. Exactly which operations count as type errors depends on the type system.
Through static types, a compiler can optimize the storage needed for each variable and the algorithms for operations on it. For example, the "float" type in many C compilers is represented in 32 bits, following the IEEE standard for single-precision floating-point numbers. The C compiler can therefore use the matching machine instructions for operations on variables of the float type.
The depth of type constraints and the way they are evaluated affect the typing of the language. In the case of type polymorphism, a programming language can additionally associate an operation with various concrete algorithms for each type. Type theory is the study of type systems arising from practical problems in computer architecture, compiler implementation, and language design.