One option is dependent pairs, where one value of the pair (in this example) would be the length of the array and the other value is a type which depends on tha

One option is dependent pairs, where one value of the pair (in this example) would be the length of the array and the other value is a type which depends on that same value (such as Vector n T instead of List T). Type-Driven Development with Idris[1] is a great introduction for dependently typed languages and covers methods such as these if you're interested (and Edwin Brady is a great teacher). [1] https://www.manning.com/books/type-driven-development-with-idris https://www.manning.com/books/type-driven-development-with-i...