I personally balk even against sized vectors. It's too easy to accidentally find yourself writing out long proofs for arithmetic theorems that could easily be verified some other way (e.g. using a SAT solver). Although Idris 2 makes great strides here with zero multiplicity annotations on the vector lengths which makes bailing out a more feasible option.
Instead of
append : Vector n a -> Vector m a -> Vector (n + m) a
I'd prefer just
append : List a -> List a -> List a
and a separate theorem
appendSumsLength : (xs : List a) -> (ys : List a) -> length (append xs ys) = length xs + length ys
Sure it's wordier in the short-term, but I think it pays dividends in longer term maintenance.
To be clear though this is a minority position. Other programmers will argue that putting the size parameter in the data type itself makes a lot of proofs essentially trivial and that at least in the case of sized vectors, the issue of "privileging a single invariant" is less of an issue, because the only defining feature of a polymorphic list is its length. I personally disagree with the merits of this trade-off for most production code, but that's starting to get into the weeds.
Instead of
I'd prefer just and a separate theorem Sure it's wordier in the short-term, but I think it pays dividends in longer term maintenance.To be clear though this is a minority position. Other programmers will argue that putting the size parameter in the data type itself makes a lot of proofs essentially trivial and that at least in the case of sized vectors, the issue of "privileging a single invariant" is less of an issue, because the only defining feature of a polymorphic list is its length. I personally disagree with the merits of this trade-off for most production code, but that's starting to get into the weeds.