7 ms·

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.

• ReleaseCandidat 3y ago
  Before const generics, you needed this kind of "types" to use integer values in generics, for example for fixed-length vectors/matrices/... (and const generics still have limitations). https://doc.rust-lang.org/reference/items/generics.html#const-generics https://doc.rust-lang.org/reference/items/generics.html#cons... They came with 1.51: https://blog.rust-lang.org/2021/03/25/Rust-1.51.0.html https://blog.rust-lang.org/2021/03/25/Rust-1.51.0.html
  • hgomersall 3y ago
    You still need them for many cases the current const generics implementation doesn't support.
• bionhoward 3y ago
  Life critical mathematics: you could verify calculations in the type system which are too risky to allow to fail at runtime.
• magicalhippo 3y ago
  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_real.h https://github.com/tmolteno/template-fft/blob/master/fft_rea...
  • ReleaseCandidat 3y ago
    You do that (as nowadays in C++) with compile time "constants" https://doc.rust-lang.org/reference/const_eval.html https://doc.rust-lang.org/reference/const_eval.html
    • magicalhippo 3y ago
      Yes, but then you wouldn't be abusing the type system, so where's the fun in that? :P
• tsnl 3y ago
  Theorem provers that use dependent typing, like Coq.
• Timshel 3y ago
  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.
• sigi64 3y ago
  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 https://aphyr.com/posts/342-typing-the-technical-interview and related to Rust, the solution https://github.com/insou22/typing-the-technical-interview-rust/blob/main/src/main.rs https://github.com/insou22/typing-the-technical-interview-ru... Or Typescript https://www.richard-towers.com/2023/03/11/typescripting-the-technical-interview.html https://www.richard-towers.com/2023/03/11/typescripting-the-...
• SkiFire13 3y ago
  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.
  • ReleaseCandidat 3y ago
    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]`?
    • madsbuch 3y ago
      you implement the function recursively and let the compiler derive a proof by induction.
• turboponyy 3y ago
  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.
• im_down_w_otp 3y ago
  We used methods akin to this back in 2019 for creating low-level HALs for insanely complicated SoCs (think experimental switch fabric controllers). We wanted the compiler to reject any program that was attempting to access the hardware incorrectly because the dev-test cycle was slow, the hardware was very fiddly, and debugging was miserable. The register definitions were all generated from the supplier data sheet (a clojure program we wrote parsed a PDF then emitted Rust). We wrote a blog post about the Rust type-level programming part of the approach: https://blog.auxon.io/2019/10/25/type-level-registers/ https://blog.auxon.io/2019/10/25/type-level-registers/
• wegfawefgawefg 3y ago
  Theres a train company using these to prove the microcontrollers and train network cant be in bad states. check youtube