[Theory part:]

So the issue here is that there exists a theorem:

If *a, k, m, n* are integers, *k != 0* and *a = km, a = kn*, then *m* and *n* are equal.

This is obviously false if *k = 0*, e.g. *0 = 0 * 3, 0 = 0 * 4*. And the relations *a = km, a = kn* can be rephrased as "*a* is divisible by *k*". This leads to the following theorem:

If *a, k* are integers, *k != 0* and *k* divides *a*, there exists a unique integer *m = a/k* that solves the equation *a = km*.

This actually is what allows us to define division on integers: it's an operation that always has either no solution or a single solution, unless the divisor is zero. The reason why some authors will disallow that *0* divides *0* is that then this second theorem could be restated without the condition *k != 0*; so it's a pure technicality.

[Practical part:]

What this means in practical terms though is that if somebody were to write:

```
if x.isDivisible(by: y) { return x / y } else { return nil }
```

(which looks totally reasonable at first sight), then this code will trap if `x`

and `y`

are both `0`

, if we define `isDivisible`

the way I previously suggested. The issue is here that the person writing this code implicitly used a theorem (see above) without checking for an additional condition, namely that `y != 0`

. The correct code would be:

```
if y != 0, x.isDivisible(by: y) { return x / y } else { return nil }
```

This leads to the following options for the implementation of `isDivisible`

:

- define the method such that it always returns a
`Bool`

. The burden of not using mathematical theorems without checking all the conditions would lie on the code author's side.
- trap when encountering
`y = 0`

. But, at least for this situation, this has zero benefits over trapping in the user code. Additionally, while *division* by zero *must* trap (because it's directly handled by the CPU), divisibility, when implemented in library code, has no such technical requirement; therefore this option makes little sense to me
- don't trap, but still keep the function partial. whether this is done by returning
`Bool?`

or by using `throws`

can be debated on a basis of ergonomics, but has the same implications semantically. this has the advantage of forcing the user to explicitly handle the zero divisor case (therefore the above code couldn't trap), but it also makes a function, which is supposedly basic, awkward to use (I think it's kind of hard to explain why `isDivisible(by:)`

should return an optional or throw).

Since I would rule out 2, this leaves options 1 and 3. I'm more partial towards 1 (it makes the definition of the function neater), but one could argue for option 3 too in the interest of safety.