This post relies heavily on some knowledge from thefunctional fundamentals series, but is not an essential part of it. Read at your own peril!

A few days ago I had an interesting discussion in the Elm slack about integer division¹. What should it return when dividing by 0? And how does this affect the type of division?

I thought division by 0 was simply impossible, and giving 0 as the second input to a division function should be considered an error.

As it turns out, I was wrong. Math doesn't care about dividing by 0. It doesn't even really define division. If we define division as the inverse of multiplication, we are left with a partial definition, as there is no multiplicative inverse for 0.

That means division by 0 requires some kind of special rule, which we are free to define however we want. Since we make our own definition, nobody can prove us wrong! Division by 0 could return e.g. 0, 42, ⊥, a house, Cthulhu or a black hole.

For our type system, that would mean the return type can be(Int ∨ a), replacinga with anything.

Something interesting: if we define division by 0 as returning 0, we get 2 nice things: a return type that is justInt, and an additional axiom for algebra. So sayingx/0 = 0 has some motivation behind it.

The catch

While the axioms of numbers do not care what division by 0 returns, type systems do. Remember howa type system is essentially a proof?

If we use only the axioms provided for numbers, we cannot disprove the result of dividing by 0, but we cannotprove it either. Symbolically:⊬ Int/0 = 0. Ergo division does not constitute a proof ofInt → Int → Int, but only ofInt → IntButNotZero → Int.

We can, however, decide thatInt is more than just a number, by giving it an additional axiom, such asInt/0 = 0.
This would fundamentally change the meaning ofInt, which would no longer be isomorphic to (capped)Integer.

The discussion, therefore, is really about whatInt should be. While I've learned a lot, my opinion has remained unchanged:

• In theory, I believe we should use as small building blocks as is feasible. That means not givingInt any additional axioms. Let people make their own type for that.²
• In practice, I expect passing0 as the divisor is almost never intentional (it hasn't been for me), so the type system should catch it.

Although anInt return type for division makes it easier to read certain formulas, I believe that is a faulty solution to the broader problem of formula printing in programming. We have LaTeX for a reason. I've mentioned this problem in anearlier post.

Admittedly, the current tools being what they are, and time being limited, the argument that anInt return type results in nicer formulas holds, and each language must make its own decision based on intended use.

Notes:

¹ Floats are a bit of a different story: their imitation of infinite precision makes a 0 float value look a lot like a limit, soFloat/0=Infinity makes a lot of sense.
² I should note thatin theory I also don't thinkInt has any business being in functional programming in the first place, as it is tightly coupled to the internal workings of anALU, making it a rather imperative sort of type.

References:

• original article about the math of dividing by 0