---
tag: 42A2M9S2C1
kind: definition
name: Type theory
msc: ["03B38", "03B16"]
defines: Q48KGV33AH
uses: [0HESMMSYEG, 0BSJ7RQ9BW, 0XHDTE5YMZ]
sources:
  - url: https://en.wikipedia.org/wiki/Type_theory
---

## Definition

A *type theory* is a formal system with these parts.

1. A collection of *types*, built from base types by type constructors.
2. A collection of *terms*, built from variables and constants by term constructors.
3. *Judgments*, in particular the typing judgment $\Gamma \vdash t : A$, which says that in the context $\Gamma = (x_1 : A_1, \dots, x_n : A_n)$ the term $t$ has type $A$.
4. *Inference rules*, which say which judgments can be derived from which, and a notion of computation or equality on terms.

Every well-formed term has a type, and a term can only be used where its type allows.

## Remarks

Example: Church's simply typed lambda calculus is a type theory.
Its types are built from base types by the arrow $A \to B$.
Its rules include: if $\Gamma, x : A \vdash t : B$, then $\Gamma \vdash \lambda x.\, t : A \to B$; and if $\Gamma \vdash f : A \to B$ and $\Gamma \vdash a : A$, then $\Gamma \vdash f\, a : B$.
Non-example: the untyped lambda calculus is not a type theory, because its terms carry no types.
In it, the self-application $\lambda x.\, x\, x$ is a legal term, while in the simply typed calculus it has no type.
In *dependent* type theories, types may depend on terms, as in the type $\mathrm{Vec}(n)$ of lists of length $n$.
Unlike a [[set|0BSJ7RQ9BW]], a term has its type as part of its form, and "$t$ has type $A$" is a judgment, not a proposition that can be true or false.
This is how type theory avoids [[Russell's paradox|0HESMMSYEG]].