Consider the example of the dependent type of number sequences of length $n$. It might be defined like this in Coq:
Inductive Sequence : nat -> Type :=
| nil : Sequence O
| cons : forall (n : nat), nat -> Sequence n -> Sequence (S n).
For every n : nat
we have a type Sequence n
. We say that Sequence
is indexed by nat
or that Sequence
depends on nat
. We could also say that Sequence n
depends on the index n
.
In any case, we are just discussing terminology here. The following are equiavalent ways of saying the same thing:
- Type $B$ depends on type $A$
- $B$ is a type family indexed by type $A$
- $B$ is a dependent type indexed by type $A$
- $B : A \to \mathsf{Type}$
- for $x : A$, $B(x)$ is a type
- $x : A \vdash B(x) \ \mathsf{type}$
The reason we use the word family is that in mathematics a collection of sets indexed by a set, $\lbrace A_i \rbrace_{i \in I}$, is called a family of sets. It corresponds to a dependent type $A$ indexed by a type $I$.