> It seems there is a fundamental difference: zero-ness is a value property while number-ness is a type property. That makes the latter trivial to check at comp

> It seems there is a fundamental difference: zero-ness is a value property while number-ness is a type property. That makes the latter trivial to check at compile time. That's because you have defined division to have two number inputs. Nothing stops you from defining it having a number and a non-zero number as an input. And a non-zero number can only be constructed with an enforced run-time check. For an example look into NonEmpty in haskell. A list type which always contains at least one element. Look at it this way. Underneath everything is bits anyway. Everything we have build on top is just "types" in a certain sense.