A dependent type is a type that can depend on a value. This lets the type system express relationships that ordinary parameterized types cannot.

For example, a vector type can record its length:

$$\operatorname{Vec}(A,n).$$

Then a safe indexing operation can require a proof that the index is in range, and vector concatenation can state its result length in the type:

$$\operatorname{append}:\operatorname{Vec}(A,m)\to\operatorname{Vec}(A,n)\to\operatorname{Vec}(A,m+n).$$

The two central dependent type constructors generalize functions and products.

A dependent function type

$$\Pi(x:A).,B(x)$$

allows the return type to depend on the argument. A dependent pair type

$$\Sigma(x:A).,B(x)$$

packages a value $x$ together with evidence or data whose type depends on $x$.

Under Curry-Howard, propositions can themselves be represented as types. A function accepting a proof that $n>0$ can therefore require that fact statically rather than checking it only at runtime.

Dependent types make specifications dramatically more expressive, but type checking becomes intertwined with reasoning about values and computation. Practical systems must carefully control which computations are allowed during type checking so that checking remains meaningful and tractable.