From mboxrd@z Thu Jan 1 00:00:00 1970 From: crossd at gmail.com (Dan Cross) Date: Mon, 8 Jun 2020 08:47:03 -0400 Subject: [COFF] [TUHS] History of popularity of C In-Reply-To: References: <202006072256.057Muo1h090326@elf.torek.net> Message-ID: [-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. -------------- next part -------------- An HTML attachment was scrubbed... URL: