Dividing by zero
Tags: functional, math, logic
Published: 2018-11-17 09:51:54

---
title: Dividing by zero
published: true
description: (⊬ (x / 0 ≠ 0)) ⊭ (⊢ (x / 0) = 0)
tags: #functional #math #logic
---

_This post relies heavily on some knowledge from the [functional fundamentals](https://dev.to/drbearhands/a-series-on-functional-fundamentals-48mb) 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<sup>1</sup>. 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](https://dev.to/drbearhands/functional-fundamentals-types-as-propositions-programs-as-proofs-56gh)? 

__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](https://en.wikipedia.org/wiki/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 `Int` any additional axioms. Let people make their own type for that.<sup>2</sup>
* In practice, I expect passing `0` as 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](https://dev.to/drbearhands/should-programming-languages-be-made-for-ides-rather-than-humans-3dnf).

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:
<sup>1</sup> 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.
<sup>2</sup> 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](https://en.wikipedia.org/wiki/Arithmetic_logic_unit), making it a rather imperative sort of type.

## References:

* [original article about the math of dividing by 0](https://www.hillelwayne.com/post/divide-by-zero/)