This post relies heavily on some knowledge from the functional 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 division1. 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), replacing a with anything.
Something interesting: if we define division by 0 as returning 0, we get 2 nice things: a return type that is just Int, and an additional axiom for algebra. So saying x/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 how a 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 cannot prove it either. Symbolically: ⊬ Int/0 = 0. Ergo division does not constitute a proof of Int → Int → Int, but only of Int → IntButNotZero → Int.
We can, however, decide that Int is more than just a number, by giving it an additional axiom, such as Int/0 = 0.
This would fundamentally change the meaning of Int, which would no longer be isomorphic to (capped) Integer.
The discussion, therefore, is really about what Int 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 giving
Intany additional axioms. Let people make their own type for that.2 - In practice, I expect passing
0as the divisor is almost never intentional (it hasn't been for me), so the type system should catch it.
Although an Int 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 an earlier post.
Admittedly, the current tools being what they are, and time being limited, the argument that an Int return type results in nicer formulas holds, and each language must make its own decision based on intended use.
Notes:
1 Floats are a bit of a different story: their imitation of infinite precision makes a 0 float value look a lot like a limit, so Float/0=Infinity makes a lot of sense.
2 I should note that in theory I also don't think Int has any business being in functional programming in the first place, as it is tightly coupled to the internal workings of an ALU, making it a rather imperative sort of type.
Top comments (4)
A church encoding implementation of division of zero seems like an interesting problem. It's hard definitely but worth trying to get a view of shortcomings of Int as a data type.
If we go by a recursive division implementation, we get an infinite recursion. That should be expected :-P
I needed a refresher about church encoding myself so I'll add a clarification for other users:
Church encoding essentially defines numbers using 0 and a "
nextfunction". E.g. 1 isnext(0)and 4 isnext(next(next(next(0)))).Division of church-encoded numbers comes down to repeatedly subtracting the divisor from the dividend until you get a number that is smaller than the divisor, then counting how many iterations you've had.
With this kind of division, dividing by 0 results in an infinite loop. Although we cannot evaluate this, we could 'cache' the value of division by 0 to infinity.
Back to the Curry-Howard isomorphism: as I briefly mentioned, under infinite recursion, the type system does not constitute a proof, so again, you could say that, even for church-encoded numbers, we do not have any proof for division by 0, ergo it should not be in the type system.
On the other hand, you might say that the proof system for weak functional programming (which is what we generally refer to as function programming) is simply not sound (i.e. wrong), and allows for infinite recursion as a 'proof', in which case dividing a church-encoded number by 0 results in infinity.
It really boils down to the context and the problem, any recursive definition could potentially be infinite recursive. Our best bet is always keeping the domain in check for the said problem and evaluating our proof. Also, even in formal math proofs a lot of things are just skipped over and considered a given. Division by zero is one of those.
Though, integer representation is a pretty fluid problem, in that there can be more than one representations that get the job done. So, when using lambda calculus or purely functional programming as a basis for proof one could argue that there may exist a better representation.