[atennapel]

Thank you for your comment, I haven't thought about it from this point of view before. What do you think about simpler datatypes like Vector? This can also be seen as a `List` with the constraint that `Vector n A = (l : List A) * length l = n`.

[dwohnitmok]

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.