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!
