Proof checking
Dependent type
A type that can mention a value.
Definition
Dependent type
A dependent type varies according to a term supplied as an index or parameter.
Dependence can record properties in types, such as vector length or the proposition being proved. The checker must compare these indexed types correctly.
01
Example
Vector α n is the type of vectors containing values of type α with length n.
02
Important distinction
A generic list type does not record its length and is not dependent on a length value.
After reading this article, you should be able to
- Define Dependent type in the sense used on this site.
- Explain what information a dependent vector type records that a list type does not.