Inductive families confusion

Stream: new members

[Andrea Delmastro]

Hello, I'm trying to figure out how inductive definitions work in Lean, but I think my question may be about a more general theoretical confusion about them.
In TPL, chapter 7, section 7, inductive families are introduced. What i can't figure out is the difference with a simpler inductive definition. For example

inductive vector (α : Type u) : nat → Type u
| nil {}                              : vector zero
| cons {n : ℕ} (a : α) (v : vector n) : vector (succ n)

Why isn't alpha considered an index? Why the definition is not something like

inductive vector :  Type u  → nat →  Type u?

The same is valid for lists,

inductive list (α : Type*)
| nil {} : list
| cons : α → list → list

why the type α of the list is not part of the indexes? Aren't we declaring a family of inductive types ranging on α?

[Jakub Kądziołka]

here, for each \a you have a separate inductive type. indices may change within the recursion

[Jannis Limperg]

Indices indeed generalise parameters, so you could only use indices when defining your inductive types. An inductive type with parameters is isomorphic -- and therefore morally equal -- to the same inductive type with indices. However, indices give a less convenient recursor and I believe tactics which wrap the recursor, particularly induction, may work less well. So it's a good idea to use parameters where possible.

[Andrea Delmastro]

So it's a good idea to use parameters where possible

So, accordingly with what @Jakub Kądziołka said, it would be a good practice to use a parameter every time I do not need to change the index in recursion?

[Jannis Limperg]

Yes, exactly.