4 ms·
Is there anything you could do with dependant types that you can't do with a number of types wrapped in an enum? A dependently typed variable should have the sa
by blotter_paper 8y ago
Is there anything you could do with dependant types that you can't do with a number of types wrapped in an enum? A dependently typed variable should have the same memory footprint of an enum, right? Do you just want a different syntax, or am I missing something?
- chongli 8y agoWith dependent types you can perform arithmetic at the type level. This lets you have functions that, e.g., take an array of length n and an array of length m and return an array of length n + m. Ideally, this would let you write programs that are provably correct with no runtime bounds checking.
- blotter_paper 8y agoI 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.