Dependent type

From Wikipedia, the free encyclopedia

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 $\mbox{Vec}({\mathbb R},n)$ . This is a dependent type because the type depends on the value $n:{\mathbb N}$ .

1 Systems of the lambda cube
2 Languages with dependent types
3 See also
4 External links

[edit] Systems of the lambda cube

[edit] First order dependent type theory

The system $λ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}\to{\mathbb R}$ in the simply typed lambda calculus.

[edit] Second order dependent type theory

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

[edit] Higher order dependently typed polymorphic lambda calculus

The higher order system $λPω$ extends $λ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.