5 ms·

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

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.

1-more 6y ago
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.
ogogmad 6y ago
> (But as a sidenote: couldn't you fix this with dependent types somehow?) Most proof assistants, including Lean, are built on dependent type theory.
- Tainnor 6y ago
  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).
  - OscarCunningham 6y ago
    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?
uryga 6y ago
> 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
- Tainnor 6y ago
  Well unless the system can somehow infer it for you. But maybe this is too hard a problem for now?
  - hansvm 6y ago
    It's impossible to infer in general, and any dependant type system needs to be somehow designed around that fact.
andolanra 6y ago
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#partial-and-checked-arithmetic 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.
- Tainnor 6y ago
  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.
  - klodolph 6y ago
    You could also argue that 0^0=1 is also not semantically correct, but it is the most widespread convention among mathematicians.
    - Tainnor 6y ago
      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.

1-more 6y ago

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.

ogogmad 6y ago

> (But as a sidenote: couldn't you fix this with dependent types somehow?) Most proof assistants, including Lean, are built on dependent type theory.

Tainnor 6y ago
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).
- OscarCunningham 6y ago
  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?

uryga 6y ago

> 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

Tainnor 6y ago
Well unless the system can somehow infer it for you. But maybe this is too hard a problem for now?
- hansvm 6y ago
  It's impossible to infer in general, and any dependant type system needs to be somehow designed around that fact.

andolanra 6y ago

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#partial-and-checked-arithmetic 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.

Tainnor 6y ago
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.
- klodolph 6y ago
  You could also argue that 0^0=1 is also not semantically correct, but it is the most widespread convention among mathematicians.
  - Tainnor 6y ago
    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.