Dependent Type Theory: Proofs, Data, and Universes

Simple types distinguish functions from their arguments and connect implication with abstraction. Mathematical specifications often need more information. A vector's type may depend on its length. A result may consist of an object together with evidence that the object satisfies a property.

Dependent type theory allows types to depend on terms. This makes the relationship between proofs and programs expressive enough to support substantial mathematics, while placing new demands on the rules for computation and equality.

A developing foundational program

Per Martin-Löf developed successive formulations of intuitionistic type theory from the early 1970s onward. The formulations changed in their treatment of universes, equality, and the relationship between mathematical judgments and internal propositions.

It is therefore misleading to attribute every feature of later dependent-type systems to a single presentation. The 1984 Intuitionistic Type Theory, based on lectures given in 1980, is one important reference point within a continuing development.

Other lines contributed to the emerging landscape. De Bruijn's Automath project investigated mechanically checked mathematical language. Jean-Yves Girard and John Reynolds independently developed second-order polymorphic lambda calculi, now associated with System F.

Polymorphism permits a term to be used uniformly across types. Dependence permits a type to refer to a term. These mechanisms can be combined, but they are distinct.

Judgments and contexts

A type theory does more than list propositions. It specifies judgments that say whether an expression is a type, whether a term has a type, and whether expressions are definitionally equal.

A context might contain

Later declarations depend on earlier ones. The expression for the type of $v$ uses both the type $A$ and the number $n$.

Context formation therefore matters. A declaration cannot generally refer to a variable that has not yet been introduced. Substitution must preserve both the terms and the types that depend on them.

This disciplined treatment of context is one reason a compact mathematical phrase can require substantial elaboration before a checker sees its precise formal meaning.

Dependent products and sums

The dependent product

is a type of functions that, for each $x:A$, produce a term of type $B(x)$. When $B$ does not depend on $x$, it reduces to an ordinary function type.

Under propositions as types, it supplies the constructive interpretation of universal quantification: give a construction that works for an arbitrary input.

The dependent sum

contains pairs $(a,b)$ where $a:A$ and $b:B(a)$. The second component's type depends on the first component's value.

For example,

can contain the number $11$ paired with a proof that $11>10$.

This is a data-bearing specification. Some assistants also provide an existential proposition in a separate logical universe with restricted elimination into data. One must not infer that every existential proof in every implementation permits unrestricted extraction of a computational witness.

A length-indexed vector

Consider a family $\operatorname{Vec}(A,n)$ with constructors

and

For elements $a,b:A$, the expression

has length two, with the length arguments left implicit here for readability.

A head operation can have type

Its input type excludes an empty vector. Pattern matching on the possible constructor supplies an element of $A$.

The claim is stronger than “the function usually receives a nonempty list.” The length restriction is part of the expression that type checking must verify. Whether that expression accurately captures the application's needs remains a separate specification question.

Computation inside type checking

Suppose a function expects a vector of length $1+1$, and we supply one of length $2$. In a theory whose natural-number computation rules reduce $1+1$ to $2$, the types can be definitionally equal.

No separate proof of equality needs to be passed at this point. The checker uses the specified computation rules.

Now compare lengths $n+0$ and $n$ for a variable $n$. Whether these are definitionally equal can depend on the chosen recursive definition of addition. If addition computes by recursion on its first argument, $n+0$ may not reduce when $n$ is a variable, even though a theorem proves the equality.

One then uses propositional equality to transport a vector between the corresponding types. A mathematically obvious equality may therefore require explicit evidence because it is not one of the equalities recognized by computation alone.

This distinction is essential to understanding proof assistants. Definitional equality governs conversion during checking; propositional equality is represented by an internal type whose inhabitants can be used in proofs.

Identity and elimination

An identity type $\operatorname{Id}_A(a,b)$ expresses an equality between terms of type $A$. Reflexivity supplies a canonical inhabitant when the endpoints agree.

Its elimination principle explains how a construction valid for reflexivity extends to general identity evidence. In a dependent setting, this supports transport: if $P$ is a family of types and $a=b$, an inhabitant of $P(a)$ can be moved to $P(b)$.

Different theories make different choices about how identity interacts with judgmental equality. Extensional equality reflection, for example, has substantial consequences for type checking.

Intensional identity also leaves room for the richer interpretations examined in Homotopy Type Theory. Those interpretations should not be assumed in advance merely because a system has dependent types.

Induction is part of the logical design

Inductive types provide constructors and principles for defining functions or proving properties by analyzing those constructors.

For natural numbers, the induction principle takes a proof of $P(0)$ and a method taking $P(n)$ to $P(n+1)$, and produces a proof of $P(n)$ for every natural number.

A recursive function and an inductive proof can therefore share the same structural organization.

Unrestricted recursion would threaten the normalization properties needed for a direct proofs-as-terms foundation. Systems consequently impose conditions on recursive definitions. Likewise, restrictions such as strict positivity control which inductive definitions are admitted.

These restrictions are mathematical safeguards built into the formal theory. They are not merely inconveniences imposed by an implementation.

Universes and the limits of type formation

A universe lets a theory speak internally about a collection of types. Its formation rules determine how much self-reference and quantification the system permits.

Girard's paradox showed that powerful combinations of dependent type formation and an unrestricted type of all types can be inconsistent. Martin-Löf revised an early formulation in response.

A common approach uses a hierarchy

A universe is then contained in a higher universe rather than being an unrestricted member of itself. Cumulativity, resizing, and impredicativity are further choices, each requiring a precise formulation.

The historical lesson resembles the response to set-theoretic paradoxes: expressive comprehension principles need careful limits. It does not follow that every impredicative type theory is inconsistent.

Constructions and inductive constructions

Thierry Coquand and Gérard Huet developed the Calculus of Constructions in the 1980s, combining dependent types with powerful forms of polymorphism. Their journal presentation appeared in 1988.

Work by Coquand, Christine Paulin-Mohring, and collaborators developed inductive types and the relationship between proofs and extracted programs. Paulin-Mohring's research is central to the account, including the rules and properties of inductive definitions in Coq. The project's publication bibliography records these developments.

This lineage became a basis for major proof-assistant implementations. Implementation choices concerning propositions, proof irrelevance, universes, elimination, and computation must still be described system by system.

A successful proof term is checked against a specific formal theory. The phrase “dependent type theory” identifies a family of foundations, not a single universal specification.

Toward structural semantics

Dependent types organize proofs through judgments, terms, and reduction rules. Another development asks how logical operations can be characterized through mathematical structure, independently of a particular symbolic presentation.

Sources and further reading

• Per Martin-Löf, Intuitionistic Type Theory (1984), based on the Padua lectures of 1980.
• Jean-Yves Girard, Interprétation fonctionnelle et élimination des coupures de l'arithmétique d'ordre supérieur (1972).
• John C. Reynolds, “Towards a Theory of Type Structure” (1974).
• Thierry Coquand and Gérard Huet, “The Calculus of Constructions” (1988).
• Thierry Coquand and Christine Paulin-Mohring, “Inductively Defined Types” (1988); Christine Paulin-Mohring, “Inductive Definitions in the System Coq: Rules and Properties” (1993).
• Rocq research bibliography, containing the historical Coq papers; Paulin-Mohring's publication list.