Hacker News Reader

Comment by Tainnor | Hacker News Reader

I ran into this argument before.

I can understand that it makes sense for proof assistants. As the post shows, proof assistants don't allow you to misuse that anywhere else.

(But as a sidenote: couldn't you fix this with dependent types somehow?)

I still think it would be wrong for a regular programming language. Afaik, the Pony language does this too, but that is a general-purpose programming language that does not check your logic, and I am very wary of something like that. People might type up some algorithms, or even just try to compute an average, and the system absolutely should yell at you if you try to divide by zero.

View on HN

Pony now includes both partial division (which raises an error when dividing by zero) and checked division (which returns a tuple of both a result and a boolean which indicates whether an error occurred): https://tutorial.ponylang.io/expressions/arithmetic.html#par...

For what it's worth, I'm willing to argue that Pony is making a strongly motivated choice by making x/0 return 0 by default with respect to their specific error-handling model. In general, I don't think it's as much of a problem as you might imagine. The average function is a perfect example: if I naïvely implement it in such a language, then it would mean… that average([]) returns 0. That doesn't seem terribly bad to me.

I don't think that the average of an empty list being zero is semantically correct, but I can accept that it may not be so bad in practice (e.g. if it shows up like that in a UI and you display the number of elements anyway).

But I still think in other situations I'd want to be yelled at for trying to divide by zero. E.g. imagine I'm trying to compute the slope of a secant between two points. If both points are the same, I'd like the compiler to yell at me (the problem either makes no sense here, indicating a problem somewhere else in my code, or that I should instead compute the derivative) - in most cases, 0 would be the wrong answer. I think the issue here is that with division by zero you lose continuity (unless you use +Inf) which can contradict intuition.

I'm not saying it doesn't work for Pony, maybe it does, but I don't think I would feel comfortable with that behaviour.

Silent wrapping around on overflow is arguably even worse, that I could definitely see leading to logic errors.

The compiler is unlikely to yell at you, the runtime normally will. Runtime errors are not usually very helpful, you are better off testing every division yourself (the Pony checked division model). Note that most non Intel CPUs don't have runtime exceptions for division by zero, Arm returns 0 and AFAIK Risc-V returns -1 but I might have misremembered. Intel is unusual in having an exception.

Yes, you're obviously correct, the compiler won't yell at me. I wasn't thinking clearly when I wrote that. I did mean the runtime. :)

But I disagree that runtime errors aren't helpful. They are very helpful to surface logic errors (if you have proper logging). If you catch a semantic error as early as possible, you have a better chance of making sure it doesn't propagate somewhere else, and it will be easier to debug the eventual issues. This is why I generally like assertions.

In practice I guess it's quite complicated. Even in a safety-critical environment where you don't want any errors, halting on an exception often seems not the best idea. For example in an air plane, a halting flight controller could be worse than some incorrect values. I generally agree that raising exceptions and logging them is the way to go if your budget allows, though the default behavior (crash, give 0, a large positive number, w/e) seems less clear (as often when choosing between lesser harms).

Another example: if your system is autonomous and re-initializing it will likely lead to the same "dirty" state (i.e. the division by zero), then recovery would not be possible after a crash. Could be a simple game, or perhaps a Mars rover for instance. In that case 1/0 = 0 is a solid choice.

Halting on exceptions of course means that you need to have some fault recovery mechanism, there are many patterns for that.

I'm not saying that 1/0 should just lead to a hard crash. Ideally you can identify subsystems and somehow handle unexpected errors at the boundaries and use some fallback behaviour.

But I agree that it's not easy and very dependent on the specific situation. I wrote a whole whitepaper about error handling and error recovery about the last system I was working on, because it's such a complex topic. It's just that "you should never raise runtime errors" or "all errors need to be handled at the level they are raised" are answers that sound good, but are impractical in certain situations. And as said, you need to deal with potential crashes anyway due to OOM, etc.

The Mars rover thing is completely different, because the engineering standards at NASA are so insanely high as to exactly prevent dumb errors like that. They can develop like that, but most other companies can't even begin to afford such a process heavy development and need to accept that programming errors are going to happen and there needs to be some recovery mechanism.

You could also argue that 0^0=1 is also not semantically correct, but it is the most widespread convention among mathematicians.

It IS semantically correct. The number of functions from a set of 0 elements to a set of 0 elements is exactly 1. No parallel argument exists for division by zero. The two situations are not analogous at all.

Mathematics is full of cases where the same notation means different things. You’ve kind of dodged the question of what 0^0 is by talking about set theory, because it is (in some sense) arbitrary that X^Y means Y -> X or its size (cardinal exponentiation), and in analysis may mean exp(y log x). We accept that for natural X,Y except (0,0) these must agree but that does not imply that they should agree at (0,0), because the definitions are simply not the same.

If you are serious about math, which it seems you are, I would be a bit more careful about “transporting” notation from one field from another and arguing about correctness.

The usual way to transport a definition from a discrete domain to a continuous one is a technique called analytic continuation. I am curious if there is an analytic continuation of the discrete X^Y which contains 0^0=1, and what that would look like, but at that point you’re definitely not talking about exponentiation any more.

See: https://en.wikipedia.org/wiki/Zero_to_the_power_of_zero

See: https://math.stackexchange.com/questions/11150/zero-to-the-z...

> it is (in some sense) arbitrary that X^Y means Y -> X or its size (cardinal exponentiation)

Are you referring to the notation? I don’t think notation is what’s being contested.

> in analysis may mean exp(y log x)

Doesn’t work with a base of 0.

> We accept that for natural X,Y except (0,0)

Why “except”?

> that does not imply that they should agree at (0,0), because the definitions are simply not the same.

The definition of exponentiation of reals typically starts with exponentiation of naturals as a given (see Baby Rudin).

> The usual way to transport a definition from a discrete domain to a continuous one is a technique called analytic continuation. I am curious if there is an analytic continuation of the discrete X^Y which contains 0^0=1

Analytic continuation refers to something else, but I get what you’re trying to say.

The answer is simple: Real exponentiation is an extension of natural exponentiation. Hence, it should have the same value as the latter wherever the latter is defined.

Yes, I’ve read that SE question before. It’s good that you brought it up. I recommend reading the comments under the accepted answer and the other answers as well.

Mathematicians not working in type theory generally agree that 1/0 is undefined (or if anything, they would set it to infinity, but even saying that would probably be too cavalier for most mathematicians). They do not necessarily for 0^0. There are good algebraic and combinatorial reasons for 0^0=1, while analysts will complain about non-continuity.

I think that’s missing the point. What I’m saying is “this is a convention, and because it is a convention, it may be reasonable to follow a different convention at times”. Different conventions are convenient for mathematicians working in different fields. Whether a convention is “semantically correct” is not a question that even makes sense, because when you define something, your definition is true by definition. The only real question here is whether you can reasonably expect people to understand you if you use different definitions.

This is a view of mathematics and programming that just completely ignores intuition. Of course, what you say is technically correct, yet mathematicians debate definitions all the time, precisely because it matters to them to get them "right" (of course, there's rarely one true answer).

This is even more true in programming. Yes, you can also learn all the type conversion rules of JavaScript, but many people agree that they are insane because they violate the principle of least surprise. Expectations matter, especially when you're fixing a bug at 3am.

Intuition is mostly an internalized notion of convention, and I don’t think that we can appeal to intuition to resolve much.

For students learning division, the fact that 1/0 is undefined is not an intuitive result and must be learned. This is their first time encountering something which is “not defined”.

We'll just have to disagree about this. I think intuition is incredibly important both in mathematics and in programming.

We agree that intuition is important, I think we disagree about where it comes from. Intuition comes from experience. A programming language is “intuitive” because it conforms to your previous experiences with programming languages.

To add to this, while you might argue that average([]) is undefined, it is no less defined than 0^0... that is, you can choose to define it by convention. For various reasons, most mathematicians have agreed that 0^0=1. This is not some obvious mathematical fact, but a choice of convention. For the same reason, we can choose that average([]) is 0.

Returning 0 for average([]) is useful. Returning a slope of 0 for a vertical linear regression is suspect.

Any choice of behavior for x/0 will be wrong in some context, and the question is really about how much help you want from the computer (both from the type system in trying to prevent/model division by 0 and at runtime via errors, via choosing a value for the division, etc).

yeah which is precisely what I'm saying (that last part).

Elm does this for integers (Floats support Infinity, natch) and I support it. Elm is meant for writing declarative UIs, and the only example I could think of for blindly dividing by 0 is taking the average of an empty list without checking first. But any time you might do that, you'd be better served by matching on the empty list _before_ trying to take the average and rendering something helpful for the user.

> couldn't you fix this with dependent types somehow?

quoting from the post:

> the way I had set things up, every time I used the [sqrt] symbol I had to supply a proof that what I was taking the square root of was non-negative.

"supplying a proof" is how you do it in dependently-typed systems afaik. the author tried it, and it was inconvenient

Well unless the system can somehow infer it for you. But maybe this is too hard a problem for now?

It's impossible to infer in general, and any dependant type system needs to be somehow designed around that fact.

> (But as a sidenote: couldn't you fix this with dependent types somehow?)

Most proof assistants, including Lean, are built on dependent type theory.

Sure but then I guess maybe you can find ergonomic improvements to your dependent type system so as not to run into the problems discussed in the article (e.g. having to reprove that something is not zero over and over again).

Maybe the way to do that would be to prove once that x is nonzero, use that to define r = 1/x, and thereafter use multiplication by r?

Reply on news.ycombinator.com