I was also puzzled by this remark. Perhaps Bram was thinking of an infinite sum type such as Arrays_0 + Arrays_1 + Arrays_2 + ... where "Arrays_n" is the type of arrays of size n. However, I don't see a way of defining this without dependent (or at least indexed) types. I think that's right, yes. We want the type checker to decide, at compile time, whether a certain operation on arrays, such as scalar product, or multiplication with a matrix, will respect the types. That means providing the information about the size to the type checker: types need to know about values, hence the need for dependent types. Ideally, a lot of the type information can then be erased at run time, so that we don't need the arrays to carry their sizes around. But the distinction between what can and what cannot be erased at run time is muddled in a dependently-typed programming language. Best wishes, Cezar Dan Cross <crossd(a)gmail.com> writes: