[COFF] [TUHS] History of popularity of C

[cezar.ionescu at conted.ox.ac.uk (Cezar Ionescu)]

> 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 a dependent
> type.

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 at gmail.com> writes:

> [-TUHS, +COFF as per wkt's request]
>
> On Sun, Jun 7, 2020 at 8:26 PM Bram Wyllie <bramwyllie at 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
> COFF at minnie.tuhs.org
> https://minnie.tuhs.org/cgi-bin/mailman/listinfo/coff