Dependent type

A dependent type may mention values^[1]. The length of a vector can live in its type, and a function's result type can be computed from its arguments, so that concatenation of a vector of length $m$ and one of length $n$ is declared to return one of length $m+n$. Martin-Löf's intuitionistic type theory of the 1970s is the standard foundation^[1], together with the Calculus of Constructions of Coquand and Huet^[4]. Under the Curry–Howard correspondence, propositions are types and proofs are programs^[5], so a type can state a theorem and a program of that type proves it. Agda^[2], Coq (renamed Rocq in 2025), Lean^[8] and Idris^[7] serve both as programming languages and as proof assistants; Haskell and OCaml approximate parts of the idea with GADTs and type-level programming^[9]. The cost is that type checking involves evaluation, so type equality is decided up to computation and functions must terminate.

module Vec where
 
open import Agda.Builtin.Nat using (Nat; zero; suc; _+_)
open import Agda.Builtin.Equality using (_≡_; refl)
 
-- A list whose length is part of its type.
data Vec (A : Set) : Nat → Set where
  []  : Vec A zero
  _∷_ : {n : Nat} → A → Vec A n → Vec A (suc n)
infixr 5 _∷_
 
-- The result type is computed from the argument types.
append : {A : Set} {m n : Nat} → Vec A m → Vec A n → Vec A (m + n)
append []       ys = ys
append (x ∷ xs) ys = x ∷ append xs ys
 
-- No case for []: a vector of length suc n cannot be empty.
head : {A : Set} {n : Nat} → Vec A (suc n) → A
head (x ∷ _) = x
 
-- Both arguments have the same length, so no case is missing.
zipWith : {A B C : Set} {n : Nat} → (A → B → C) → Vec A n → Vec B n → Vec C n
zipWith f []       []       = []
zipWith f (x ∷ xs) (y ∷ ys) = f x y ∷ zipWith f xs ys
 
-- Tests, checked by evaluation during type checking.
test-append : append (1 ∷ 2 ∷ []) (3 ∷ []) ≡ 1 ∷ 2 ∷ 3 ∷ []
test-append = refl
 
test-zip : zipWith _+_ (1 ∷ 2 ∷ []) (10 ∷ 20 ∷ []) ≡ 11 ∷ 22 ∷ []
test-zip = refl

Vec.agda: no errors

head needs no case for the empty vector, because [] has type Vec A zero and cannot have type Vec A (suc n). The type checker rejects a call on an empty vector:

module HeadEmpty where
open import Vec
open import Agda.Builtin.Nat using (Nat)
 
oops : Nat
oops = head []

HeadEmpty.agda:6,13-15
Nat.zero != (Nat.suc _n_2) of type Nat
when checking that the expression [] has type
Vec _A_1 (Nat.suc _n_2)

Function types generalize to dependent products, written ${\Pi }_{x:A}B(x)$ or $(x:A)\to Bx$, where the result type may refer to the argument. Their rules are those of the simply typed lambda calculus with substitution in the result type^[1]:

When $B$ does not mention $x$, ${\Pi }_{x:A}B$ is the ordinary function type $A\to B$. Dependent sums ${\Sigma }_{x:A}B(x)$ are pairs whose second component's type depends on the first, such as a vector packaged with its length. Types themselves are values of a universe type, Set in Agda, so a function can compute a type.

module Choose where
 
open import Agda.Builtin.Nat using (Nat)
open import Agda.Builtin.Bool using (Bool; true; false)
open import Agda.Builtin.String using (String)
open import Agda.Builtin.Equality using (_≡_; refl)
 
-- A type computed from a value.
Field : Bool → Set
Field true  = Nat
Field false = String
 
-- The result type depends on the argument.
default : (b : Bool) → Field b
default true  = 0
default false = "none"
 
check₁ : default true ≡ 0
check₁ = refl
 
check₂ : default false ≡ "none"
check₂ = refl

Choose.agda: no errors

Since types contain terms, two types can be equal because their terms compute to the same thing: Vec A (1 + 2) and Vec A 3 are the same type. The conversion rule makes this part of typing^[1]:

where $\equiv$ is definitional equality, equality up to evaluation. Deciding it requires evaluating open terms, with free variables, which is why type checkers for these languages contain an evaluator. For the check to terminate, evaluation must terminate: dependently typed languages require functions to be total, checking that recursion is structural or otherwise well founded and that pattern matches cover all cases. A non-terminating function could also prove anything, since loop : False with loop = loop would be a proof of falsehood.

Definitional equality is weaker than provable equality. 0 + n reduces to n because addition recurses on its first argument, but n + 0 does not reduce when n is a variable, so the type checker cannot see that it equals n and a proof is needed.

module BadProof where
 
open import Agda.Builtin.Nat using (Nat; zero; suc; _+_)
open import Agda.Builtin.Equality using (_≡_; refl)
 
-- n + zero does not reduce: _+_ recurses on its first argument.
+-zero : (n : Nat) → n + zero ≡ n
+-zero n = refl

BadProof.agda:8,12-16
n + zero != n of type Nat
when checking that the expression refl has type n + zero ≡ n

Under the Curry–Howard correspondence, a universally quantified proposition is a Π type and its proof is a function; an existential is a Σ type; and equality is the identity type $a\equiv b$, with one constructor refl : a ≡ a^[5][1]. A proof by induction is a recursive function, each case of which is checked by evaluation.

module Proofs where
 
open import Agda.Builtin.Nat using (Nat; zero; suc; _+_)
open import Agda.Builtin.Equality using (_≡_; refl)
 
cong : {A B : Set} {x y : A} (f : A → B) → x ≡ y → f x ≡ f y
cong f refl = refl
 
-- A proof is a program: induction is recursion, and each case is checked
-- by evaluating both sides.
+-assoc : (a b c : Nat) → (a + b) + c ≡ a + (b + c)
+-assoc zero    b c = refl
+-assoc (suc a) b c = cong suc (+-assoc a b c)
 
+-zero : (n : Nat) → n + zero ≡ n
+-zero zero    = refl
+-zero (suc n) = cong suc (+-zero n)

Proofs.agda: no errors

Proof assistants built on this idea have verified an optimizing C compiler, CompCert, in Coq^[10], and the four-colour theorem^[11], and Lean's mathematics library formalizes a large body of undergraduate and research mathematics^[8].

Barendregt organized typed lambda calculi by which kinds of abstraction they allow^[3]. The simply typed lambda calculus has only terms depending on terms. Adding terms that depend on types gives polymorphism, System F; adding types that depend on types gives type operators; together they give System Fω^[13], the basis of Haskell's core language. Adding types that depend on terms gives dependent types, λP, the logical framework LF. The Calculus of Constructions, λC, has all three^[4]; Coq and Lean are based on extensions of it with inductive types and a hierarchy of universes, needed because a type of all types leads to an inconsistency, Girard's paradox.

Languages without dependent types approximate them. In Haskell, DataKinds promotes data constructors to the type level, GADTs let constructors refine an index, and type families compute with types^[9]. Values and types remain separate, so a run-time value that should determine a type must be mirrored by a singleton, a value whose type exactly reflects it.

{-# LANGUAGE DataKinds, GADTs, KindSignatures, TypeFamilies #-}
import Data.Kind (Type)
 
data Nat = Z | S Nat
 
-- The length index lives at the type level, as a promoted Nat.
data Vec (n :: Nat) (a :: Type) where
  Nil  :: Vec 'Z a
  Cons :: a -> Vec n a -> Vec ('S n) a
 
type family (m :: Nat) + (n :: Nat) :: Nat where
  'Z + n = n
  'S m + n = 'S (m + n)
 
append :: Vec m a -> Vec n a -> Vec (m + n) a
append Nil ys = ys
append (Cons x xs) ys = Cons x (append xs ys)
 
vhead :: Vec ('S n) a -> a
vhead (Cons x _) = x
 
-- A type cannot mention a run-time Int, so replicate takes a singleton:
-- a value whose type mirrors it exactly.
data SNat (n :: Nat) where
  SZ :: SNat 'Z
  SS :: SNat n -> SNat ('S n)
 
vreplicate :: SNat n -> a -> Vec n a
vreplicate SZ _ = Nil
vreplicate (SS n) x = Cons x (vreplicate n x)
 
toList :: Vec n a -> [a]
toList Nil = []
toList (Cons x xs) = x : toList xs
 
main :: IO ()
main = do
  let v = append (Cons 1 (Cons 2 Nil)) (vreplicate (SS (SS SZ)) (0 :: Int))
  print (toList v, vhead v)

([1,2,0,0],1)

OCaml's GADTs support the same length-indexed vectors, with lengths encoded as types. Neither language checks that type-level functions terminate or that the resulting logic is consistent, so the types document and enforce invariants but are not proofs in the sense of a proof assistant.

De Bruijn's AUTOMATH, begun in 1967, was the first system to check mathematical proofs with dependent types^[6]. Howard described the correspondence between proofs and programs in 1969^[5], and Martin-Löf developed intuitionistic type theory from 1971, giving Π and Σ types and identity types their standard form^[1]. Coquand and Huet introduced the Calculus of Constructions in 1985, and the Coq proof assistant was built on it from 1989^[4]. Barendregt's lambda cube of 1991 classified the systems^[3]. Epigram, by McBride and McKinna, explored dependently typed programming with pattern matching^[12], and Norell's Agda 2 of 2007 made it practical^[2]. Idris in 2013 aimed at general-purpose programming^[7], and Lean 4 in 2021 at both programming and mathematics^[8].

• Refinement typeA refinement type is a base type paired with a logical predicate that its values must satisfy, such as {v : Int | v > 0}, the positive integers. Type checking generates verification conditions, implications between predicates, and discharges them with an SMT solver, so a program can be checked against preconditions, postconditions and invariants without the programmer writing proof terms. The predicates are restricted to a decidable logic, typically linear arithmetic with uninterpreted functions, which is what keeps checking automatic. LiquidHaskell, F* and Liquid Types are the best-known systems.
• GADTA generalized algebraic data type (GADT) is an algebraic data type whose constructors may each give a more specific result type than the declared one, instead of all sharing one polymorphic return type. Matching on a constructor then tells the type checker what the type parameter was, so a single well-typed eval can return an int for an Add node and a bool for an Eq node, checked at compile time rather than by a run-time tag test. GADTs express typed syntax trees, type representations and equality proofs, typed format strings and length-indexed data. The price is that type inference needs annotations.
• Phantom typeA phantom type is a type parameter that appears in a type's declaration but in none of its fields, used to keep otherwise identical representations apart: lengths in metres and in feet, validated and unvalidated strings, read-only and writable handles, SQL expressions of different result types. It carries no data and costs nothing at run time. Combined with an abstract type whose constructors are hidden, it lets a library enforce invariants through the type checker. Unlike a GADT index it tells a pattern match nothing; it constrains what callers may do, not what the compiler can learn.
• Higher-kinded typeA higher-kinded type is a type constructor, such as Maybe or List, that takes types as arguments, and higher-kinded polymorphism is the ability to abstract over such constructors with type variables, so that Functor f can be instantiated at Maybe or at lists without naming their element types. Kinds classify types the way types classify values: Int has kind Type, Maybe has kind Type → Type. Higher-kinded variables are what make a single Functor or Monad class usable across every container. Haskell and Scala support them directly; OCaml expresses the same abstraction with module functors or an encoding, and Java and Go cannot express it.
• Church–Rosser theoremThe Church–Rosser theorem states that β-reduction in the λ-calculus is confluent: if a term reduces to two different terms, both can be reduced further to a common term. It follows that a term has at most one normal form, so the order in which redexes are reduced cannot change the result of a terminating computation, and that the λ-calculus is consistent, since two different normal forms are never equal. Church and Rosser proved it in 1936. The standard modern proof, due to Tait and Martin-Löf, uses parallel reduction, which has the diamond property that single-step reduction lacks. Confluence is the central property of rewriting systems in general.

1. [1]P. Martin-Löf, Intuitionistic Type Theory, Bibliopolis (1984).
2. [2]U. Norell, Towards a Practical Programming Language Based on Dependent Type Theory, PhD thesis, Chalmers (2007).
3. [3]H. Barendregt, “Introduction to generalized type systems”, Journal of Functional Programming 1 (1991).
4. [4]T. Coquand, G. Huet, “The calculus of constructions”, Information and Computation 76 (1988).
5. [5]W. A. Howard, “The formulae-as-types notion of construction”, in To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, Academic Press (1980).
6. [6]N. G. de Bruijn, “The mathematical language AUTOMATH, its usage, and some of its extensions”, Symposium on Automatic Demonstration, Lecture Notes in Mathematics 125, Springer (1970).
7. [7]E. Brady, “Idris, a general-purpose dependently typed programming language: design and implementation”, Journal of Functional Programming 23 (2013).
8. [8]L. de Moura, S. Ullrich, “The Lean 4 theorem prover and programming language”, CADE (2021).
9. [9]R. A. Eisenberg, Dependent Types in Haskell: Theory and Practice, PhD thesis, University of Pennsylvania (2016).
10. [10]X. Leroy, “Formal verification of a realistic compiler”, Communications of the ACM 52 (2009).
11. [11]G. Gonthier, “Formal proof—the four-color theorem”, Notices of the AMS 55 (2008).
12. [12]C. McBride, J. McKinna, “The view from the left”, Journal of Functional Programming 14 (2004).
13. [13]J.-Y. Girard, Interprétation fonctionnelle et élimination des coupures de l’arithmétique d’ordre supérieur, thèse d’État, Université Paris 7 (1972).

last updated 29 September 2026