4 ms·
FWIW, most (arguably any/all) non-dependently-typed languages would let that slide, as [] is of type "array of (at best) X (which could be inferred as number by
by saurik 6y ago
FWIW, most (arguably any/all) non-dependently-typed languages would let that slide, as [] is of type "array of (at best) X (which could be inferred as number by working backwards from the declaration)" and one of the operations you can do on an array is to index it, by a (maybe unsigned) integer, with 0 (either way) thereby being a valid index. For this to fail, in addition to the type of the array being parameterized by its size (which is at least not too uncommon if not exactly common) the type of that index operator has to be (more notably) at least parameterized by the concrete value 0 if not the abstract expression 0 (which would let you use a proof assistant to verify it for non-constant cases).
- Measter 6y agoWhile not a dependently-typed language, the Rust compiler can do this here for arrays. Arrays in Rust have the length as part of their type, which is compile-time constant, and if you're indexing with another compile-time constant the compiler will check it. So for a line: let number: i32 = [][0]; The compiler knows the array is 0-length, therefore the index is out of bounds, and emits this error: error: this operation will panic at runtime --> src/main.rs:2:23 | 2 | let number: i32 = [][0]; | ^^^^^ index out of bounds: the length is 0 but the index is 0 | = note: `#[deny(unconditional_panic)]` on by default Of course, it's trivial to defeat by converting the array to a slice first, then you get a runtime error. As an aside, am I the only one who got Four Candles'd by that title?