Difference between type parameters and indices?

When you see a family of types, you may wonder whether each of the arguments it has are parameters or indices.

---

Parameters are merely indicative that the type is somewhat generic, and behaves parametrically with regards to the argument supplied.

What this means for instance, is that the type List T will have the same shapes regardless of which T you consider: nil, cons t0 nil, cons t1 (cons t2 nil), etc. The choice of T only affects which values can be plugged for t0, t1, t2.

---

Indices on the other hand may affect which inhabitants you may find in the type! That’s why we say they index a family of types, that is, each index tells you which one of the types (within the family of types) you are looking at (in that sense, a parameter is a degenerate case where all the indices point to the same set of “shapes”).

For instance, the type family Fin n or finite sets of size n contains very different structures depending on your choice of n.

The index 0 indices an empty set.
The index 1 indices a set with one element.

In that sense, the knowledge of the value of the index may carry important information! Usually, you can learn which constructors may or may not have been used by looking at an index. That’s how pattern-matching in dependently-typed languages can eliminate non-feasible patterns, and extract information out of the triggering of a pattern.

---

This is why, when you define inductive families, usually you can define the parameters for the entire type, but you have to specify the indices for each constructor (since you are allowed to specify, for each constructor, what indices it lives at).

For instance I can define:

F (T : Type) : ℕ → Type
C1 : F T 0
C2 : F T 1
C3 : F T 0

Here, T is a parameter, while 0 and 1 are indices. When you receive some x of type F T n, looking at what T is will not reveal anything about x. But looking at n will tell you:

• that x must be C1 or C3 when n is 0
• that x must be C2 when n is 1
• that x must have been forged from a contradiction otherwise

Similarly, if you receive a y of type F T 0, you know that you need only pattern-match against C1 and C3.