4 ms·
I just read up on type arithmetic and I guess this is still whooshing over my head, because I can't see what this changes. I can have a function take two vector
by blotter_paper 8y ago
I just read up on type arithmetic and I guess this is still whooshing over my head, because I can't see what this changes. I can have a function take two vectors of enums and return a new vector with the combined length. I can do operations based on the types of values held by variants in enums, matching only the possible variants. I don't see what can't be done as efficiently with an enum, but I'm very open to being ignorant and clueless.
- chongli 8y agoIf you have a function that returns the first n elements of a vector, how do you make sure there are enough elements? Most languages would either insert a runtime check or throw an exception at runtime. With a dependently typed language, you can do the check statically. This means knowing the provenance of n and the vector itself and doing a compile time proof that n can never exceed the length of the vector.
- blotter_paper 8y agoOkay, I see how that sort of check could be useful. I don't think it's impossible to do without dependant types in principle, but Rust isn't doing it AFAIK, and I see your point.