6 ms·

I think this behavior makes perfect sense when you view it through the lens of type theory. Functions that return a real number must always return a real number

by e79 6y ago

I think this behavior makes perfect sense when you view it through the lens of type theory. Functions that return a real number must always return a real number. Some function types are defined by something like ‘R, error’, and then it’s up to the caller to check ‘error’. Others throw exceptions that bubble up the call stack and may never return ‘R’, which in a sense breaks the type contract and has “exception” theory preceding type theory.

kevinbuzzard 6y ago
(disclaimer: I'm the author of the blog post). The argument the other way is that if a mathematician sees this convention, their reaction is likely to be "that's just silly, 1/0 is obviously 'halt and catch fire'", and any attempt to defend this by saying "it makes perfect sense viewed through the lens of type theory" runs the risk of the response "well I won't be doing my mathematics in type theory then". In the comments to the blog post (and in personal emails) people have suggested that instead of trying to defend the idea that 1/0=0 (which is what I was trying to do, given that I am now very much used to it) I should instead be complaining to the Lean designers to make the front end "work more like a mathematician expects". However this is difficult, because talking to mathematicians it becomes clear that they have different opinions about what "actually happens" when you put garbage in.
- e79 6y ago
  What would “halt and catch fire” look like for a proof assistant? If I’m trying to prove a theorem that performs division over the reals, would it then have to mechanically prove that there cannot exist any inputs that would result in division by zero? Isn’t that then itself a theorem that I’d have to explicitly define using tactics?
  - thaumasiotes 6y ago
    Well, if you're doing a proof and (for example) you want to cancel x in the numerator of a fraction with x in the denominator, you then apply the constraint x ≠ 0 to every subsequent step of the proof. (You may then do a separate proof in the case that x = 0, if you want to prove something for all x including 0.)
    - zozbot234 6y ago
      That's actually needed for a real proof. One should keep in mind that y = ax is not injective if a=0, so that "cancel a variable" step you're thinking of is most likely incorrect without that side-condition.
      - thaumasiotes 6y ago
        ...yes?
- garmaine 6y ago
  Except that's a false dichotomy. Sqrt() could instead return Enum { Real | Complex } and the typing enforces that the surrounding math handles the appropriate cases (or proves that negative input is not allowed). Likewise for division by zero, etc.
  - Tainnor 6y ago
    Sure, but imagine that every time you divide, the result may be optional. At least in a general purpose language that would clutter the code with optional handling even in cases where you know (but the compiler doesn't) that the value absolutely can't be zero. Relatedly, there is value to non-local error handling (i.e. unchecked exceptions), catching logical errors at a local level makes little sense.
    - garmaine 6y ago
      There's a couple of points to be made to that. 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.
      - Tainnor 6y ago
        I feel you're missing the point: - 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.
- enriquto 6y ago
  > if a mathematician sees this convention, their reaction is likely to be "that's just silly, 1/0 is obviously 'halt and catch fire'" 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.
contravariant 6y ago
Well, if you ask the mathematicians then f(x) = 1/x isn't defined on the real numbers, it's defined on the non-zero real numbers. It always returns a real number but it's domain has a different type. 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.
- ragnese 6y ago
  f(x) = 1/x is also defined over what we call the "extended reals" which is just R + inf. 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.
  - ogogmad 6y ago
    The codomain doesn't have to equal the image. The image is the non-zero reals, but the codomain could be any superset of it (including all of R). The word "range" is ambiguous.
    - ragnese 6y ago
      Thank you. I've forgotten some of the terminology, since I haven't thought about real math in a few years. :(
  - contravariant 6y ago
    There's no real problem with defining the codomain to be too big. Although you can indeed also pick the non-zero reals as the co-domain.
  - thaumasiotes 6y ago
    > f(x) = 1/x is also defined over what we call the "extended reals" which is just R + inf. 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.
jhanschoo 6y ago
I don't understand what you mean. You still have the different obvious ways of formulating, e.g. division in type theory: 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.
- e79 6y ago
  I agree that they all have their advantages and disadvantages. My point was agreeing with the author that a proof assistant returning 0 for n/0 isn’t nonsensical. It’s debatable whether it is the best approach, but it is sound. The reasoning is clear if you consider R to be an inductive type, which many proof assistants including Lean do. Returning anything but an element of an inductive type would be wrong.
- kmill 6y ago
  By the way, 3 and 4 are pretty much the same in Lean, assuming you define "R\{0}" using complementation rather that somehow defining the nonzero reals from scratch.
- SquishyPanda23 6y ago
  > 3 and 4 are tedious, since you always need to prove that the inputs are nonzero. 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.
  - 6y ago
dependenttypes 6y ago
What you are saying might make sense in regular programming languages like go/rust/etc but it does not make sense in type theory. Rather the reason that n / 0 = 0 makes sense in type theory is that you can simply define types such as (n : Nat) -> (m : Nat) -> Nonzero m -> n / m * m = n as in you do not need to make your laws hold true for every possible input of / which is why it does not break regular mathematics.

by e79 6y ago

kevinbuzzard 6y ago

(disclaimer: I'm the author of the blog post). The argument the other way is that if a mathematician sees this convention, their reaction is likely to be "that's just silly, 1/0 is obviously 'halt and catch fire'", and any attempt to defend this by saying "it makes perfect sense viewed through the lens of type theory" runs the risk of the response "well I won't be doing my mathematics in type theory then". In the comments to the blog post (and in personal emails) people have suggested that instead of trying to defend the idea that 1/0=0 (which is what I was trying to do, given that I am now very much used to it) I should instead be complaining to the Lean designers to make the front end "work more like a mathematician expects". However this is difficult, because talking to mathematicians it becomes clear that they have different opinions about what "actually happens" when you put garbage in.

e79 6y ago
What would “halt and catch fire” look like for a proof assistant? If I’m trying to prove a theorem that performs division over the reals, would it then have to mechanically prove that there cannot exist any inputs that would result in division by zero? Isn’t that then itself a theorem that I’d have to explicitly define using tactics?
- thaumasiotes 6y ago
  Well, if you're doing a proof and (for example) you want to cancel x in the numerator of a fraction with x in the denominator, you then apply the constraint x ≠ 0 to every subsequent step of the proof. (You may then do a separate proof in the case that x = 0, if you want to prove something for all x including 0.)
  - zozbot234 6y ago
    That's actually needed for a real proof. One should keep in mind that y = ax is not injective if a=0, so that "cancel a variable" step you're thinking of is most likely incorrect without that side-condition.
    - thaumasiotes 6y ago
      ...yes?
garmaine 6y ago
Except that's a false dichotomy. Sqrt() could instead return Enum { Real | Complex } and the typing enforces that the surrounding math handles the appropriate cases (or proves that negative input is not allowed). Likewise for division by zero, etc.
- Tainnor 6y ago
  Sure, but imagine that every time you divide, the result may be optional. At least in a general purpose language that would clutter the code with optional handling even in cases where you know (but the compiler doesn't) that the value absolutely can't be zero. Relatedly, there is value to non-local error handling (i.e. unchecked exceptions), catching logical errors at a local level makes little sense.
  - garmaine 6y ago
    There's a couple of points to be made to that. 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.
    - Tainnor 6y ago
      I feel you're missing the point: - 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.
enriquto 6y ago
> if a mathematician sees this convention, their reaction is likely to be "that's just silly, 1/0 is obviously 'halt and catch fire'" 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.

contravariant 6y ago

Well, if you ask the mathematicians then f(x) = 1/x isn't defined on the real numbers, it's defined on the non-zero real numbers. It always returns a real number but it's domain has a different type. 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.

ragnese 6y ago
f(x) = 1/x is also defined over what we call the "extended reals" which is just R + inf. 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.
- ogogmad 6y ago
  The codomain doesn't have to equal the image. The image is the non-zero reals, but the codomain could be any superset of it (including all of R). The word "range" is ambiguous.
  - ragnese 6y ago
    Thank you. I've forgotten some of the terminology, since I haven't thought about real math in a few years. :(
- contravariant 6y ago
  There's no real problem with defining the codomain to be too big. Although you can indeed also pick the non-zero reals as the co-domain.
- thaumasiotes 6y ago
  > f(x) = 1/x is also defined over what we call the "extended reals" which is just R + inf. 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.

jhanschoo 6y ago

I don't understand what you mean. You still have the different obvious ways of formulating, e.g. division in type theory: 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.

e79 6y ago
I agree that they all have their advantages and disadvantages. My point was agreeing with the author that a proof assistant returning 0 for n/0 isn’t nonsensical. It’s debatable whether it is the best approach, but it is sound. The reasoning is clear if you consider R to be an inductive type, which many proof assistants including Lean do. Returning anything but an element of an inductive type would be wrong.
kmill 6y ago
By the way, 3 and 4 are pretty much the same in Lean, assuming you define "R\{0}" using complementation rather that somehow defining the nonzero reals from scratch.
SquishyPanda23 6y ago
> 3 and 4 are tedious, since you always need to prove that the inputs are nonzero. 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.
- 6y ago

dependenttypes 6y ago

What you are saying might make sense in regular programming languages like go/rust/etc but it does not make sense in type theory. Rather the reason that n / 0 = 0 makes sense in type theory is that you can simply define types such as (n : Nat) -> (m : Nat) -> Nonzero m -> n / m * m = n as in you do not need to make your laws hold true for every possible input of / which is why it does not break regular mathematics.