4 ms·

Edit: I guess there's a reason I'm not a language designer. I've always thought that programming languages should have a nonzero number class in the vein of un

by c3534l 8y ago

Edit: I guess there's a reason I'm not a language designer. I've always thought that programming languages should have a nonzero number class in the vein of unsigned and float and that division should only be defined with a nonzero number class as the denominator. To divide a 64-bit float by another float, you'd have to either specify it as nonzero in the type or convert it somehow. Make division by zero impossible with the type-checker. Setting your programming language to evaluate x/0 = 0 seems evil. You're taking a bug in the programmers code and then hiding the fact that something logically unsound happened and in a way that would be very difficult to debug or detect. In fact, this is what happens when C# think it's being clever by returning infinity as the result of a division operation (which isn't even a number). It's a bug that winds up infecting every function that relies on that code without ever throwing an error. A programming language shouldn't return NaN or Infinity or anything like that when it encounters division by zero. It should demand you use error-handling or ensure it can't happen. If it does happen, it should tell you exactly where the problem occurred and not assume that some arbitrary value will work just as well.

throwaway080383 8y ago
You still have runtime issues if you're doing arithmetic with that type and end up getting zero.
- dllthomas 8y ago
  Only if arithmetic operators have to return the same type they operate on.
recursive 8y ago
So what type is `integer - integer`? It might be zero, but the type system doesn't statically know whether it is or not. If the result of every arithmetic expression is possibly zero, then you're back to run-time checks for every value. I don't see how this is practically useful.
- c3534l 8y ago
  I would think that the result of a nonzero int minus a nonzero int would be an integer. So f(nonzero x, y) = y / x is fine, but f(nonzero x, nonzero y, z) = z / (x - y) is not.
- Zalastax 8y ago
  In Agda you have the choice of either making it truncate at 0 or constrain the domain to (a - b, a >= b) in which case you don't hve to define the function when a < b. This of course is only suitable for theorem proving at the moment, but research is being done on how to have proofs like a >= b without sacrificing performance.
spooneybarger 8y ago
Hi, I'm on the Pony core team and I generally agree with you. The problem is, if you want to allow people to write high performance code, you are penalizing them becaues, for floating point: 1.0/0.0 is infinity. That's not C# being clever. That's C# following the floating point standard and using the math that the computer provides. To not use that standard means that you make every use of division slower, even if the programmer has in some way assert and otherwise knows that that they won't be dividing by zero. Note that 1/0 is integer math and for that there is no standard and its undefined behavior. You can't return NaN or Infinity for that without boxing numbers which is a performance hit and would be penalizing programmers who want/need to go as fast as possible.
- skybrian 8y ago
  I'm curious, what do you think about Julia's approach with its special "missing" value? Does this approach make sense outside the context of data analysis? https://julialang.org/blog/2018/06/missing https://julialang.org/blog/2018/06/missing
  - spooneybarger 8y ago
    I can't really comment. I don't know how they are doing it and why they made that choice. I assume that Julia was already boxing integers in some fashion at which point this 100% makes sense to me. Also, given the performance profile that you are seeking to allow programmers to achieve, I think boxing all integers makes sense, then you can give folks protection from integer overflow and underflow and otherwise make how the computer does math more closely approximate what we expect from doing math. I think that following my above reasoning that only having floating point math can also make sense. That is... in most programming languages 3 and 3.0 are different. Such that 3/ 2 = 1 and 3.0/2.0 = 1.5. We allow for 3/2=1 because, integer math is faster than floating point math and we want to allow folks to go as fast as possible when doing things like addition, subtraction and multiplication and accept that we can't represent all the numbers that come from division and give an approximation.
    - skybrian 8y ago
SamReidHughes 8y ago
Error handling your infinite results would dramatically slow down your programs. And C# doesn't think it's being clever, it's following IEEE float behavior implemented in the hardware.
- deleted 8y ago
  [deleted]
mywittyname 8y ago
I don't think this really solves the problem. It just kicks the same problem over to addition instead. let a = 17 let b = 10 let c = 7 let d = a - (b + c) // throws AddsToZeroException > Make division by zero impossible with the type-checker. Forcing programmers to consider division by zero when it occurs can be done simply by having the language compiler force handling of a divide by zero exception when division occurs.
- spooneybarger 8y ago
  > Forcing programmers to consider division by zero when it occurs can be done simply by having the language compiler force handling of a divide by zero exception when division occurs. Which is what Pony originally did and, lordy that can be an ergonomic nightmare when I know I don't have 0 and can prove it except, I can't prove it to the compiler and the type system. This problem is why integer division by zero is zero in Pony. Because, I can as a programmer prove that I won't divide by zero, but having a type system or compiler where I can prove it to it that is a computation engine that takes user input is a very non-trivial problem. The solution in Pony is going to be a combination of "safe math operators" and adding value dependent typing to the compiler. "safe math operations" would be: *?, /?, -?, +? that will error on division by zero as well as integer overflow and underflow (and have slower performance as well)
  - gowld 8y ago
    Wouldn't it be better to have an explicit unsafeCastToNonZero() function in the stdlib instead forcing invisible unsafe casts in every division statement of every program?
- dllthomas 8y ago
  > Forcing programmers to consider division by zero when it occurs can be done simply by having the language compiler force handling of a divide by zero exception when division occurs. That's materially different than a non-zero type, and IMO it's meaningfully worse. The type checker is most useful when it moves information.
deleted 8y ago
[deleted]
tikhonj 8y ago
This kind of type becomes really tedious to use unless there is some sort of viable "subtyping"—you certainly want to be able to use a non-zero number where any number works and, ideally, you want to be able to recover a non-zero number when you write a function that takes in a normal number and always returns a positive value. If you're forced to use a bunch of explicit conversion functions to achieve this you add a lot of noise to your code and, generally, the most common function is going to be along the lines of "I know this is positive, so throw an error if it's 0"—which is exactly what we get anyway. Explicit might be better than implicit most of the times, but it is possible to be too explicit. That said, we can achieve this, although it's probably a bit trickier than you'd think at first. The best option I know is called "refinement typing", which basically allows you to specify types as subsets (ie "the set of integers which are not 0") and automatically verifies whether your functions actually return a value in the subset. Liquid Haskell[1] is an example of a system you can use today to play with the idea. It uses an automatic logic solver (Z3) under the hood to automatically prove that your refinements hold. (For example, I believe it should be able to automatically verify that the function f x = abs x + 1 will never be 0.) [1]: https://ucsd-progsys.github.io/liquidhaskell-blog/ https://ucsd-progsys.github.io/liquidhaskell-blog/
- spooneybarger 8y ago
  Work was done on adding simple value dependent types to Pony as part of someone's academic work, sadly it hasn't made its way into mainline Pony yet. https://vimeo.com/175746403 https://vimeo.com/175746403
- Zarel 8y ago
  > generally, the most common function is going to be along the lines of "I know this is positive, so throw an error if it's 0"—which is exactly what we get anyway. That's still a lot better than before. It's not too hard to read a function and be reasonably confident that it will always return a positive value. On the other hand, it's pretty hard to audit an entire codebase to make sure a value can never be negative, or something like that. The main difference is probably only needing to do that audit once, when writing the function, instead of every time you need to rely on the function's return value being positive. It would also save a lot of work because a lot of operations _can_ be detected automatically. positive * positive = positive, etc. So you would only have to manually assert in the cases it wouldn't be doable automatically, which would be significantly fewer than before.
jay-anderson 8y ago
Rust recently added nonzero number types (see https://github.com/rust-lang/rfcs/blob/master/text/2307-concrete-nonzero-types.md https://github.com/rust-lang/rfcs/blob/master/text/2307-conc...). Though I believe the primary motivation here was the reduce memory usage in some special cases.
Someone 8y ago
I think you’ll find that extremely annoying in programs that do ‘real’ calculations. The compiler will rarely be able to prove that a divisor is non-zero, so you will have to add lots of code to handle edge cases. That can be worth it if you are writing robust numerical code, but I doubt even those writing numerical software libraries would want to handle each edge case. Worse, division by zero is just the tip of the iceberg. There’s overflow and underflow (which both can happen with addition, subtraction, multiplication, and division) and invalid operations (0/0, √-1, arcsin(2), etc), and you might even want to extend this to detect inexact computations (e.g. to properly report whether you are sure a later division by zero actually is a division by zero) IEE754 ‘won’ because it is relatively simple to use and many times good enough for real use.
dllthomas 8y ago
The complaints from tikhonj about verbosity are on point, but I think you're right about the shape of it. Other things being equal, it's much better to enable the type system to help you move checks further upstream.

by c3534l 8y ago

throwaway080383 8y ago

You still have runtime issues if you're doing arithmetic with that type and end up getting zero.

dllthomas 8y ago
Only if arithmetic operators have to return the same type they operate on.

recursive 8y ago

So what type is `integer - integer`? It might be zero, but the type system doesn't statically know whether it is or not. If the result of every arithmetic expression is possibly zero, then you're back to run-time checks for every value. I don't see how this is practically useful.

c3534l 8y ago
I would think that the result of a nonzero int minus a nonzero int would be an integer. So f(nonzero x, y) = y / x is fine, but f(nonzero x, nonzero y, z) = z / (x - y) is not.
Zalastax 8y ago
In Agda you have the choice of either making it truncate at 0 or constrain the domain to (a - b, a >= b) in which case you don't hve to define the function when a < b. This of course is only suitable for theorem proving at the moment, but research is being done on how to have proofs like a >= b without sacrificing performance.

spooneybarger 8y ago

Hi, I'm on the Pony core team and I generally agree with you. The problem is, if you want to allow people to write high performance code, you are penalizing them becaues, for floating point: 1.0/0.0 is infinity. That's not C# being clever. That's C# following the floating point standard and using the math that the computer provides. To not use that standard means that you make every use of division slower, even if the programmer has in some way assert and otherwise knows that that they won't be dividing by zero. Note that 1/0 is integer math and for that there is no standard and its undefined behavior. You can't return NaN or Infinity for that without boxing numbers which is a performance hit and would be penalizing programmers who want/need to go as fast as possible.

skybrian 8y ago
I'm curious, what do you think about Julia's approach with its special "missing" value? Does this approach make sense outside the context of data analysis? https://julialang.org/blog/2018/06/missing https://julialang.org/blog/2018/06/missing
- spooneybarger 8y ago
  I can't really comment. I don't know how they are doing it and why they made that choice. I assume that Julia was already boxing integers in some fashion at which point this 100% makes sense to me. Also, given the performance profile that you are seeking to allow programmers to achieve, I think boxing all integers makes sense, then you can give folks protection from integer overflow and underflow and otherwise make how the computer does math more closely approximate what we expect from doing math. I think that following my above reasoning that only having floating point math can also make sense. That is... in most programming languages 3 and 3.0 are different. Such that 3/ 2 = 1 and 3.0/2.0 = 1.5. We allow for 3/2=1 because, integer math is faster than floating point math and we want to allow folks to go as fast as possible when doing things like addition, subtraction and multiplication and accept that we can't represent all the numbers that come from division and give an approximation.
  - skybrian 8y ago

SamReidHughes 8y ago

Error handling your infinite results would dramatically slow down your programs. And C# doesn't think it's being clever, it's following IEEE float behavior implemented in the hardware.

deleted 8y ago
[deleted]

mywittyname 8y ago

I don't think this really solves the problem. It just kicks the same problem over to addition instead. let a = 17 let b = 10 let c = 7 let d = a - (b + c) // throws AddsToZeroException > Make division by zero impossible with the type-checker. Forcing programmers to consider division by zero when it occurs can be done simply by having the language compiler force handling of a divide by zero exception when division occurs.

spooneybarger 8y ago
> Forcing programmers to consider division by zero when it occurs can be done simply by having the language compiler force handling of a divide by zero exception when division occurs. Which is what Pony originally did and, lordy that can be an ergonomic nightmare when I know I don't have 0 and can prove it except, I can't prove it to the compiler and the type system. This problem is why integer division by zero is zero in Pony. Because, I can as a programmer prove that I won't divide by zero, but having a type system or compiler where I can prove it to it that is a computation engine that takes user input is a very non-trivial problem. The solution in Pony is going to be a combination of "safe math operators" and adding value dependent typing to the compiler. "safe math operations" would be: *?, /?, -?, +? that will error on division by zero as well as integer overflow and underflow (and have slower performance as well)
- gowld 8y ago
  Wouldn't it be better to have an explicit unsafeCastToNonZero() function in the stdlib instead forcing invisible unsafe casts in every division statement of every program?
dllthomas 8y ago
> Forcing programmers to consider division by zero when it occurs can be done simply by having the language compiler force handling of a divide by zero exception when division occurs. That's materially different than a non-zero type, and IMO it's meaningfully worse. The type checker is most useful when it moves information.

deleted 8y ago

[deleted]

tikhonj 8y ago

This kind of type becomes really tedious to use unless there is some sort of viable "subtyping"—you certainly want to be able to use a non-zero number where any number works and, ideally, you want to be able to recover a non-zero number when you write a function that takes in a normal number and always returns a positive value. If you're forced to use a bunch of explicit conversion functions to achieve this you add a lot of noise to your code and, generally, the most common function is going to be along the lines of "I know this is positive, so throw an error if it's 0"—which is exactly what we get anyway. Explicit might be better than implicit most of the times, but it is possible to be too explicit. That said, we can achieve this, although it's probably a bit trickier than you'd think at first. The best option I know is called "refinement typing", which basically allows you to specify types as subsets (ie "the set of integers which are not 0") and automatically verifies whether your functions actually return a value in the subset. Liquid Haskell[1] is an example of a system you can use today to play with the idea. It uses an automatic logic solver (Z3) under the hood to automatically prove that your refinements hold. (For example, I believe it should be able to automatically verify that the function f x = abs x + 1 will never be 0.) [1]: https://ucsd-progsys.github.io/liquidhaskell-blog/ https://ucsd-progsys.github.io/liquidhaskell-blog/

spooneybarger 8y ago
Work was done on adding simple value dependent types to Pony as part of someone's academic work, sadly it hasn't made its way into mainline Pony yet. https://vimeo.com/175746403 https://vimeo.com/175746403
Zarel 8y ago
> generally, the most common function is going to be along the lines of "I know this is positive, so throw an error if it's 0"—which is exactly what we get anyway. That's still a lot better than before. It's not too hard to read a function and be reasonably confident that it will always return a positive value. On the other hand, it's pretty hard to audit an entire codebase to make sure a value can never be negative, or something like that. The main difference is probably only needing to do that audit once, when writing the function, instead of every time you need to rely on the function's return value being positive. It would also save a lot of work because a lot of operations _can_ be detected automatically. positive * positive = positive, etc. So you would only have to manually assert in the cases it wouldn't be doable automatically, which would be significantly fewer than before.

jay-anderson 8y ago

Rust recently added nonzero number types (see https://github.com/rust-lang/rfcs/blob/master/text/2307-concrete-nonzero-types.md https://github.com/rust-lang/rfcs/blob/master/text/2307-conc...). Though I believe the primary motivation here was the reduce memory usage in some special cases.

Someone 8y ago

I think you’ll find that extremely annoying in programs that do ‘real’ calculations. The compiler will rarely be able to prove that a divisor is non-zero, so you will have to add lots of code to handle edge cases. That can be worth it if you are writing robust numerical code, but I doubt even those writing numerical software libraries would want to handle each edge case. Worse, division by zero is just the tip of the iceberg. There’s overflow and underflow (which both can happen with addition, subtraction, multiplication, and division) and invalid operations (0/0, √-1, arcsin(2), etc), and you might even want to extend this to detect inexact computations (e.g. to properly report whether you are sure a later division by zero actually is a division by zero) IEE754 ‘won’ because it is relatively simple to use and many times good enough for real use.

dllthomas 8y ago

The complaints from tikhonj about verbosity are on point, but I think you're right about the shape of it. Other things being equal, it's much better to enable the type system to help you move checks further upstream.