4 ms·

When reading this headline, my very first thought was "we wouldn't have this problem if more people used Ada" for that very reason. I don't even think Rust can

by ajdude 3y ago

When reading this headline, my very first thought was "we wouldn't have this problem if more people used Ada" for that very reason. I don't even think Rust can do something like type Element is Integer range 100 .. 1000;

richie_adler 3y ago
Pascal can also do this.
tialaramex 3y ago
That's correct, Rust does not have this, in principle Pattern Types (a possible future Rust feature) could do this, but you probably wouldn't use them for this purpose. WUFFS can do this, it calls such types "refined" types - and indeed WUFFS can also do: assert n_bits < 12 via "a < b: a < c; c <= b"(c: width) What that's saying is "As the programmer I say on this line n_bits is strictly less than 12, and I claim you can prove that based on knowing the value of width, and here's why" WUFFS doesn't know how to create such a proof, it's in quotes because WUFFS has a list of proofs a human gave it, baked in, and just accepts any of those proofs, after all a human mathematician assured it these are true. But it can check the rest of your assertion given this proof, and if that fails your software doesn't compile. WUFFS requires that it can see why everything you're doing is OK, whether that's indexing into an array (if you write dogs[k] where dogs is an array of 16 dogs, WUFFS needs to be certain that k is strictly in the range from zero to fifteen inclusive, or the program won't compile) or arithmetic (if bits is supposed to be an integer between one and thirty two inclusive then we can't very well do bits = k * 2 can we, because k might be zero) As a result WUFFS gets to be entirely safe. As a side effect (and also with the help of some clever SIMD friendly language design choices) WUFFS gets to go very, very fast. And all for the very affordable price of abandoning generality. The next Doom, Excel, Apache and Linux cannot be written in WUFFS. But the question is why your thumbnail making code, or your file compressor is written in anything else.
koito17 3y ago
Depending on what you allow in predicate types, you end up making type inference (and/or type checking) an undecidable problem. In Common Lisp, you can write (deftype element () `(integer 100 1000)) and in this case, a "smart" compiler like SBCL will be able to infer the bounds of (the element x), but for more complex predicates, like (deftype even-element () `(and (integer 100 1000) (satisfies evenp))) I highly doubt there is a single CL compiler out there that'd be able to e.g. optimize (logand 1 (the even-element x)) into the constant 0. Thus declaring types like this -- in Common Lisp at least -- is only really useful for documenting code and run-time validation.
- moonchild 3y ago
  Extant cl compilers are quite primitive. Well known and uncomplicated analyses exist that can cope with this; e.g. in llvm https://godbolt.org/z/nadbG5zGs https://godbolt.org/z/nadbG5zGs

by ajdude 3y ago

richie_adler 3y ago

Pascal can also do this.

tialaramex 3y ago

That's correct, Rust does not have this, in principle Pattern Types (a possible future Rust feature) could do this, but you probably wouldn't use them for this purpose. WUFFS can do this, it calls such types "refined" types - and indeed WUFFS can also do: assert n_bits < 12 via "a < b: a < c; c <= b"(c: width) What that's saying is "As the programmer I say on this line n_bits is strictly less than 12, and I claim you can prove that based on knowing the value of width, and here's why" WUFFS doesn't know how to create such a proof, it's in quotes because WUFFS has a list of proofs a human gave it, baked in, and just accepts any of those proofs, after all a human mathematician assured it these are true. But it can check the rest of your assertion given this proof, and if that fails your software doesn't compile. WUFFS requires that it can see why everything you're doing is OK, whether that's indexing into an array (if you write dogs[k] where dogs is an array of 16 dogs, WUFFS needs to be certain that k is strictly in the range from zero to fifteen inclusive, or the program won't compile) or arithmetic (if bits is supposed to be an integer between one and thirty two inclusive then we can't very well do bits = k * 2 can we, because k might be zero) As a result WUFFS gets to be entirely safe. As a side effect (and also with the help of some clever SIMD friendly language design choices) WUFFS gets to go very, very fast. And all for the very affordable price of abandoning generality. The next Doom, Excel, Apache and Linux cannot be written in WUFFS. But the question is why your thumbnail making code, or your file compressor is written in anything else.

koito17 3y ago

Depending on what you allow in predicate types, you end up making type inference (and/or type checking) an undecidable problem. In Common Lisp, you can write (deftype element () `(integer 100 1000)) and in this case, a "smart" compiler like SBCL will be able to infer the bounds of (the element x), but for more complex predicates, like (deftype even-element () `(and (integer 100 1000) (satisfies evenp))) I highly doubt there is a single CL compiler out there that'd be able to e.g. optimize (logand 1 (the even-element x)) into the constant 0. Thus declaring types like this -- in Common Lisp at least -- is only really useful for documenting code and run-time validation.

moonchild 3y ago
Extant cl compilers are quite primitive. Well known and uncomplicated analyses exist that can cope with this; e.g. in llvm https://godbolt.org/z/nadbG5zGs https://godbolt.org/z/nadbG5zGs