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:
“It is possible to make friends with our children—but probably not while they are children.... Friendship is a relationship of mutual dependence-interdependence. A family is a relationship in which some of the participants are dependent on others. It is the job of parents to provide for their children. It is not appropriate for adults to enter into parenthood recognizing they have made a decision to accept dependents and then try to pretend that their children are not dependent on them.”
—Donald C. Medeiros (20th century)
“But the mother’s yearning, that completest type of the life in another life which is the essence of real human love, feels the presence of the cherished child even in the debased, degraded man.”
—George Eliot [Mary Ann (or Marian)