Parameterized vs. non-parameterized inductive types

Stream: general

[nrs]

Is the definition for vectors with signature inductive Vect : Type -> Nat -> Type identical to the one given by inductive Vect (A : Type) : Nat -> Type? If so, what is the difference, and can it be stated type-theoretically? Or does the difference exist purely as an artifact of Lean's implementation?

[Kyle Miller]

What comes before the colon is known as a parameter, and what's after is known as an index. The inductive command will try to promote indices to parameters if it's possible, so so long as both work, there should be no difference.

[Kyle Miller]

The difference appears in the type's recursor.

[nrs]

Kyle Miller said:

The difference appears in the type's recursor.

Oh thanks a lot for pointing this out!! I'll be staring at each one's recursor for a while (edit for anyone else interested: you need to turn off auto index promotion)

[nrs]

Kyle Miller said:

What comes before the colon is known as a parameter, and what's after is known as an index. The inductive command will try to promote indices to parameters if it's possible, so so long as both work, there should be no difference.

after two hours of staring at the recursors, I think I understood. if we disable automatic index promotion, would it be correct to say that inductive Vect : Type -> Nat -> Type 1 is equivalent to inductive Vect : Nat -> Type 1? I base this on analyzing the recursors and noticing that there's not much you can do with the first Type other than ignore it, the recursor needs to define a function to eliminate each constructor, but this function takes a Type argument of which we know nothing

[nrs]

consider def vecRecb : Vect α n -> Nat := fun vec => Vect.casesOn vec (fun {α} => n) (fun {α β} t vec2 => n); here {a} stands for the first Type in the above signature

[nrs]

would be nice if someone knew exactly what's the type-theoretical relationship of .casesOn to .recOn, tried using the latter but got that the code elaborator doesn't support it

[nrs]

cf def vecReca : Vect α n -> Nat := fun vec => Vect.rec n (fun a b c => n) vec