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: https://www.hillelwayne.com/post/divide-by-zero/ 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?

3 Likes

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".

" x / 0 = 0 is a sensible behavior so long as you never use it", which is a contradiction.

Iā€™ve come to learn that sensible means wildly different things, even among mathematicians. I take it to mean ā€œis as useful as it can beā€, or ā€œyou can now do something which you couldnā€™t do otherwise, and nothing you were able to do before breaksā€.
With x / 0 = 0, you can compute a value for division for any pair of natural numbers, with the result being a natural number again. I call that sensible. If you want to take this as "x / 0 = 0 is useful because it prevents the results of all other divisions to be wrapped in a Some", then yes, thatā€™s it. I donā€™t know anything thatā€™s more mathematically sensible.

So what do you mean by sensible?

One sensible behavior would be that x / y = z implies that x = y * z for the domain over which division is defined. That sort of implication is what I mean by ā€œsupports equational reasoningā€

That puts limitations on the domain that are probably not reasonable for use in a programming languageā€¦ Youā€™d have to use something like rational numbers without 0. Do you want to add an extra type of numbers just for division?
(For natural numbers, thereā€™s of course x / y = z ā‡’ āˆƒr. y * z + r = x, but then you end up with r < y ā†ā†’ y ā‰  0, which you donā€™t want.)

@caesar: We can restrict the domain by returning an Optional Natural instead of a Natural. e.g. 4 / 2 = Some 2 and 1 / 0 = None Natural

When I went to elementary school we were taught that the lowest natural number was 1. I wonder if that would have been a better choice for Dhall. Anyway, Iā€™m a bit surprised nobody mentioned the possibility of adding a new type PositiveNatural and

Natural/divide : Natural ā†’ PositiveNatural ā†’ Natural

Parse donā€™t validate and all that. Of course this would open a can of arithmetic worms, the correct type of (+) to start with.

1 Like

@Gabriel439
Returning None doesnā€™t remove the input values from the domain (set of possible input values). I donā€™t think you can limit the domain in total computation, other than by introducing a new type like @blamario does. Can of worms.

Actually there might be a good solution to this problem. This discussion was revived on this issue:

ā€¦ and in the course of that discussion we figured out how to create a safe type for the division function, which is:

Natural/divide : āˆ€(divisor : Natural) ā†’ (Natural/isZero divisor == False ā‰” True) ā†’ Natural ā†’ Natural

For more details, see: Add arithmetic operations for Natural and Integer Ā· Issue #1213 Ā· dhall-lang/dhall-lang Ā· GitHub