In computer science and logic, a dependent type is a type which depends on a value. Dependent types play a central role in Intuitionistic Type Theory and in the design of experimental functional programming languages like DML or Epigram.

An example is the type of $n$-tuples of real numbers, which we may denote as $\backslash mbox\{Vec\}(\{\backslash mathbb\; R\},n)$, this is a dependent type because the type depends on the value $n:\{\backslash mathbb\; N\}$.

Languages with Dependent Types

• Epigram
• Dependent ML
• Xanadu
• ATS
• Cayenne

Type theory