Modulo function for Natural numbers?

#1

Hello all,

I was wondering if anyone has been able to write a modulo function for Natural numbers in Dhall? It’s not entirely clear to me whether this is actually possible without recursion. I’ve read the section of the docs on translating recursive code to dhall but found it was stretching my rather limited math talent.

#2

Should anyone need this in the future, I’ve written a modulo function by riding off the back of the recursive List type:

let Prelude =
      https://prelude.dhall-lang.org/v20.1.0/package.dhall
        sha256:26b0ef498663d269e4dc6a82b0ee289ec565d683ef4c00d0ebdd25333a5a3c98

let modulo =
    λ(a : Natural) ->
    λ(n : Natural) ->
        let flattened = Prelude.List.generate a Natural (λ(_ : Natural) -> n)
        let ff =
            λ(_ : Natural) →
            λ(acc : Natural) →
            if Prelude.Natural.lessThan acc n
                then acc
                else Natural/subtract n acc
        in List/fold
            Natural
            flattened
            Natural
            ff
            a

I imagine this is not exactly the most optimal implementation but it works for my purposes for the time being.