I would like to compute the quotient of two Naturals. The requirement I need to fulfill is that I have a few configuration items that must be dynamically defined as shares of another (i.e. one container has X memory, two configuration keys for the process in that container are defined as X / Y and X / Z).
My first idea was to use recursion, but this approach didn't work:
let quotient =
\(n: Natural) ->
\(m: Natural) ->
if lessThan n m then 0
else 1 + quotient (Natural/subtract m n) m
In particular, Dhall complains that quotient has not been defined yet when I try to call it. Given Dhall's total functional paradigm (and my unfamiliarity with it) this seems reasonable. I assume there may be some way of doing it, but unfortunately I couldn't get to it.
I did another attempt using Natural/fold that works, but I'm not sure whether this makes sense.
let quotient =
λ(n : Natural) →
λ(m : Natural) →
let div =
λ(n : Natural) →
λ(m : Natural) →
let Div = { q : Natural, r : Natural }
in Natural/fold
n
Div
( λ(d : Div) →
if Natural/isZero m
then d
else if lessThan d.r m
then d
else { q = d.q + 1, r = Natural/subtract m d.r }
)
{ q = 0, r = n }
in (div n m).q
This passes all the following assertions.
let example1 = assert : quotient 1 1 ≡ 1
let example2 = assert : quotient 2 2 ≡ 1
let example3 = assert : quotient 3 1 ≡ 3
let example4 = assert : quotient 3 2 ≡ 1
let example5 = assert : quotient 9 4 ≡ 2
let example6 = assert : quotient 4 5 ≡ 0
let example7 = assert : quotient 0 1 ≡ 0
let example8 = assert : quotient 0 2 ≡ 0
let example9 = assert : quotient 1 0 ≡ 0
let example9 = assert : quotient 0 0 ≡ 0
let example9 = assert : quotient 2 0 ≡ 0
Returning 0 when dividing by 0 is fine in my case.
Is there a more idiomatic way of achieving this? I looked for a ready-made integer division function in the Prelude but couldn't find it.
Currently there is not a simpler way to implement Natural division besides what you have already written, but there may be a more efficient approach. Another approach that would give logarithmic time complexity but with a significantly more complex implementation is "guess and check", where you do a binary search around around the desired number to find the largest number x such that x * m = n.
I wouldn't really recommend that, though and I think probably a better way is to see if there is a sensible built-in to add to the language that could power integer division efficiently. Ideally such a built-in would be well-defined for all inputs, so adding integer division directly would probably not work (since x / 0 is not well-defined). However (I'm spitballing here), perhaps a built-in like Natural/safeDivide x y == x / (y + 1) could work, and then users could define their own wrappers around that if they want to permit division by 0. Probably the best place to solicit ideas for what the built-in would look like is the Discourse forum: