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. > > 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. In C, the types depend on the values of expressions evaluated at certain points in time. You could rewrite int len = 1; char buf[len]; as int len = 1; const int hidden_state = len; char buf[hidden_state]; Deputy did this differently. Martin > 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 > > > > >
