This what is being discussed in the thread, dependent types imply generic value parameters, but provide a complete story of what you can do with those value parameters. As soon as you introduce value parameters, it would make sense to have functions that are evaluated on those values at compile-time. As in this example, if you encode collection's length in its type, you'll also want a type-level + function that guarantees that concatenation of multiple collections produces a type that encodes the sum of their lengths.
2 Likes