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?