[tj800x]

Somewhat related: I'm surprised we don't see NonZero numbers (NzInts, NzNats, and NzReals, etc). This would seem to avoid a lot of division by zero problems at the type level. I realize this might "back up" checking for zeros into the origin of denominator values, but that seems like it would be an improvement to me.

[itishappy]

In the same vein, having a dedicated type for natural (or even Peano) numbers can be quite nice. I've seen some clever use-cases in Haskell and Rust such as statically enforcing bounds checks. Can't have a negative length list!