2 ms·

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 s

• dwohnitmok 5y ago
  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.