- Division must be impure (because it can throw an exception, crash the program, etc.)
- Division must be partial - i.e. return Option[Int].
Both seem worse compared to defining division by zero as zero. Coq, Lean, and Pony do the same. https://github.com/ponylang/pony-tutorial/blob/master/conten...
When you write code that may divide by zero you need to check the result afterwards (and in truly defensive programming that is every time you divide numbers). 0 is not a great choice because it doesn't necessarily mean you divided by zero - in floating point, dividing by a sufficiently large number or when working with the status register set to flush denormals to zero then normal division can result in 0. For integer division, any fraction will result in 0.
No valid division can result in NaN or INT_MAX.
- introduce a non-zero number type, define division as Number/NonZeroNumber -> Number, and provide a simple, non-verbose way to convert a Number into NonZeroNumber (with default value in case of zero, and/or direct assignment after a non-zero-check)
- optionally introduce an unsafe division operator that takes two Numbers and returns Option[Number]