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!
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):
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!