Am Freitag, dem 14.03.2025 um 14:42 -0400 schrieb John McCall: > 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. Yes, I guess this is all true. But let's rephrase my point a bit more precisely: One could take a strict subset of C that includes variably modified types but obviously has to forbid a lot other things (e.g. arbitrary pointer conversions or unsafe down-casts and much more) and make this a memory-safe language with dependent types. This would also require adding run-time checks at certain places where there is now UB, in particular where two VLA types need to be compatible. Martin > > John.
