DEPENDENT TYPE

(Redirected from Dependent types)
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 or Epigram.
An example is the type of $n$-tuples of real numbers, which we may denote as $mbox\{Vec\}(\{mathbb\; R\},n)$. This is a dependent type because the type ''depends'' on the value $n:\{mathbb\; N\}$.

Contents

Systems of the lambda cube

Pure first order dependent types

Languages with dependent types

See also

External links

Systems of the lambda cube

Pure first order dependent types

The system $lambda\; 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 $mbox\{Vec\}(\{mathbb\; R\},n)$ for $n$-tuples of real numbers, as above, $Pi\; n:\{mathbb\; N\}.mbox\{Vec\}(\{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. $Pi\; n:\{mathbb\; N\}.\{mathbb\; R\}$ is the type of functions from natural numbers to the real numbers, written as $\{mathbb\; N\}\; o\{mathbb\; R\}$ in the simply typed lambda calculus.

Languages with dependent types

★ Aldor

★ ATS

★ Cayenne

★ Coq

★ Dependent ML

★ Epigram

★ Mizar system

★ 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