Vect a n = vector of a with known length n
(n ** Vect a n) = vector of a with unknown length n
When I think of it this way it's obvious why filter takes a Vect and returns a pair. Though it seems ugly to have to write each vector function to take both "static" and "dynamic" vectors.
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.
Comments
Am I correct in my understanding of these types?
When I think of it this way it's obvious why filter takes a Vect and returns a pair. Though it seems ugly to have to write each vector function to take both "static" and "dynamic" vectors.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.