8 ms·
> But is Pony doing something unsound? Absolutely not. It is totally fine to define 1/0 = 0. Nothing breaks It actually does break something, the symmetry betw
by luso_brazilian 8y ago
> But is Pony doing something unsound? Absolutely not. It is totally fine to define 1/0 = 0. Nothing breaks
It actually does break something, the symmetry between division and multiplication and the many pieces of code that assume that (x / y) * y equals x. Here is a naive and non practical example, but it is not impossible to find a real world example where this simplified code manifests itself accidentally or by design
function do_something_with_x(x, y) {
let ratio = x / y;
if (do_something_with_ratio(ratio)) {
return x * y;
}
else return null;
}
Again, this is a naive example but one that could manifest itself with a very imprecise result when y = 0
- leereeves 8y ago> (x / y) * y equals x Even without Pony's assumption, that's only true when y != 0.
- lmm 8y agoIt's true up to NaNs, which we can treat as bottoms.
- deleted 8y ago[deleted]
- umanwizard 8y agoYeah, (x/y)*y = x is true whenever it's a meaningful statement. x/y has no meaning in standard mathematics when y=0. 1/0 isn't infinity or anything else in standard math, it's literally un-grammatical nonsense.
- chess19 8y agoIt should be true for every y that is allowed in the denominator. That is how fractions are handled in higher math. (Either called "localization" or "ring of fractions").
- FlipperBucket 8y ago> the many pieces of code that assume that (x / y) * y equals x The same issue if division by zero throws an exception. This is simply a more practical approach that dispenses with the exception handling (ie becomes a less irregular test case). Edit: Not buggy behavior, when expected.
- lmm 8y agoAssuming an exception is equivalent to any non-exceptional value doesn't break anything. See "Fast and Loose Reasoning is Morally Correct".
- sclv 8y agoHoly moly that is not at all what that paper says! It specifically argues that certain equational properties of a given total language continue to hold in the total fragment of a given partial language. It is an embedding theorem combined with lifting properties, not a license to perform _any_ reasoning at all regarding the non-total portion of the language it considers!
- Jaxan 8y agoI would say an exception is much more convenient. Buggy code that silently continues to run is very hard to debug!
- cousin_it 8y agoI used to think the same way: let's throw an exception on divide by zero, and forget NaN like a bad dream! But then someone explained to me that it's common to feed a billion numbers into a long calculation, then look at the results in the morning and find them okay, apart from a few NaNs. If each NaN led to an exception, you'd come back in the morning and find that your program has stopped halfway through. So there's a certain pragmatism to having numeric code silently continue by default.
- seanmcdirmid 8y ago
- gjulianm 8y agoI think OP means that nothing breaks mathematically. It is not inconsistent and not false, so you can work with it. The only issue is to deal specially with the case of division by zero, which you have to do anyways. Code that assumes that (x/y) * y = x is wrong if you don't check for y = 0, independently of what you define x/0 to be.
- pmiller2 8y agoIt is inconsistent. If 1/0 = 0, then 1 = 0*0.
- tzs 8y agoIt's not inconsistent. See this article [1] for an explanation. It's the first thing covered in the "Objections" section. [1] https://www.hillelwayne.com/post/divide-by-zero/ https://www.hillelwayne.com/post/divide-by-zero/
- FlipperBucket 8y ago1/0 = undef (cast to 0) 1 != 0*0 I don't see the inconsistency. Abstract math vs practical application.
- pmiller2 8y agoYou’re doing something different than real number arithmetic. Saying 1/0 = x, and then treating x like a real number is inconsistent. But just saying “we are going to augment the real numbers with an element x that is not a real number, and then define some properties of x and prove things about it” is not.
- FlipperBucket 8y ago> You’re doing something different than real number arithmetic Computer languages execute on rules that are not utilizing real number arithmetic. I didn't want to mention it, but there's these things called floats... Edit: Pony took out the "normal" version of division by zero and suggest to write a wrapper to check beforehand.
- ballenf 8y agoWhat if number types were Optionals after any operation that could result in any kind of unusual number (sqrt(-1), Infinity, NaN)? Or maybe after every operation, since any operation could overflow the type. Do any languages do that? Seems more consistent (if way more hassle) than giving a mathematically false result out of pragmatism. At least in a strictly typed language.
- JadeNB 8y agoYou know what would happen. Math is ubiquitous in lots of code, so syntactic shortcuts would be introduced. Thus, we wouldn't use `a >>= (\x -> 2x) >>= (\x -> x^2)`, but would soon introduce syntactic sugar. For example, we could re-define `[asterisk]` so that it had type `Maybe Number -> Maybe Number -> Maybe Number`. You'd need a `return` (or `Just`) at the beginning, but soon that would be elided too, so that numeric literals would be auto-promoted to `Maybe Number`s. Then the language would add silent mechanisms to allow `Maybe Number`s to be displayed easily. You should check if your `Maybe Number`s are `Just Number`s before letting them out to play, but, if the language doesn't force you, then you know you won't. And then we're right back in the current situation.
- AnIdiotOnTheNet 8y agoZig defines checked versions of mathematical operators in its std lib [0], which return an Error Union. It's like an Optional (which Zig also has), but with an error instead of null. Your code can choose to handle this error however it wants. [0] https://ziglang.org/documentation/master/#Standard-Library-Math-Functions https://ziglang.org/documentation/master/#Standard-Library-M...
- klodolph 8y agoJavaScript does that…
- ballenf 8y agoHow so without optionals or static typing?
- klodolph 8y ago> …any pieces of code that assume that (x / y) * y equals x… What? If you’re using integers or floating-point numbers, that has never been true in general. Consider x=1, y=49 in the realm of IEEE doubles. Addition isn’t even associative, consider 1e-50 + 1 - 1.
- tlb 8y agoIt's talking about integer arithmetic, so it's already not true that (x / y) * y == x. For example, (5 / 2) * 2 == 4.
- vmchale 8y agoAlso just defining division to be whatever you want in the moment is not actually pragmatic, it's stupid and trivial. There's a reason we define a symplectic manifold the way we do. There's not a reason to say `1/0 = 0`, aside from the fact that the Pony designers didn't care to find a good solution to the problem.