In computer science and logic, a dependent type is a type that depends on a value. Dependent types play a central role in intuitionistic type theory and in the design of functional programming languages like ATS, Agda and Epigram.
An example is the type of n-tuples of real numbers. This is a dependent type because the type depends on the value n.
Deciding equality of dependent types in a program may require computations. If arbitrary values are allowed in dependent types, then deciding type equality may involve deciding whether two arbitrary programs produce the same result; hence type checking may become undecidable.
The Curry–Howard correspondence implies that types can be constructed that express arbitrarily complex mathematical properties. If the user can supply a constructive proof that a type is inhabited (i.e., that a value of that type exists) then a compiler can check the proof and convert it into executable computer code that computes the value by carrying out the construction. The proof checking feature makes dependently typed languages closely related to proof assistants. The code-generation aspect provides a powerful approach to formal program verification and proof-carrying code, since the code is derived directly from a mechanically verified mathematical proof.
Read more about Dependent Type: Systems of The Lambda Cube, Comparison
Famous quotes containing the words dependent and/or type:
“For my part, I have no hesitation in saying that although the American woman never leaves her domestic sphere and is in some respects very dependent within it, nowhere does she enjoy a higher station . . . if anyone asks me what I think the chief cause of the extraordinary prosperity and growing power of this nation, I should answer that it is due to the superiority of their woman.”
—Alexis de Tocqueville (1805–1859)
“The real American type can never be a ballet dancer. The legs are too long, the body too supple and the spirit too free for this school of affected grace and toe walking.”
—Isadora Duncan (1878–1927)