6 min read
On this page

Dependent Types

Core Idea

Type System Features Hierarchy

Dependent types are types that depend on values. This unifies the term and type levels, allowing types to express precise specifications.

In simple types, A -> B says "given any A, produce a B." With dependent types, (x : A) -> B(x) says "given x of type A, produce a value of type B(x)" where B may mention x. The type of the output depends on the value of the input.

Pi Types (Dependent Function Types)

The Pi type (product type) generalizes function types:

Pi (x : A). B(x) or (x : A) -> B(x)

An inhabitant of Pi (x : A). B(x) is a function that, given x : A, returns a value of type B(x).

Typing rules:

Gamma |- A : Type    Gamma, x:A |- B : Type
--------------------------------------------  (Pi-Form)
Gamma |- Pi (x:A). B : Type

Gamma, x:A |- M : B
--------------------------------------------  (Pi-Intro / Lambda)
Gamma |- lambda x. M : Pi (x:A). B

Gamma |- M : Pi (x:A). B    Gamma |- N : A
--------------------------------------------  (Pi-Elim / App)
Gamma |- M N : B[x := N]

Special case: When B does not mention x, Pi (x:A). B degenerates to A -> B (ordinary function type).

Examples:

  • vector_head : Pi (n : Nat). Vec A (n + 1) -> A -- type ensures non-empty vector
  • matrix_mult : Pi (m n p : Nat). Mat m n -> Mat n p -> Mat m p -- dimensions must match

Sigma Types (Dependent Pair Types)

The Sigma type (sum type) generalizes pairs:

Sigma (x : A). B(x) or (x : A) * B(x)

An inhabitant is a pair (a, b) where a : A and b : B(a). The type of the second component depends on the value of the first.

Typing rules:

Gamma |- A : Type    Gamma, x:A |- B : Type
--------------------------------------------  (Sigma-Form)
Gamma |- Sigma (x:A). B : Type

Gamma |- a : A    Gamma |- b : B[x := a]
--------------------------------------------  (Sigma-Intro / Pair)
Gamma |- (a, b) : Sigma (x:A). B

Gamma |- p : Sigma (x:A). B
Gamma, x:A, y:B |- C : Type
Gamma, x:A, y:B |- M : C[(x,y) := p]        (Sigma-Elim)
--------------------------------------------
Gamma |- let (x, y) = p in M : C[p]

Special case: When B does not mention x, Sigma (x:A). B = A * B (ordinary pair type).

As logical connective: Under Curry-Howard, Sigma types correspond to existential quantification: Sigma (x:A). B(x) = "there exists x:A such that B(x)."

Universes

Universes are "types of types," resolving the paradox of "Type : Type" (which leads to Girard's paradox / inconsistency).

Universe hierarchy: Type_0 : Type_1 : Type_2 : ...

Each Type_i contains types at level i but not itself. The rules:

  • If A : Type_i, then A : Type_{i+1} (cumulativity)
  • If A : Type_i and B : Type_i, then A -> B : Type_i
  • Type_i : Type_{i+1}

Universe polymorphism: To avoid duplicating definitions at each level, modern systems support universe-polymorphic definitions: id : forall {i}. (A : Type_i) -> A -> A.

Typical ambiguity: Coq and Lean allow omitting universe levels, inferring them automatically and checking consistency.

Prop vs Type: Some systems (Coq) distinguish Prop (propositions, proof-irrelevant) from Type (data). Prop : Type_0, and Prop is impredicative (forall A:Prop. A is in Prop), while Type levels are predicative.

Inductive Types

Inductive types define types by specifying constructors. The elimination principle (recursion/induction) is derived.

Basic Examples

Inductive Nat : Type :=
  | zero : Nat
  | succ : Nat -> Nat

Inductive List (A : Type) : Type :=
  | nil : List A
  | cons : A -> List A -> List A

Indexed Inductive Types (Inductive Families)

Types can be indexed by values, enabling precise specifications:

Inductive Vec (A : Type) : Nat -> Type :=
  | vnil : Vec A 0
  | vcons : forall n, A -> Vec A n -> Vec A (n + 1)

The type Vec A n enforces the length invariant at the type level.

Inductive Fin : Nat -> Type :=    -- finite sets {0, ..., n-1}
  | fzero : forall n, Fin (n + 1)
  | fsucc : forall n, Fin n -> Fin (n + 1)

W-Types (Well-Founded Trees)

W-types are a general form of inductive types in type theory:

Given A : Type and B : A -> Type, the W-type W(x:A). B(x) consists of well-founded trees where:

  • Each node is labeled with a : A
  • Each node has |B(a)| children
W (x : A). B(x) has constructor:
  sup : (a : A) -> (B(a) -> W(x:A).B(x)) -> W(x:A).B(x)

Examples:

  • Natural numbers: A = Bool, B(true) = Empty (zero has no children), B(false) = Unit (successor has one child)
  • Binary trees: A = Bool, B(true) = Empty (leaf), B(false) = Bool (internal node has two children)
  • Lists of A: A' = Unit + A, B(inl tt) = Empty (nil), B(inr a) = Unit (cons has one child)

W-types, together with Pi, Sigma, identity types, and universes, suffice to derive all inductive types in extensional type theory.

The Calculus of Constructions (CoC)

The Calculus of Constructions (Coquand-Huet, 1988) is at the apex of the lambda cube, combining dependent types, polymorphism, and type operators.

Sorts: Prop, Type (or *, Box in original notation) Core rules (PTS formulation):

  • Axiom: Prop : Type
  • Rules: (Prop, Prop, Prop), (Prop, Type, Type), (Type, Prop, Prop), (Type, Type, Type)

This allows:

  • Terms depending on terms (ordinary functions): (Prop, Prop)
  • Terms depending on types (polymorphism): (Type, Prop)
  • Types depending on terms (dependent types): (Prop, Type) -- wait, actually this is (Type, Prop)
  • Types depending on types (type operators): (Type, Type)

Prop is impredicative: forall (P : Prop). P is itself in Prop. This enables encoding of inductive types via Church-style encodings within the theory.

Strong normalization: CoC is strongly normalizing (Coquand, 1986), hence consistent as a logic.

The Calculus of Inductive Constructions (CIC)

CIC (Paulin-Mohring, 1993) extends CoC with primitive inductive types, forming the basis of Coq (now Rocq). Key additions:

  1. Inductive definitions with strict positivity checking (ensures consistency)
  2. Pattern matching with dependent elimination
  3. Universe hierarchy Type_0 : Type_1 : ... (predicative)
  4. Prop remains impredicative (for proof irrelevance)
  5. Fixpoint definitions with structural recursion (termination checking via guard condition)

Strict Positivity

An inductive type T must appear only strictly positively in its constructors:

  • T can appear as the final return type
  • T can appear to the right of arrows, but NOT to the left of an arrow in a negative position

Allowed: cons : A -> List A -> List A (List appears positively) Forbidden: bad : (Nat -> Nat) -> Nat is fine, but bad : (T -> Nat) -> T is rejected because T appears negatively (to the left of an arrow leading to T)

Violating strict positivity allows encoding paradoxes (Curry's paradox / non-termination).

Definitional vs Propositional Equality

Definitional equality (judgmental, computational): M =_def N, checked automatically by the type checker via computation (beta-reduction, delta-unfolding, iota-reduction for match).

Propositional equality: Id_A(M, N) or M =_A N, a type that may or may not be inhabited. Requires an explicit proof term (typically refl : Id_A(M, M)).

The gap between definitional and propositional equality is a fundamental tension:

  • More definitional equalities make type checking more convenient but harder to decide
  • Extensional type theory (ETT): Makes propositional equality imply definitional equality (reflection rule). Type checking becomes undecidable.
  • Intensional type theory (ITT): Keeps them separate. Type checking is decidable but proofs require explicit equality reasoning (transport/rewrite).

Decidability and Type Checking

| System | Type Checking | Type Inference | |---|---|---| | CoC | Decidable | Partially decidable (elaboration with unification) | | CIC (Coq) | Decidable | Partial (holes, implicit arguments) | | ETT | Undecidable | Undecidable | | ITT | Decidable | Partial |

Termination checking: CIC requires all recursive functions to be structurally decreasing (or satisfy a more sophisticated termination criterion). This is conservative -- some terminating functions are rejected.

Proof Assistants Based on Dependent Types

| System | Theory | Key Features | |---|---|---| | Coq/Rocq | CIC | Tactics, extraction, universe polymorphism | | Lean 4 | CIC variant | Metaprogramming, type class inference | | Agda | ITT with pattern matching | Cubical mode, sized types | | Idris 2 | Quantitative TT | Linear types, elaboration reflection | | F* | Dependent + effects | SMT integration, refinement types |

Logical Strength

The proof-theoretic strength of these systems varies:

  • STLC: Intuitionistic propositional logic
  • System F: Second-order arithmetic (PA_2)
  • CoC: Higher-order intuitionistic logic
  • CIC + universes: Comparable to ZFC with inaccessible cardinals (depending on the universe structure)

Adding more universe levels increases proof-theoretic strength. Coq with its full universe hierarchy can encode significant portions of mathematics, though it cannot prove its own consistency (by Godel's theorem).