That's right.

You don't normally need to write each vector function both ways. If you can statically know the length (which you normally do in practice, at least in my experience) then you can write down a more precise type. filter serves as an example of what you might do when you need to compute an index dynamically.