Dependent Type

A dependent type is a type whose definition depends on a value. In contrast to simply-typed systems where 'List A' describes lists of elements of type A regardless of their length, a dependent type 'Vec A n' describes lists of length n, where n is a term that appears in the type itself. This fusion of terms and types makes dependent type theory simultaneously a programming language and a logic: programs are proofs, and types are propositions, as the Curry-Howard correspondence demands.

Dependent types transform the compiler from a mere syntax checker into a theorem prover. When a function claims to return a vector of length n + m, the compiler verifies that the returned expression indeed has that length. The specification is the proof, and the program cannot be built unless the proof is correct. Languages such as Agda, Coq, and Lean use dependent types to write programs that are correct by construction, though the cost is that type checking becomes undecidable in general and may require user guidance.

The concept originates in Per Martin-Löf's intuitionistic type theory, which sought to replace the set-theoretic foundations of mathematics with a constructive framework in which every proof carries computational content. Dependent types are the mechanism that makes this replacement possible, and they are the reason that modern proof assistants can extract executable programs from formal proofs.