4 ms·
I think the fix is dependent types, right? If the compiler can reason about the index and the size of the vector, that's one way. For example; let x = 5; let
by staticassertion 6y ago
I think the fix is dependent types, right? If the compiler can reason about the index and the size of the vector, that's one way.
For example;
let x = 5;
let y = vec![0; y * 2];
for i in 0..x * 3 {
y[x]
}
That shouldn't compile.
- Kinrany 6y agoTypo: should be `[0; x * 2]`
- staticassertion 6y agoYeah, I caught it too late to edit :\
- zelly 6y agoDependent typing can make guarantees like that if there are no loops, no parallel mutation, no I/O, no cosmic rays. For example if I made y have rand() elements then there's nothing a compiler can ever do about that. In other cases the compiler can check types by executing code (not always decidable). Dependently typed languages are not Turing complete. They can help with proofs and such but it's physically impossible to use dependent types for general purpose programming (e.g. try writing Linux in Idris, you can't).
- sfvisser 6y agoDependent types strictly just means being able to parametrize types with values. You can design many different types of PLs with this feature. You don’t need strict reasoning for it to be useful like any other type level feature.
- anchpop 6y agoDependent types are cool, but I think the best fix would be refinement types. They are sort of similar, except refinement types use a SAT solver to prove correctness, while dependent types require to prove everything yourself (to the point where realistically something like what you posted probably wouldn't compile in most dependently typed languages). Refinement types also compose better. Because of the SAT solver you have some restrictions on what you can prove, but they're so much more ergonomic I think it's more than worth it.
- staticassertion 6y agoSure, agreed that refinements are likely the better approach here.