Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

Doing First Grade Math in Rust's Type System

fprasx.github.io

Post reply on HN
Print view View original

21–30 of 43 posts

Re: Doing First Grade Math in Rust's Type System

#21

Post by madsbuch »

ReleaseCandidat wrote: post #19
SkiFire13 wrote: post #17

Earlier quoted context omitted.

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]`?

you implement the function recursively and let the compiler derive a proof by induction.

Re: Doing First Grade Math in Rust's Type System

#22

Post by hgomersall »

ReleaseCandidat wrote: post #5
scns wrote: post #3

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.

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#cons... They came with 1.51: https://blog.rust-lang.org/2021/03/25/Rust-1.51.0.html

You still need them for many cases the current const generics implementation doesn't support.

Re: Doing First Grade Math in Rust's Type System

#28

Post by queuebert »

ReleaseCandidat wrote: post #18
orlp wrote: post #16

Earlier quoted context omitted.

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 ;)

This could be fine, because in science we rarely add dimensionless numbers. Usually they are a scaling factor (i.e. multiplicative).

Re: Doing First Grade Math in Rust's Type System

#30

Post by im_down_w_otp »

scns wrote: post #3

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.

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/

Post reply on HN