[-TUHS, +COFF as per wkt's request]

On Sun, Jun 7, 2020 at 8:26 PM Bram Wyllie <bramwyllie@gmail.com> wrote:
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.