Natural division


:wave: everybody!

Last week I needed to write a piece of configuration where a container was assigned a certain amount of memory and a couple of configuration keys for the process running insideit were set as shares of the available memory. In other words, container has memory X and process has a key set to X / N and another which is X / M.

In order to get to this I implemented integer division using fold and asked on StackOverflow (link) whether my solution made sense or not.

Two nice outcomes were a very nice alternative solution and an interesting point raised by @Gabriel439 to implement integer division as a built-in.

This requires some discussion of course, firstly regarding whether you do see a need for this to be in the language and, if there are no objections, on how to deal with division by zero.

Unless we want to further discuss the introduction of a type which is all non-zero Naturals, I see three possible designs (in pseudo-Haskell):

  1. Return an Optional Natural which is Nothing when dividing by 0 and Just the integer division of the two dividends in other cases
    quotient :: Natural -> Natural -> Optional Natural
    quotient n 0 = Nothing
    quotient n m = Just (div n m)
  2. Return 0 when dividing by 0
    quotient :: Natural -> Natural -> Natural
    quotient n 0 = 0
    quotient n m = div n m
  3. Return the numerator when dividing by 0
    quotient :: Natural -> Natural -> Natural
    quotient n 0 = n
    quotient n m = div n m

The third was actually just the result of my first attempt at implementing the function. I don’t think it’s a good design in general but it didn’t look completely off in my specific case (do you want to know how many shares empty shares of memory in the container? All of them, buddy!) so I thought it was worth mentioning.

The first one is very explicit about the values on which the operation is defined, but I’m afraid it can become a bit unwieldy to manage. Users would end up writing boilerplate code to define a default value.

The second one doesn’t make much sense mathematically, but if well documented is probably the conservative choice to make.

Adopting 1. and 2. as separate available choices is another possibility (calling them, for example, safeDiv and div.


If the builtin provides option 1 (i.e. returning and Optional), it’d be easy enough to provide either/both of the other behaviors as Prelude functions, so that makes a bit more sense to me. It also avoids anyone ever being bit by unexpected behavior of a builtin.

Should quot be the builtin or quotRem, though? I suppose one could implement rem in the Prelude using quot, but idk if it would be preferable/more efficient to have the builtin return both values and then discard the unneeded one (especially since many usecases need both in my experience).


Another option is to provide a division operator where the denominator is guaranteed to be non-zero by adding 1 to it, like this:

Natural/dividePositive y x = x / (y + 1)

Then you could implement the Optional version efficiently in terms of that and Natural/isZero and Natural/subtract:

let Natural/divide : Natural → Natural → Optional Natural
      = λ(x : Natural) → λ(y : Natural) →
          if Natural/isZero y
          then None Natural
          else Some (Natural/dividePositive (Natural/subtract 1 y) x)

The main reason I suggest doing it this way is that if you statically know that the denominator is non-zero then you can skip the Optional check entirely. For example, if you wish to divide by 3, then you just write Natural/dividePositive 2 and no additional Optional-handling is necessary.

Also, to answer @SiriusStarr’s question, I think implementing just division is enough, since we can derive remainder from division + Natural/subtract


I’d like to point out that returning an arbitrary answer (mostly 0) when dividing by 0 is not such an uncommon thing to do: Then again, the fact that defining x / 0 = 0 is mathematically sound does not mean it’s a good idea to do in a programming language.

If you chose between Natural/divide x y = x / (y + 1) and a Natural/divide x 0 = 0, I think it’s just the question of “Which do you think will happen more often?”:

  • People accidentally dividing by 0
  • People forgetting to subtract 1 before dividing

I’d think the latter is a larger problem…

I also have another question: Why is it okay for Natural/subtract 3 1 to return 0, but division requires these kinds of stunts?


I am not very fond of the idea of having Natural/dividePositive in the language. It feels like it’s easy to misuse and it requires a wrapper in the Prelude to be used effectively.

This was a very interesting read, thanks for sharing!

I like this point made by @caesar but I’d like to give it a different spin: for those who have a better historical context, what was the driving principle behind the idea of “clamping” subtraction? We can probably use the same principle to come up to a design that makes sense.


Another question to consider is are we talking Natural division or Integer division? One can be implemented in terms of the other, of course, but the “add 1 to the denominator” approach obviously only works for Natural division.

The Optional solution personally seems like the most adherent to the principle of least astonishment (the “add 1 to the denominator” massively fails this). And I would say that builtins are probably more likely to be used by someone not checking the documentation than Prelude functions (since all the Prelude functions are documented in the file), so the most “obvious”/expected behavior should probably be the builtin, where there is a valid choice between several options.

As to @caesar’s question about Natural/subtract, I’d argue that that is also the least astonishing solution. Since the “correct” answer is limited by the type itself being a Natural, clamping negative results to zero seems the most logical thing to do (especially if one thinks of Naturals as S(S(S(Z))), in which case it makes sense that subtraction is unwrapping layers of succ one at a time, with the base case being that zero can’t be further unwrapped).


Natural. My mistake, fixed the title.

Probably the least astonishing thing is to return an Integer instead of a Natural, but returning zero to keep the operation closed on Naturals seems very practical.


The conversion seems to have stalled. :slightly_smiling_face:

I believe the two main idea are returning a Natural that is 0 when dividing by 0 or an Optional Natural that is None when dividing by 0.

I’d be happy to work on this if we have some form of consensus. I’m leaning slightly towards returning 0, it feels more consistent with the behaviour of Natural/subtract.


Is one of these more efficient to implement integer division with, since we’ll presumably want to have those in the Prelude?


I’d be okay with an Integer division that returned an Optional result, but I’m against returning 0. I’ve read the post you refer to, but there is a hole in the argument of the post, which is that you can’t prove any useful equations about integers where division by zero behaves that way. Division essentially becomes a useless operation for equational reasoning purposes under the limitations outlined in the post.


Division essentially becomes a useless operation for equational reasoning purposes

This is false, and that was the entire point of that article. I have no confidence that I can explain this better than the article, but I can’t help but try:

When you do equational reasoning (not sure what that is, but…), you have to make sure that no divisor in your equations is zero before rewriting any equations. Adding x / 0 = 0 doesn’t change that. So it can’t make anything useless.

Additionally, the whole maths-based discussion assumes that the numbers you’re working with are in a Field. The natural numbers aren’t a field, there aren’t any multiplicative inverses (for numbers except 1) which are usually used for defining what division is, hence none of the equations you think of hold. They only hold on things like rational, real, or complex numbers, or in Galois Fields.
I apologize for posting this link, it’s pointless to bring maths into this discussion.

What to return for division by 0 is an engineering question, and should imho be based on:

  • Returning 0 (or any other value) might mask some bugs
  • Returning an Optional means additional typing effort and is inconsistent with Natural/subtract (admittedly, the latter is a cosmetic flaw, thanks to type checking)

Regardless of the treatment of 0, because the equational reasoning you think of is not possible on naturals, adding natural/integer division might also cause people to run into ‘bugs’ like “Ooops, I divided 1337 by 1024 first and then multiplied by 42, why is my result 42 and not 54?” (I’ve seen it happen.)


@caesar: I’m not convinced by that line of reasoning. I read that as saying: "x / 0 = 0 is a sensible behavior so long as you never use it", which is a contradiction.


I thought the tl;dr was that "x / 0 = 0 is a sensible behaviour so long as you don’t assume that that means that 0 has a multiplicative inverse".