Integer division in Dhall

Question

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.

Answer 1

TL;WR Edit:

let Natural/div = λ(n : Natural) → λ(m : Natural) → 
    let div = https://github.com/jcaesar/dhall-div/releases/download/1/quotient.dhall sha256:d6a994f4b431081e877a0beac02f5dcc98f3ea5b027986114487578056cb3db9
    in (div n m).q

---

Gabriel Gonzalez had me well nerd-sniped with his answer mentioning binary search. For a while, I was running in circles, trying whether the division by two necessary for the search couldn't be implemented by converting numbers to List Bool (well, it can, with the same problem as below), then I noticed that you can just implement long division:

let Natural/le = λ(a : Natural) → λ(b : Natural) → Natural/isZero (Natural/subtract b a)
let Natural/equals = λ(a : Natural) → λ(b : Natural) → Natural/le a b && Natural/le b a
  
let bits =    
      λ(bits : Natural) →
        Natural/fold
          bits          
          (List Natural)
          ( λ(l : List Natural) →
                l
              # [ merge
                    { Some = λ(i : Natural) → i * 2, None = 1 }
                    (List/last Natural l)
                ] 
          )
          ([] : List Natural)

in  λ(w : Natural) →
      let bits = bits w
      in  λ(n : Natural) →
          λ(m : Natural) → 
            let T = { r : Natural, q : Natural } : Type
            let div =
                  List/fold
                    Natural
                    bits
                    T 
                    ( λ(bit : Natural) →
                      λ(t : T) →
                        let m = m * bit
                        in  if    Natural/le m t.r
                            then  { r = Natural/subtract m t.r, q = t.q + bit }
                            else  t 
                    )               
                    { r = n, q = 0 }
            in  if Natural/equals m 0 then 0 else div.q

The only catch is that since there's no logarithm, you can't do the left-alignment in the tableau for long division, i.e. you don't know how the position of the MSB in n or how long subs has to be.

The theorist in me is sad because I just reduced division to (a coarse approximation of) logarithm, but the practitioner says "You're happy with u64 all the time, shut up."

---

[Edit] After a bit of thinking, I still can't compute the logarithm efficiently and for all inputs (I don't think that's possible). But I can find the next power of two from the logarithm for numbers up to a fixed large limit (2^2^23 or 42 × 10^2525221, but see below). It is possible to modify the above function (let's call it quotient) the following way:

let Natural/less =
      λ(a : Natural) → 
      λ(b : Natural) →
        if Natural/isZero (Natural/subtract a b) then False else True

let max = 23

let powpowT = { l : Natural, n : Natural }
      
let powpow =
      Natural/fold
        max
        (List powpowT)
        ( λ(ts : List powpowT) →
            merge 
              { Some = 
                  λ(t : powpowT) → [ { l = t.l + t.l, n = t.n * t.n } ] # ts
              , None = [ { l = 1, n = 2 } ]
              }
              (List/head powpowT ts)
        )
        ([] : List powpowT)

let powpow = List/reverse powpowT powpow
      
let bitapprox =
      λ(n : Natural) →
        List/fold
          powpowT 
          powpow
          Natural 
          ( λ(e : powpowT) →
            λ(l : Natural) →
              if Natural/less n e.n then e.l else l
          )
          0

in  λ(n : Natural) → λ(m : Natural) → quotient (bitapprox n) n m

This gives an acceptably efficient implementation of quotient, with a long division tableau that's maximally twice as large as necessary. On my desktop (62GB) m, I can compute e.g. 2^(2^18) / 7 in 11 seconds, but run out of memory for larger numbers.

Anyway, if you have beef with numbers that large, you're using the wrong language.

Answer 2

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:

https://discourse.dhall-lang.org/