Type theory is the study of systems that classify the terms of a formal language by assigning each one a type. The Stanford Encyclopedia of Philosophy entry on type theory describes it as “fundamental both in logic and computer science,” and explains that types serve as a classification system for terms that prevents self-reference paradoxes.
The historical motivation was logical. The Stanford entry shows how distinguishing “objects, predicates, predicate of predicates, etc.” blocks Russell’s paradox: a predicate cannot be applied to itself because its type forbids it. By making the paradoxical sentence syntactically ill-formed rather than merely false, the type discipline keeps the system consistent.
The same discipline carries directly into programming. A type checker rejects programs that try to use a value in a way its type does not allow, which is the practical meaning of the slogan that well-typed programs “cannot go wrong.” This is why typed functional languages and proof assistants such as Coq, Agda, and Lean are all built on type theory.
Type theory connects to many of the ideas in this library. It supplies the rules behind type inference and parametric polymorphism, and through the Curry-Howard correspondence it ties types to logical propositions and programs to proofs.