Dependent type
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 DML 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>.
Languages with Dependent Types
- Epigram
- Dependent ML
- Xanadu
- ATS
- Cayenne
External Links
Categories
Type theory