How to define a polymorphic `Vector` type in Lean 4 as a `Subtype` of `List`?

Question

The List type in Lean 4's prelude has a lot of nice goodies implemented, e.g. List.map, List.join, etc.

A classic example in dependently-typed languages is Vector a n where a is the type of the elements of the container, and n is the length. This allows you to do nice things like write a function concat (u : Vector a m) (v : Vector a n) : Vector a (m + n) whose type signature guarantees that the function returns a vector of the expected length.

Following a comment on a previous answer I'd like to write a Vector type as a Subtype of List, as a first step towards getting these methods for a sized container. But I'm new to Lean, and I don't exactly understand how this works. Subtype takes a predicate a -> Prop, which appears to work a bit like a filter on the parent type, which in this case is a := List. But all lists are valid vectors, so it doesn't seem like this is much use. The predicate should always return true, no?

My question is:

How can I use Subtype to get a subtype of List whose length is encoded in its type? And as a follow-up, how can I construct an element of this type from an existing List?

Answer 1

You're right that all lists are valid vectors, but the predicate is exactly how to specify that the Vector has a certain number of elements.

def Vec (n : Nat) (a : Type) := { ls : List a // ls.length = n }

def myVec : Vec 3 Nat := ⟨[1, 2, 3], rfl⟩