[algas]

Interesting article! Given that subtraction isn't closed on the natural numbers, I wonder if it would be possible to implement subtraction as operations on a new type (Integer, Z):

     Z = N x N (Cartesian product or sum type)
     for p, q in Z: p=q if p.first + q.second = q.first + p.second
     p + q := (p.first + q.first, p.second + q.second)
     p - q := (p.first + q.second, p.second + q.first)

Rational numbers can similarly be defined by new operations and equivalence relations on the product set Z x Z. I don't know enough Rust to say whether it's feasible to implement this in the type system, but I'd be curious to hear from someone more experienced!

[Brananarchy]

https://docs.rs/typenum/latest/typenum defines a "reasonable" implementation of integer arithmetic including addition, subtraction, multiplication, and division (and abs, and remainder, and a bunch of other "standard" integer ops).

I think that building rationals on top of it would be pretty easy, though not necessarily performant.