Problem Detail: Can anyone simplify the meaning of families of types index by a type. It looks i get it but quite not understood it. What do you mean by a “family” ? I understand index by a value (n length sequence) then what you mean by index by a type. Any example how you index by a type ? Thanks.
Asked By : Pushpa
Answered By : Andrej Bauer
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$.
Best Answer from StackOverflow
Question Source : http://cs.stackexchange.com/questions/55475 3.2K people like this
