Comment by spooneybarger | Hacker News Reader

Comment by spooneybarger | Hacker News Reader

Parent Full thread

That's covered in the Pony tutorial.

https://tutorial.ponylang.org/gotchas/divide-by-zero.html

I can elaborate a bit on what is in the tutorial. With the current semantics, you as the application programmer can check for division by zero and throw `error` if you want. Otherwise, every division operation would be partial which given that pony forces you to handle all partial functions, can get to be very painful.

We are working on adding value dependent types and will be revisiting the divide by 0 question. Some work was done on that for a thesis a couple years back but hasn't been integrated into Pony by the author as they have had time constraints since leaving school. You can check out a video about the work here: https://vimeo.com/175746403

It's definitely something that folks bring up. We aren't thrilled with the current functionality but feel its better than the previous functionality and are looking to slow improve the situation over time.

It can definitely bite the uninitiated if they aren't careful.

It might be worth clarifying in that tutorial that this behavior is different for floating point division by zero (correct?) I believe that numerical tools like MATLAB give the same result as Pony for integer divide by zero, if that gives you or others more comfort... Although they return a 'divide by zero warning' at the same time which can be user-disabled.

It's better to be wrong and functional than correct and complicated?

PS: This is the approach PHP took in the early days too.

BTW, this is the same approach taken by the Coq, Isabelle and Lean theorem provers. In all of them, 1/0 = 0. It is certainly unconventional, but whether this is wrong is a matter of philosophy. Basically, division by zero is undefined, but you can define it to be zero and so extend the definition. This is consistent with the rest of arithmetic. You get more theorems (like for all a, b and c, a/c = b/c), but no inconsistencies.

You'd think that in these kinds of dependent type systems you would have to use the type system to prove that when doing a/b, b is never equal to 0.

Well, designing a language (even a mathematical one) is an art, and you need to trade off measures of convenience. The mathematical axioms that define division by zero to be equal to zero are consistent and so "correct" (if unconventional), and it turns out to be more convenient to define things in this way in those particular formalisms (rather than having to prove each time that you're not zero). You can define different theories in those systems that leave zero outside the domain of division or define it to be some value that means "undefined", but that's how it's done in the default arithmetical theories in those languages (and, BTW, Isabelle/HOL is not based on dependent types; Coq and Lean are). Other proof systems, like TLA+, do it differently.

For a recent discussion about this on the Isabelle mailing list, see here https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2018-Mar... (search for 1/0)

The users of Coq and Isabelle are generally people with mathematics degrees who check their work. Not your average programmer.

You are correct that the requirements are different, but not exactly for the reasons you mention. Users of those languages use them to prove theorems, and the theorems you get are correct with respect to the arithmetical theory used. Programmers may want some error condition when dividing by zero, because that's what they believe their users expect (say, the program drives some actuator, and bad things may happen if division by zero is not detected). So yeah, the justification for this behavior needs to be different.

It's an intersting philosophical conversation. Take floating point for example. I just fired up a Python interpreter and did:

>>> 0.3 * 3.0

0.8999999999999999

There's are a lot of areas of computer science that touch on these sorts of problems. And people love to do Wat! talks for all those fun edge cases where how computers work and how programming languages work run up against our expectations of what we expect to be correct.

It’s not wrong. It’s just a definition issue. The result is undefined in mathematics.

Throwing an error is actually “wrong” as the result should actually be undefined/null but most languages throw for practical reasons.

So in fact it’s most languages that are being “wrong but functional”. Pony is just functioning differently.

You are right, but the question is what most programmers want. It is certainly reasonable to believe that most want some special treatment of division by zero. Assuming the program is connected to some actuator (even a screen) -- as most programs are -- while not wrong mathematically, this results in something that is wrong "physically," and doing so silently, without a mechanism to later recover, from the result alone, whether division by zero occurred.

Right, though there’s nothing intrinsically better about throwing an error - it’s just the idiom programmers are more familiar with.

If it’s raised and documented well there’s no reason it wouldn’t work as undefined (could throw type errors on usage after that for example).

> Right, though there’s nothing intrinsically better about throwing an error - it’s just the idiom programmers are more familiar with.

Well, it can be argued that physics dictates an error is intrinsically better than 0, and that programs care about physics at least as much as about mathematics.

Reply on news.ycombinator.com