(You may then do a separate proof in the case that x = 0, if you want to prove something for all x including 0.)
Relatedly, there is value to non-local error handling (i.e. unchecked exceptions), catching logical errors at a local level makes little sense.
First, we should be extending our hardware numerics to support the extended real number line, inclusive of infinity, in a way which causes a lot of these exceptions to disappear. Division by zero should result in an inf, not an exception or NaN.
Second, those exceptions which can't be eliminated DO need to be handled anyway. To say "but then we'd have to handle a bunch of exceptional cases everywhere!" is exactly the point. They do need to be handled.
Finally, language and compiler improvements can make handling exceptional cases easier. E.g. let numerical methods specify domain and range requirements and have these be compiler-enforced. Then the implementation is freed from handling exceptional conditions that only arise with inputs outside of its declared domain.
- Division by zero resulting in Inf could be fine in some cases, but might also lead to issue in other situations. The "calculate a slope through two separate points" is a good example: the slope through a single point is either undefined or the derivative, but it's not infinity. In any case, division by zero is sufficiently "weird" or "corner case-y" that you'd want to pay special attention to it. And if the runtime blows up in your face and tells you something is wrong, that can in many cases be better than to continue with wrong values (compile-time checks are always better, but not always feasible).
- First, it's not true that all exceptions need to be handled. This heavily dependens on the use case. If you're an app developer, then the app crashing might be a better (!) alternative than e.g. corrupting data, if it happens rare enough. After all, the user can just restart the app. Even if you write a server side app, you may get away with crashing, as long as you have a supervisor or so restarting unhealthy processes/instances. I'm not saying, crashes are good behaviour, but im some cases they are better behaviour than some of the alternatives (and in any case, no code is ever crash-proof, you can always have OOM, stack overflow, etc.). This is the concept of fault tolerance: you might not know which bugs happen, but you want to be able to recover from them somehow. In fact, if I'm not mistaken, Erlang basically takes this philosophy to an extreme.
- Even if you handle exceptions, you don't necessarily want to handle them locally. This is why many languages have unchecked exceptions. You're free to declutter a huge chunk of your application of error handling that would be extremely tedious, and just handle the (rare) exception at the top-level, or whatever intermediate layer best knows how to deal with it. Sometimes you just want to assert something about the state of your program that the compiler doesn't know and throwing an unchecked exception in case the condition is violated and only handling it at the topmost layer of your application is a perfectly reasonable decision.
The original article was about a theorem prover, but I was under the impression that the discussion had migrated to a more general discussion about division by zero in programming languages. Apologies if that wasn't intended.
mathematician here. The expression 1/0 is not "obviously" halt and catch fire. Extended real numbers (either projectively or affinely) are a well-known thing. If you see the expression 1/0 or 1/f(x) where f(x) may take the 0 value you do not halt and catch fire; you assume that the operations are taking place in a place where they make sense. A very common usage is when f(x)=0 for a zero-measure set of x, and then 1/f(x) has dirac masses at these points (weighted by the absolute value of the derivative of f).
On the other hand, I agree that "type theory" would sound like a ridiculously unnecessary abstraction to most of us.
This places the burden on the person using the function to prove that x isn't 0, but that's the price you have to pay to have a proper multiplicative inverse.
But, I don't think what you said is quite right, either. If you define f(x) = 1/x over the non-zero reals, then the range does have the same type as the domain- you can't get zero out of the function, so the range is also the non-zero reals.
Not quite. The extended reals are ℝ + {inf, -inf}. This has the problem that 1/x approaches inf from the right and -inf from the left.
As ogogmad notes, in order to define a value for 1/x at 0, you need the projectively extended reals.
For example, if we take a mercator projection of the globe onto a 2-infinite-ended cylinder, the latitude coordinate could meaningfully be either +∞ or –∞. If we take the stereographic projection of the globe onto the plane, every pair of coordinates with one infinite value corresponds to the same point on the sphere.
You are both right. There are several, different, extensions of the reals. The "projective" extension turns the real line into a (topological) circumference by adding a single point at infinity. The "affine" extension turns it into a closed segment by adding two infinities, one at each end; this corresponds to the convention used by ieee floating point numbers. There are many more extensions, like complex numbers, dual numbers, p-adic numbers, and in many of them (except complex numbers) you have various kinds of divide-by-zero fun.
Alternatively, defining f(0) to be infinity (a projectively extended real number) also allows f to be continuous.
Another possibility is to define f(0) to be some kind of "bottom" value. See the following tweets by Andrej Bauer: https://twitter.com/andrejbauer/status/1268860981943439361
Continuity is important because without it we lose computability. Every computable function is continuous (in an appropriate sense).
1. The article's way: "R^2->R", but garbage value for 0 in the second argument.
2. What you propose: "R^2->Maybe R"
3. The mathematician's dependent-type-theoretic way "R * (x:R, proof that x!=0) -> R",
4. the conventional way "R * (R\{0}) -> R".
They have their advantages and disadvantages. The first is useful in proof verification since it simplifies most proofs, from which perspective this garbage value of 0 is actually well-behaved, and doesn't need to be handled as a special case. But you allow seemingly nonsense theorems when you forget to condition (x>0).
What you propose is similar, except that you are forced to reason about whether the output value is valid.
3 and 4 are tedious, since you always need to prove that the inputs are nonzero. 4 is more tedious since you have merely shifted the problem of handling the zero case into proving properties about the canonical embedding "R->R\{0}" (which must still have a garbage value for 0). On the upside, these functions surject into R.
Or assume it. This is what you have to do in real life anyway. If you can't assume the inputs are nonzero you have to prove it. Otherwise the proof doesn't work.
Such as what? I’ve only spent a few hours with lean, but I’m fairly sure that any attempt to prove something silly would fail because it would catch the weird behavior of 0.
For example. If you tried to use a/a = 1 as the article mentions, you’d be unable to prove it without adding the condition that a != 0, and you’d be unable to use it further on without that condition in place.
“There exists a real number r such that 1/r = 0.”
If you try to translate this theorem into maths, you will run into trouble at some point. At which point exactly depends on how you want to make things precise... which is exactly what mathematicians avoid when talking about division in fields.
(n : Nat) -> (m : Nat) -> Nonzero m -> n / m * m = n