Hi Martin, The C design of VLAs misunderstood dependent typing.
For a program to be validly typed when there are dependent types, you need to be able to write down the types of any values and variables at program points where they are in use. This is problematic when there are assignments to variables involved in dependent types. The values that the dependent types used are “gone”, so the program is no longer validly typed using the source-level types. The Deputy system handled this by introducing temporary variables to hold values used in dependent types. For C, that corresponds to introducing hidden state, which is not done anywhere else in the language. It also doesn’t work when you have global variables involved in dependent types, as you potentially need an unlimited number of copies. In your example: > int len = 1; > char buf[len]; // len is evaluated and the array has size 10 > len = 10; // has no impact on the type of 'buf' What is the dependent type of buf after you’ve assigned to len? The compiler can introduce a temporary, but the type is “gone” at the source level. Claiming that buf has the type of “array of length len” is not correct: > int len = 1; > char buf[len]; // len is evaluated and the array has size 10 > len = 10; // has no impact on the type of ‘buf’. *** The dependent type of > buf in the source code (char [len]) is now wrong.*** There’s a misunderstanding of how type systems work. There’s the static typing of a program - what is declared in the source code and “type checked” at compile time. Then there is soundness: ensure that the program respects the types at runtime. A proof of soundness takes the static type checking rules and combines them with the runtime semantics and shows that programs “never go wrong”, i.e. access values at the wrong type. To have soundness, Deputy had to take the C source level programs and translate them to dependently-typed programs with extra state and extra runtime checks. It’s a perfectly valid approach, but then one needs to understand that the source-level types no longer correspond to the dependent types used in type checking. Deputy specifically restricted the dependent types of values stored on the heap: a value with a dependent type had to be stored in a member and the dependent type was specified in terms of other members in the same object. As for the rules around scoping, we only need to rules that differ because the original design was flawed and missed common use cases. David > On Mar 13, 2025, at 11:16 PM, Martin Uecker <uec...@tugraz.at> wrote: > > > Hi David, > > Am Donnerstag, dem 13.03.2025 um 19:23 -0700 schrieb David Tarditi: >> >> I skip your initiial part. I think this was all discussed before > > (also in WG14) and I still come to different conclusions. Just > two comments: > > ... >> >> The VLA semantics are also problematic. User can side-effect >> variables used in a VLA declaration after the declaration, while >> the declaration is in scope. It is not obvious how to implement >> bounds checking, because the bounds could be gone (invalid). >> It is a design flaw that the declared bounds can become invalid >> while the declaration is in scope. > > Variably modified types do not work like this C. The size > expression is evaluated at the point of declaration. If there > is a variable in it, it is never accessed later and changing it > does not affect the type anymore. > > int len = 1; > char buf[len]; // len is evaluated and the array has size 10 > len = 10; // has no impact on the type of 'buf' > > In fact, one can also have more complicated expressions. > > int len = 11; > char buf[len + 1]; // has size 11. > > and those are also not re-evaluated later. > > > This is exactly how it works in other dependently types languages, > so I do not think one can make the case that C got these semantics > wrong. > > Bounds checking also works already today: https://godbolt.org/z/5P8so1reb > > (although there are still missing pieces which would be important > but which compilers currently do not implement. But for GCC I have > a local branch which adds most of those.) > > >> >> Finally, when you get to nested pointers, the syntax (and typing) >> for VLAs becomes confusing. This isn’t VLAs fault. It is there in the >> original C design. > > Your comments about C's syntax certainly have some truth to them, > but I personally - as a C programmer and teacher - would find > it much worse to add new inconsistent rules to the language > just to be able to write something in a more succinct way > in some specific cases. A programmer would still have to > learn and nderstand the general C syntax and all the existing > rules name lookup rules. > > I do not think adding new inconsistent rules would make the > language simpler and clearer in general, even it it may look > like this when only considering a narrow use case. > > > Martin > >
