Why Vector is defined as a List subtype

Stream: mathlib4

[Aiken Cairncross]

I was looking for a statically sized Array type in the std/mathlib and came upon Vector and was surprised to see it's defined as a subtype of List. Not being all that familiar with Lean, I was expecting it to either be defined inductively (to maybe make some proofs simpler?) or as a subtype of Array (for a generally more performant CPU representation). Is there any advantage to it being defined the way it is?

[Mario Carneiro]

This definition is a bit simpler for proofs than the inductive type, because it means you can prove the theorem about List and lift it to Vector

[Joachim Breitner]

Hopefully eventually we have custom eliminators a.k.a. pattern synonyms and you can freely switch between the two worlds as is most convenient.

[Wrenna Robson]

@Aiken Cairncross for some stuff, people also use tuples, i.e. Fin n -> YourTypeHere, though I'm not sure they have great performance.

[Henrik Böving]

Fin n -> Typ is not a good runtime representation at all and should probably only be used for proof stuff.

[Eric Wieser]

It's pretty reasonable as a way to consume tuples, as it lets you pass Array.get which should be just as efficient as passing an array

[Wrenna Robson]

Henrik Böving said:

Fin n -> Typ is not a good runtime representation at all and should probably only be used for proof stuff.

Would that I had thought about this without writing my thing that currently uses tuples. Though in my defense they are the easiest way to use a permutation on something.

[Wrenna Robson]

Not that I guess permutations are that nice computationally.