[dwohnitmok]

For the sake of discussion I'm going to say something stronger than I believe, but which I don't think gets enough airtime so I want to expose its most extreme version. Having sufficient type direction such that there is only one possible implementation of a function is a bad thing. It represents a tightly constrained data type that will be painful to make even the smallest changes to down the road and duplicates code for no real benefit.

The definition of `RuntimeLength` does not do away with the need to define `uncompress`, all it does is move it into the definition of `RuntimeLength`. In fact my version of `RuntimeEncodedList` and `uncompress` is less overall code than `RuntimeLength` and `uncompress`. Indeed the only reason the compiler can synthesize `uncompress` is because it duplicates `RuntimeLength`! So really the compiler hasn't reduced the amount of work that needs to be done. Just like I could've messed up my definition of `uncompress`, its equivalent in `RuntimeLength` could also have been written incorrectly. We haven't reduced the amount of code that needs to be checked by a human for correctness (in the absence of other invariants), only moved it from a function definition to a data type definition.

By moving it into a function, however, we can then selectively add as many additional properties as we want (such as the `uncompress(compress xs) == xs` invariant), without having to worry about privileging one over any other.

[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.