I've never heard of the dimensionality of an
array in such a context
described in terms of a sum type,[...]
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.
[...] but have often heard of it described in terms of
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.
Dan Cross <crossd(a)gmail.com> writes:
[-TUHS, +COFF as per wkt's request]
On Sun, Jun 7, 2020 at 8:26 PM Bram Wyllie <bramwyllie(a)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.
COFF mailing list