I created an issue https://github.com/dhall-lang/dhall-lang/issues/1213

Perhaps this issue should be deleted in favor of a discussion here. Let me paste the text:

I think dhall could benefit from adding some arithmetic operations on Natural:

```
division with remainder: Natural.div 5 3 === Some 1, Natural.rem 5 3 === Some 2, Natural.div 1 0 === None Natural (returns None when trying to divide by zero)
the bit length of a natural number: Natural.bitLength 8 === 4, Natural.bitLength 7 === 3, Natural.bitLength 0 === 0
greatest common divisor: Natural.gcd 9 6 === 3, Natural.gcd 1 0 === 0
integer power: Natural.pow 2 5 === 32, Natural.pow 10 0 === 1
integer square root: Natural.sqrt 9 === 3, Natural.sqrt 10 === 3
```

These operations can be implemented more easily using foldWhile:

let foldWhile: ∀(n: Natural) → ∀(res : Type) → ∀(succ : res → Optional res) → ∀(zero : res) → res =

λ(n: Natural) → λ(R: Type) → λ(succ: R → Optional R) → λ(zero: R) →

let Acc: Type = { current: R, done: Bool }

let update: Acc → Acc = λ(acc: Acc) →

if acc.done then acc

else merge { Some = λ(r: R) → acc // {current = r}, None = acc // {done = True} } (succ acc.current)

let init: Acc = { current = zero, done = False }

let result: Acc = Natural/fold n Acc update init

in

result.current

I propose to add these operations as built-ins. These operations can be implemented in plain dhall via Natural/fold, although inefficiently since there is no way to stop iterating when the result is already obtained.

Example code is here: https://github.com/winitzki/scala-examples/blob/master/chapter11/src/test/scala/example/naturals.dhall

Similar code for foldWhile can be added to List.

What do you think?