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:
“In looking back over the college careers of those who for various reasons have been prominent in undergraduate life ... one cannot help noticing that these men have nearly always shown from the start an interest in the lives of their fellow students. A large acquaintance means that many persons are dependent on a man and conversely that he himself is dependent on many. Success necessarily means larger responsibilities, and responsibilities mean many friends.”
—Franklin D. Roosevelt (1882–1945)
“The type of fig leaf which each culture employs to cover its social taboos offers a twofold description of its morality. It reveals that certain unacknowledged behavior exists and it suggests the form that such behavior takes.”
—Freda Adler (b. 1934)