Not What You Meant? There are 16 definitions for Dependency.

Dependent type

About 1 pages (404 words)

Know this topic well? Help others and get FREE products!

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 <math>n</math>-tuples of real numbers, which we may denote as <math>\mbox{Vec}({\mathbb R},n)</math>. This is a dependent type because the type depends on the value <math>n:{\mathbb N}</math>.

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

Systems of the lambda cube

First order dependent type theory

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

Second order dependent type theory

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

Higher order dependently typed polymorphic lambda calculus

The higher order system <math>\lambda \mbox{P}\omega</math> extends <math>\lambda \mbox{P2}</math> 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.