Natural division

[stefanobaghino]

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.

[SiriusStarr]

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

[Gabriel439]

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

[caesar]

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?

[stefanobaghino]

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.

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/

This was a very interesting read, thanks for sharing!

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

[SiriusStarr]

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

[stefanobaghino]

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.

Natural. My mistake, fixed the title.

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

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.

[stefanobaghino]

The conversion seems to have stalled.

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.

[SiriusStarr]

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

[Gabriel439]

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.

[caesar]

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

[Gabriel439]

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

[stefanobaghino]

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

[caesar]

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

[Gabriel439]

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”

[caesar]

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

[Gabriel439]

@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

[blamario]

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.

[caesar]

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

[Gabriel439]

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

Add arithmetic operations for Natural and Integer

… 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