On 14 Mar 2025, at 14:13, Martin Uecker wrote: > Am Freitag, dem 14.03.2025 um 10:11 -0700 schrieb David Tarditi: >> Hi Martin, >> >> The C design of VLAs misunderstood dependent typing. > > They probably did not care about theory, but the design is > not inconsistent with theory.
This is almost true, but for bad reasons. The theory of dependent types is heavily concerned with deciding whether two types are the same, and C simply sidesteps this question because type identity is largely meaningless in C. Every value of variably-modified type is (or decays to) a pointer, and all pointers in C freely convert to one another (within the object/function categories). _Generic is based on type compatibility, not equality. So in that sense, the standard doesn’t say anything inconsistent with theory because it doesn’t even try to say anything. The reason it is not quite true is that C does have rules for compatible and composite types, and alas, those rules for variably-modified types are not consistent with theory. Two VLA types of compatible element type are always statically considered compatible, and it’s simply UB if the sizes aren’t the same. The composite type of a VLA and a fixed-size array type is always the fixed-size array type. The standard is literally incomplete about the composite type of two VLAs; if you use a ternary operator where both operands are casts to VLA types, the standard just says it’s straight-up just undefined behavior (because one of the types has a bound that’s unevaluated) and doesn’t even bother telling us what the static type is supposed to be. John.
