Hacker News Reader

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.

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

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.

If I understand correctly, instead of the usual kind of boxing, they use a separate type tag (one byte) and support union types with up to 255 other "special" enum values. The type tags and data are stored separately, so instead of an array of boxed values, they internally have two arrays, one for type tags and the other for data.

Apparently this can work well with SIMD instructions.

That's pretty cool. There's a lot that a couple of us on the Pony core team like about Julia from our limited knowledge. I'll have to look into that more.

I would like to add, given that this is my favorite talk, that the decisions a language ends up making in things like this are a good reflection of its values. Bryan Cantrill has an incredibly good talk on this that I recommend to anyone reading this:

https://vimeo.com/230142234

Julia doesn't box integers, that would destroy speed. It also doesn't protect from overflow/underflow. It specializes on Vector{Int} so that's it's just a standard vector of integers. Then Vector{Union{Int,Missing}} is stored in memory as a vector of integers with a bitarray declaring missings. Indexing operations are expanded to ifelse a check for the existence and then return the value if it exists or a missing. Then branches are added by the compiler to handle the small unions. This keeps pure integer use without overhead, and gives a small penalty when using missing (which doesn't turn out to be all that bad due to how pipelining is usually done), but it's safe and any type can have missing values.

Thank you. I look forward into learning more about how Julia handles this.

> We allow for 3/2=1 because, integer math is faster than floating point math

Is it? I didn't measured it myself, but from reading Abrash's The Black Book I had got an idea that floating point division is faster on x86 with FPU.

Anothor option is to use a NonZero type. A NonZero type is one that has been checked to not be zero. The type system ensures that you can only use a NonZero as a denominator in a division. You can minimize the number of checks for zero and the type system still protects you. And at points where performance trumps safetly you can still use a special version of division that returns 0 when the denominator is 0.

How can 1 / 0 = 0 be fast? It's not a standard floating point instruction, so extra logic is needed to convert the Inf to a 0.

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/

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

> 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.

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.

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.

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.

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.

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.

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.

> 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)

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?

> 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.

Rust recently added nonzero number types (see 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.

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.

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

Only if arithmetic operators have to return the same type they operate on.