4 ms·

What we need is a numeric type that cannot be zero.

drdaeman 20d ago
What we need are refinement types, where there’s a base type and a predicate. F* has this: val (/) : int -> (divisor:int { divisor <> 0 }) -> int
rhdunn 20d ago
It would be more flexible for a compiler to reuse the range analysis logic used in optimizations for statically verifiable divide by zeros. That way you could extend it to other things like statically verifiable overflows.
yeputons 20d ago
And also cannot be INT_MIN, otherwise -1 / INT_MIN is undefined behaviour(!) in C and C++.
winwang 20d ago
Every day, we stray closer to Haskell. Dare I say it: good!
duped 20d ago
For stuff like niche value optimization sure. For practical arithmetic code, nah. Like with this bug, all that changed is that garbage data in gives the user an error that they tried to process garbage data. Adding a new type doesn't make the code better, it just moves the error around. And you really don't want an infix division operator to fail to type check if the right hand side isn't a nonzero type, do you?
- robertlagrant 13d ago
  I think moving the error around is a good idea. E.g. integer division would end up with five cases: Int / 0 -> DivisionByZeroError PositiveInt / PositiveInt -> PositiveFloat PositiveInt / NegativeInt -> NegativeFloat NegativeInt / PositiveInt -> NegativeFloat NegativeInt / NegativeInt -> PositiveFloat And the type signatures of those possible return values can drive validation checks upstream of the calculation, so you're not actually ever going to return DivisionByZeroError. You're making sure through validation checks or case logic that that can never be returned.
roadbuster 20d ago
The only way to achieve this is to either put a runtime software check on a variable whenever it's assigned/used, or to literally add hardware support in processors themselves which literally throws an interrupt when a "neverShallBeZero" variable is assigned to zero. There's no viable way to statically prove at compile-time that these variables will never become zero at runtime, ultimately forcing a system of endless runtime checks (be it software or hardware)... which is why processors already throw exception interrupts when division by zero is attempted.
- colechristensen 20d ago
  You're kind of saying the only way to do it is in software or hardware :) An alternative https://en.wikipedia.org/wiki/Projectively_extended_real_line https://en.wikipedia.org/wiki/Projectively_extended_real_lin... The projectively extended real line defines division by zero, no reason you couldn't have a floating point type that implemented it. >There's no viable way to statically prove at compile-time that these variables will never become zero at runtime strongly typed programming languages like Ada allow for types which have ranges such as disallowing zero -- but also any arbitrary thing like you can create a floating point "degrees" type which is [0.0, 360.0] or any other ranged type
- inigyou 20d ago
  It's possible, just extremely difficult.

What we need are refinement types, where there’s a base type and a predicate. F* has this: val (/) : int -> (divisor:int { divisor <> 0 }) -> int

rhdunn 20d ago

It would be more flexible for a compiler to reuse the range analysis logic used in optimizations for statically verifiable divide by zeros. That way you could extend it to other things like statically verifiable overflows.

yeputons 20d ago

And also cannot be INT_MIN, otherwise -1 / INT_MIN is undefined behaviour(!) in C and C++.

winwang 20d ago

Every day, we stray closer to Haskell. Dare I say it: good!

duped 20d ago

For stuff like niche value optimization sure. For practical arithmetic code, nah. Like with this bug, all that changed is that garbage data in gives the user an error that they tried to process garbage data. Adding a new type doesn't make the code better, it just moves the error around. And you really don't want an infix division operator to fail to type check if the right hand side isn't a nonzero type, do you?

robertlagrant 13d ago
I think moving the error around is a good idea. E.g. integer division would end up with five cases: Int / 0 -> DivisionByZeroError PositiveInt / PositiveInt -> PositiveFloat PositiveInt / NegativeInt -> NegativeFloat NegativeInt / PositiveInt -> NegativeFloat NegativeInt / NegativeInt -> PositiveFloat And the type signatures of those possible return values can drive validation checks upstream of the calculation, so you're not actually ever going to return DivisionByZeroError. You're making sure through validation checks or case logic that that can never be returned.

roadbuster 20d ago

The only way to achieve this is to either put a runtime software check on a variable whenever it's assigned/used, or to literally add hardware support in processors themselves which literally throws an interrupt when a "neverShallBeZero" variable is assigned to zero. There's no viable way to statically prove at compile-time that these variables will never become zero at runtime, ultimately forcing a system of endless runtime checks (be it software or hardware)... which is why processors already throw exception interrupts when division by zero is attempted.

colechristensen 20d ago
You're kind of saying the only way to do it is in software or hardware :) An alternative https://en.wikipedia.org/wiki/Projectively_extended_real_line https://en.wikipedia.org/wiki/Projectively_extended_real_lin... The projectively extended real line defines division by zero, no reason you couldn't have a floating point type that implemented it. >There's no viable way to statically prove at compile-time that these variables will never become zero at runtime strongly typed programming languages like Ada allow for types which have ranges such as disallowing zero -- but also any arbitrary thing like you can create a floating point "degrees" type which is [0.0, 360.0] or any other ranged type
inigyou 20d ago
It's possible, just extremely difficult.