Dependent types aren't needed for sum types though, which is what you'd normally use for an array that carries its size, correct?
No, I don't think so. I've never heard of the dimensionality of an array in such a context described in terms of a sum type, but have often heard of it described in terms of a dependent type. However, I'm no type theorist.
- Dan C.