In programming language theory, a branch of computer science, type theory provides the formal basis for the design, analysis and study of type systems. Indeed, many computer scientists use the term type theory to refer to the formal study of type systems for programming languages, although some limit it to the study of more abstract formalisms such as typed λ-calculi. At the broadest level, type theory is the branch of mathematics and logic that concerns itself with classifying entities into collections called types. In this sense, it is related to the metaphysical notion of 'type'. Modern type theory was invented partly in response to Russell's paradox, and features prominently in Russell and Whitehead's Principia Mathematica.

History of type theory

Practical impact of type theory

Connections to constructive logic

Relation to other topics

Type system

Definitions of type system vary, but the following one due to Benjamin C. Pierce roughly corresponds to the current consensus in the programming language theory community:

type system is a tractable syntactic method for proving the absence of certain program behaviors by classifying phrases according to the kinds of values they compute.
(Pierce, 2002)

In other words, a type system divides program values into sets called types (this is called a "type assignment"), and makes certain program behaviors illegal on the basis of the types that are thus assigned. For example, a type system may classify the value "hello" as a string and the value 5 as a number, and prohibit the programmer from adding "hello" to 5 based on that type assignment. In this type system, the program

"hello" + 5

would be illegal. Hence, any program permitted by the type system would be provably free from the erroneous behavior of adding strings and numbers.

The design and implementation of type systems is a topic nearly as broad as the topic of programming languages itself. In fact, type theory proponents commonly proclaim that the design of type systems is the very essence of programming language design: "Design the type system correctly, and the language will design itself."

See also

• Intuitionistic Type Theory for the original type theory in mathematics
• Type system for a more practical discussion of type systems for programming languages
• Duck typing for a trivial solution to typing in some programming languages
• Data type for concrete types of data in programming

• Domain theory
• Category theory

Further reading

• Peter B. Andrews, An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof, Second Edition, Kluwer Academic Publishers, 2002. ^*
• Benjamin Pierce, Types and Programming Languages, MIT Press, 2002. (ISBN 0-262-16209-1)
• Glynn Winskel: The Formal Semantics of Programming Languages, An Introduction, The MIT Press 1993 (ISBN 0-262-23169-7)
• Luca Cardelli, "Type Systems," The Computer Science and Engineering Handbook, Allen B. Tucker (Ed.), chapter 103, pp. 2208-2236, CRC Press, Boca Raton, FL, 1997. (online)
• Simon Thompson, Type Theory and Functional Programming, Addison-Wesley, 1991, ISBN 0-201-41667-0, ^*.

External links

• Abstract data type
• A summary paper on the formal basis of ADTs, relationship to category theory, and list of good references. Pages 3-4 appear relevant. Reference number ^* looks good, but it may not be available online.
• Naïve Computational Type Theory by Robert L. Constable
• Introduction to Type Theory (The Nuprl Book)

Mathematical logic | Logic in computer science | Type theory

Typentheorie | Théorie des types | Teoria dei tipi | טיפוס (לוגיקה מתמטית) | Теория типов | 类型论