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 Dependent ML and 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\}$.

Systems of the lambda cube

First order dependent type theory

The system $\backslash lambda\; \backslash mbox\{P\}$ of pure first order dependent types, corresponding to the logical framework LF, is obtained by generalising the function space type of the simply typed lambda calculus to the dependent product type.

Writing $\backslash mbox\{Vec\}(\{\backslash mathbb\; R\},n)$ for $n$-tuples of real numbers, as above, $\backslash Pi\; n:\{\backslash mathbb\; N\}.\backslash mbox\{Vec\}(\{\backslash mathbb\; R\},n)$ stands for the type of functions which given a natural number n returns a tuple of real numbers of size n. The usual function space arises as a special case when the range type does not actually depend on the input, e.g. $\backslash Pi\; n:\{\backslash mathbb\; N\}.\{\backslash mathbb\; R\}$ is the type of functions from natural numbers to the real numbers, written as $\{\backslash mathbb\; N\}\backslash to\{\backslash mathbb\; R\}$ in the simply typed lambda calculus.

Second order dependent type theory

The system $\backslash lambda\; \backslash mbox\{P2\}$ of second order dependent types is obtained from $\backslash lambda\; \backslash mbox\{P\}$ by allowing quantification over type constructors. In this theory the dependent product operator subsumes both the $\backslash to$ operator of simply typed lambda calculus and the $\backslash forall$ binder of System F.

Higher order dependently typed polymorphic lambda calculus

The higher order system $\backslash lambda\; \backslash mbox\{P\}\backslash omega$ extends $\backslash lambda\; \backslash mbox\{P2\}$ to all four forms of abstraction from the lambda cube: functions from terms to terms, types to types, terms to types and types to terms. The system corresponds to the Calculus of constructions.

Languages with dependent types

• Agda
• Aldor
• ATS
• C++ templates - type parameters can be values
• Cayenne
• Coq
• Dependent ML
• Epigram
• Mizar system
• NuPRL
• PVS
• Sage Programming Language
• Twelf
• Xanadu

See also

• Lambda cube
• Typed lambda calculus
• Intuitionistic type theory

External links

• Why Dependent Types Matter T. Altenkirch, C. McBride, J. McKinna

 This computer science-related article is a stub. You can help Wikipedia by expanding it.

This logic-related article is a stub. You can help Wikipedia by expanding it.

This article is licensed under the GNU Free Documentation License. It uses material from Wikipedia

This article is licensed under the GNU Free Documentation License. It uses material from Wikipedia