From mboxrd@z Thu Jan 1 00:00:00 1970 From: cezar.ionescu at conted.ox.ac.uk (Cezar Ionescu) Date: Mon, 08 Jun 2020 15:46:32 +0200 Subject: [COFF] [TUHS] History of popularity of C In-Reply-To: References: <202006072256.057Muo1h090326@elf.torek.net> Message-ID: <87ftb5hdqf.fsf@virtdeb.speedport.ip> > 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 writes: > [-TUHS, +COFF as per wkt's request] > > On Sun, Jun 7, 2020 at 8:26 PM Bram Wyllie 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