[seanmcdirmid]

If you implement by manipulating the types directly, a few operations with a loop (just for counting lines mind you). Again, I’m not sure how this would be done in Agda, Idris, or COQ, and the system designing is a bit different from other type systems.

But also, any discrete one dimensional problem like wc is going to benefit from a type system with types that resembles regular expressions.