4
$\begingroup$

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.

Improve this question
$\endgroup$

1 Answer 1

Reset to default
6
$\begingroup$

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$.

Improve this answer
$\endgroup$
2
  • 4
    $\begingroup$ Some more terminology, for what it's worth. There is also a distinction between parameterized and indexed families of types. An excerpt from the Agda reference manual: The difference between an index and a parameter is that the index need not be constant throughout the definition of the type. The linked article has some examples illustrating the statement. $\endgroup$
    – Anton Trunov
    Apr 5, 2016 at 8:21
  • 3
    $\begingroup$ @AntonTrunov: it is worth pointing out that the index/parameter terminology applies specifically to inductive datatypes, not to general types. In terms of fixed points, it is the difference between defining a family of types $B : A \to \mathsf{Type}$ as $\mu B : \mathsf{Type} . \lambda x : A . \cdots$ or $\lambda x : A . \mu B : \mathsf{Type} . \cdots$ $\endgroup$
    – Andrej Bauer
    Apr 5, 2016 at 9:06

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Not the answer you're looking for? Browse other questions tagged or ask your own question.