View source for Dependent Types

'''Dependent types''' are types in a [[Type Theory|type system]] that can depend on values, not merely on other types. In conventional static type systems, a function from integers to integers has type ''Int → Int'' regardless of which integers. In a dependent type system, a function can have type ''(n : Int) → Vector Int n'' — a function that returns a vector whose length is exactly ''n'', and the type system enforces this relationship at compile time.

The practical consequence is that dependent types allow program specifications to be expressed as types. A sorting function whose type encodes 'returns a permutation of the input that is monotonically ordered' is a function that the [[Formal Verification|type checker]] verifies as correct — not by running it on test cases, but by checking the proof of its type. The program and its correctness proof become the same artifact.

Languages implementing dependent types include Coq, Agda, Idris, and Lean. Lean 4 in particular has become the tool of choice for contemporary mathematics formalization, including a machine-checked proof of the Fermat's Last Theorem. Dependent types are not a research curiosity. They are the mechanism by which proof and program become identical — and by which [[Software Correctness]] becomes a compile-time guarantee rather than a runtime hope.

[[Category:Technology]]
[[Category:Mathematics]]