Can someone give an example of a useful application of this technique? Honest question, if it is just for fun that is fine with me.
Theorem provers that use dependent typing, like Coq.
Doing First Grade Math in Rust's Type System
11–20 of 43 posts
Re: Doing First Grade Math in Rust's Type System
#12Can someone give an example of a useful application of this technique? Honest question, if it is just for fun that is fine with me.
Something like a typed heterogeneous list is often build in a similar way.
A simpler version is probably a simple non empty list where you always have the guaranty of at least one element.
Re: Doing First Grade Math in Rust's Type System
#13[deleted]
Re: Doing First Grade Math in Rust's Type System
#14Earlier quoted context omitted.
While not nearly as involved, I've seen similar-ish techniques used for FFTs and similar algorithms, in order to precompute constants. Here[1] is an example in C++ but given the article it seems you could do something similar in Rust. [1]: https://github.com/tmolteno/template-fft/blob/master/fft_rea...
You do that (as nowadays in C++) with compile time "constants" https://doc.rust-lang.org/reference/const_eval.html
Yes, but then you wouldn't be abusing the type system, so where's the fun in that? :P
Re: Doing First Grade Math in Rust's Type System
#15Can someone give an example of a useful application of this technique? Honest question, if it is just for fun that is fine with me.
This technique is good for job interviews, when they ask me to solve leetcode problems. I was inspired by the blog:
https://aphyr.com/posts/342-typing-the-technical-interview
and related to Rust, the solution
https://github.com/insou22/typing-the-technical-interview-ru...
Or Typescript https://www.richard-towers.com/2023/03/11/typescripting-the-...
Re: Doing First Grade Math in Rust's Type System
#16"is much faster and the one you should probably use in practice" Where is this useful in practice? Exercises maybe. Like doing planks for example. I have never needed to plank "in practice" other than to exercise.
One practical use case is for dimensional analysis. A type is then a k-tuple of type-level integers where k is the number of primitive units, e.g. (kg, m, s). Then m^2 / kg would be the tuple (-1, 2, 0). Multiplying two quantities adds the tuples elementwise. For example multiplying the above type by a quantity of type kg / m / s (corresponding to (1, -1, -1)) would give (0, 1 -1), which is the correct m / s.
Addition would only be allowed if the types are equal.
Re: Doing First Grade Math in Rust's Type System
#17Can someone give an example of a useful application of this technique? Honest question, if it is just for fun that is fine with me.
As others mentioned, nowadays const generics replace this technique for most problems. This technique however is still useful if you need something like `[T; A+B]` (an array whose length is the sum of two generic constants), which is not yet possible with const generics.
Re: Doing First Grade Math in Rust's Type System
#18"is much faster and the one you should probably use in practice" Where is this useful in practice? Exercises maybe. Like doing planks for example. I have never needed to plank "in practice" other than to exercise.
One practical use case is for dimensional analysis. A type is then a k-tuple of type-level integers where k is the number of primitive units, e.g. (kg, m, s). Then m^2 / kg would be the tuple (-1, 2, 0). Multiplying two quantities adds the tuples elementwise. For example multiplying the above type by a quantity of type kg / m / s (corresponding to (1, -1, -1)) would give (0, 1 -1), which is the correct m / s. Additio…
This doesn't work with dimensionless numbers, as they would need to have e.g. the type `(0, 0, 0)` for multiplication but `(-1, 2, 0)` or `(0, 1 -1)` for addition.
Edit: I've just realised that that's actually correct ;)
Re: Doing First Grade Math in Rust's Type System
#19Can someone give an example of a useful application of this technique? Honest question, if it is just for fun that is fine with me.
As others mentioned, nowadays const generics replace this technique for most problems. This technique however is still useful if you need something like `[T; A+B]` (an array whose length is the sum of two generic constants), which is not yet possible with const generics.
How do you prove to the type-checker that e.g. `append(v: [T, N], w: [T, M]) -> [T, N + M]`?
Or, to make it easier, that just `append(v: [T, N], x: T]) -> [T, N + 1]`?
Re: Doing First Grade Math in Rust's Type System
#20Can someone give an example of a useful application of this technique? Honest question, if it is just for fun that is fine with me.
Not really in the programming mainstream, but in research-oriented languages with dependent typing like Lean or Idris, constraining your "implementation search space" with types and leveraging the type system to prove properties about your program is commonplace.