Division by Zero

I’ve entered an issue about this a month ago
and because the reaction has been numb,
I wanted to ask if you saw it as a problem,
that Elm has no consistent or noticeable way
of telling, if a division by zero has occurred in a
calculation.
I have identified some functions,
that implemented some kind of division
and got radically different results.
Once Elm even crashed!
What do you think of this?
I have proposed a possible solution on GitHub,
but because I didn’t get any answer and it is
an extremely breaking change, I thought to ask
here, if you had an opinion on the matter.
The issue in question is: https://github.com/elm/core/issues/1072

4 Likes

I would handle this in a library: one that returns a Maybe type. For most cases having the deal with Maybe is just not needed and becomes extremely annoying code.

So I suggest you create an Elm library that implements your proposal.

That would be alright, if the function
modBy wouldn’t crash!
I have no idea how to fix that, but it needs to be fixed and
not in a library.

1 Like

An option would be to implement what you describe:
modBy returns (Maybe number)
but add functions like riskyModBy or crashableModBy that returns number. so that one does not need to worry about handeling maybe’s if you don’t need to.
The update for packages would be pretty simple: replace modBy with riskyModBy
Doing the oposite and call the new function safeModBy would not break anything, but in my opinion elm should be safe by default and then opt out of safety if you know what you are doing.
(Just like Http.request / Http.riskyRequest )

I dislike that solution, because “Elm has no runtime errors” is
one of it’s core promises.

I have a different proposal, that might help and not cause a
crash:
We create a new Value as part of Int and Float called
NotANumber that is returned if an invalid calculation (division by zero) is performed.
And if you make any operation using NotANumber
(+,-,*,/) NotANumber is the result.

Thus, you can check for this result whenever you want
and if a lazy or bad program were to output NotANumber
to the user, they would also immediately understand
the problem, while crashes or NaN or Infinity are less
helpful.

Hmm isn’t that what NaN already means?

Currently NaN is a member of Float but not Int. Maybe it would make sense to have it in Int as well, and have division and modBy 0 return NaN? I agree that having modBy crash is very unexpected.

1 Like

As I know it, there is no NaN value in Elm,
at least the following doesn’t compile:

NaN

The Error being:

I cannot find a `NaN` variant:

3|   NaN
     ^^^
These names seem close though:

    EQ
    Err
    GT
    LT

Hint: Read <https://elm-lang.org/0.19.1/imports> to see how `import`
declarations work in Elm.

Thus I think it doesn’t exist or it doesn’t exist in
any useful manner, because you can’t match for it.
And also, NaN is a cryptic shortcut for Not a Number
and anybody who isn’t familiar with programming, will
have to look it up or be left wondering, what it means,
that an App in Elm outputted NaN, while any user,
who can understand English, will understand when
an app prints “NotANumber”, even if it is written in a weird way.

In this solution, I have thought mostly about, what
would happen if Elm introduced this feature today.
Many developers wouldn’t fix their programs fast
enough, so it would only be caught, once the results
of a calculation were in some way printed,
which is when the users will know what NotANumber
means, while they are going to be confused with NaN
or Infinity or any other value of this sort.

NaN does exist in Elm, and there is the isNaN function to check for it (also isInfinite)
https://ellie-app.com/7Qfvy4RHZdNa1

Maybe it could be renamed to NotANumber though :man_shrugging:

My Problem wit that is, that you can’t use case … of to match
against NaN, or can you?
And if you can, do you have to do something like:

case x of
    (0 / 0) -> 

Which, to me, looks less like intention and more like an unreadable
hack, that nobody will understand, if they wouldn’t know what
0 / 0 computes to, but how should they know?
It isn’t just the total lack of documentation (I have a PR on GitHub
pending, that would have fixed, if you went back a few commits),
but also how all functions implementing division return something else on division by 0, so nobody could know that in general, all divisions by 0 return this or that value.

Where did you get the information, that NaN would only exist in
Float?
Because remainderBy returns NaN as a Float:

remainderBy 0 5 
NaN : Int

I would really like to know that.
And also whether NaN was a planned part of Elm’s Data types
or a legacy from compiling to JS.

Ah interesting, might have just remembered wrong :man_shrugging:

I’m guessing Elm follows JS and IEEE 754 regarding Float, for now anyway.

In my opinion, you pointed out two severe bugs which should be solved ASAP. After that, we can discuss if there is a handier way of doing division by zero. Edit: taking the dates of multiple, already, filled, issues into account, it’ll probably take some more time before this gets fixed…

First, that modBy 0 gives an error instead of 0 is bad because we don’t want runtime exceptions. Exactly this was the reason for Elm to decide that 1 // 0 == 0 instead of throwing an error. Edit: Apparently it is already on a fix-me list dating from 2015…

Second, that remainderBy 0 gives NaN leaks that Elm under the hood uses JavaScript numbers to represent integers. NaN is part of IEEE Floats, but not Ints. Edit: Harry shows this nicely in an issue comment.

So, both should either return 0 if their type stays Int -> Int -> Int to be consistent with //; or their types should be Float -> Float -> Float so that NaN can be a result of both calculations.

1 Like

I have already discussed in my issue, why returning 0 is bad.
It makes it impossible to test later on, if the calculation is invalid,
after all x/0 == 0/x using this rule. ( the first term being mathematically invalid, while the second is valid.)
I have stated this clearly in the first line of my issue:
There is no answer to the equation x = a/0 where a ∈ R.
Not even x = +∞ or x = - ∞ are valid.

I have created a small bug fix to all the affected functions using a case of matching and returning NaN if the divisor = 0.
It isn’t perfect, especially because I have no idea how the type checker will react.

The current state of things in Elm is kind of a mess:

Floats are messy but at least they’re IEEE floats so their behavior is well-documented.

Ints, on the other hand, are crazy. Part of this comes from the fact that they have to use JavaScript numbers internally which are floats; but a better-documented and saner solution is certainly desirable: For example, if Elm should compile to Web Assembly some day in the future.

The current state is this: Integer division rounds towards zero. x // 0 is defined to be 0 for any x. The expression remainderBy 0 x returns NaN but modBy 0 x gives a runtime exception. Further, you can get Infinity : Int by using round on Infinity : Float. You cannot get Infinity : Int by integer operations alone (I think). This combination of choices does not make any sense to me.

Here’s what I believe would be reasonable: Ints are 32 bit or 64 bit integers and their only values are the numbers between −2^31 − 1 and 2^31 (or with 63 instead of 31). So no NaNs or Infinitys in Int.

Integer division a // b does not perfectly answer the question “Which number q solves a = q · b?” anyways (because there is no such a integer if b does not divide a), so there is some leeway. The most sensible definition seems to me to ask for two numbers q and r that satisfy

a = b · q + r.

To make this well-defined, you have to restrict r. The two common choices are
(a) 0 ≤ r < |b| or
(b) 0 ≤ |r| < |b| where r has the same sign as a.
If a is positive these are the same. But for negative numbers, (a) is much more useful in my experience while (b) is more common in programming languages (I think it’s easier to implement in hardware). In version (a), integer division rounds towards negative infinity; in version (b), integer division rounds towards zero.

In both cases, the restriction does not work for b = 0. However, in this case r is already determined by the equation above: It has to be a because b · q is always 0 when b is 0. For q you can choose whatever you want but q = 0 seems the most symmetric choice in this case.

So here is what I think would be best:
a // b returns the result of (the ordinary division) a / b rounded down (i.e. towards negative infinity) if b ≠ 0 and it returns 0 if b = 0. modBy b a returns remainder of this division which is always a number between 0 (inclusive) and |b| (exclusive) if b ≠ 0 and it returns a if b = 0. (This implements version (a) above.) This definition makes it so that

(a // b) + modBy b a == a

always holds.

You can get rid of remainderBy or use it to implement version (b) above. In this case it should be accompanied by a second division function that rounds towards zero. If this function is call quotBy (for example) we would have

quotBy b a + remainderBy b a == a

for all numbers again.

I don’t have a good solution for rounding NaN : Float and Infinity : Float. Either change the type signature of these functions to round : Float -> Maybe Int or have them return 0 or maxInt. Defining them to be NaN : Int or Infinity : Int seems unwise as those definitions will almost certainly make it impossible to use Web Assembly ints in the future.

2 Likes

And how do you propose to solve the following problem?
There is an unknown function f which takes some arguments and may or may not do some division.
How do you check, if the results of f are invalid?
If the result is somehow 0 or a (to use your terminology), you can’t tell and have to lookup the function and check every calculation.

This situation might seem odd, but anyone using
a library will not want to inspect every function in
the same.

In conclusion, I think we have no choice but to use Maybe,
if you’re right and want to one day be able to compile to WebAsm.

I find this argument unconvincing because it applies to every unknown function. An integer division by zero is just one way in which there might be a subtle mistake in the definition of f. Another might be that f does an integer division but the default rounding of a // b leads to wrong results – I cannot check for that either, so maybe a // b should only be allowed if a actually divides b and return NaN otherwise?

There are essentially four solutions to a // 0:

  1. Return an arbitrary result – choosing 0 seems the most natural to me. The advantages are that you stay within Int and that // is a total function. The disadvantage is that a // 0 is probably a mistake that you are now silently ignoring.
  2. Return NaN or Infinity. The advantages are that you might be able to detect a division by zero (depending on the further computation). The disadvantages are that these are not usually values of Int so that you have to do your Int computations using floating point math. NaN as a value of Int is not something many people expect. (Not even the developers of Elm: Note that the isNaN function has type Float -> Bool.)
  3. Crash. The advantage is that you notice the (probably) mistaken calculation and don’t accidentally use its result in further computations, corrupting your data. The disadvantage is that you crash.
  4. Change the result type to Maybe Int. The advantage is that you cannot forget to handle the case of a division by zero. The disadvantage is that your computation now involves Elm constructs (which might make it harder to optimize) and that you always have to handle this case even though there are many situations where you know that division by zero cannot occur: For example, if the divisor is a fixed number.

None of these is perfect. The usual solution (in other languages) is 3 but it is not very Elm like. The costs of 2 and 4 seem very high for a relatively minor problem to me. That leaves option 1.

(In any case, the current state of affairs appears to be basically random with no unifying principle behind it.)

3 Likes

So, the perfect solution would be one, that:

  1. Doesn’t break the definition of Int
  2. Does signal to the program if division by zero has occurred
  3. Doesn’t force the handling of the division by zero case, if not necessary.

I think in the already existing functions in Basics.elm,
this is impossible to achieve.
I thus have this proposal:

  1. We define a value inside the Integer realm, that is used whenever /, //, modBy or remainderBy have to divide by 0. (This value would probably be 0)
  2. We define a set of functions, doing the exact same thing as /, //, modBy and remainderBy and return a Maybe number. These functions I would put into Basics.elm and refer to them in the documentation of the first set of functions.

With this solution, anyone who doesn’t want to, doesn’t
have to bother with division by 0, but can if they want to or need to.
And all informed developers know about this slightly inaccurate
behavior of /, //, modBy and remainderBy.

This proposal is probably the only thing we can do without major breaks.
It solves most of my problems, for whom I raised this issue
in the first place:

  • The inconsistency of division by 0
  • The crashing of modBy
  • The undocumented nature of the problem

Although it doesn’t solve the problem of lazy developers using the wrong functions where they really shouldn’t.

2 Likes

@Lucas_Payr proposed adding refinement types a while back Elm-Refine: Proposal. I’m guessing nothing came of it but the idea would be that, for example, modBy’s type signature would be changed from
modBy: Int -> Int -> Int to modBy: IntWithoutZero -> Int -> Int and IntWithoutZero would be defined with a special syntax (there’s more discussion in the thread about what that could look like)

{-| @refine \int -> int /= 0
-}
type alias IntWithoutZero =
    Int

The compiler would then verify that this condition holds everywhere modBy is called. I guess in cases where it can’t be proven, the user would need to write if value == 0 then ... else modBy value n or something.