If you don't want to implement this function yourself, there's a show function in the standard library.
If you want to write it yourself: the usual way of converting a number into a string is to extract the digits by repeatedly dividing with a remainder. For example (remainders are written in parens):
7214 / 10 = 721 (4)
721 / 10 = 72 (1)
72 / 10 = 7 (2)
7 / 10 = 0 (7)
You then just collect the remainders into list, reverse it and convert the digits to chars. It might be tempting to try this in Agda as well, however, you'll run into problems with termination checker.
Firstly, you'll have to convince it that divMod (that is, division with remainder - modulus) terminates. You can just hardcode the divisor into the function and convincing the termination checker becomes easy.
The hard part is showing that repeatedly dividing the number by 10 actually terminates. This will most likely involve some rather complex tricks (such as well founded recursion).
If you want to know how it's done this way, take a look at the implementation linked above. Anyways, there's a bit less efficient but much simpler way of doing this.
Let's represent digits by a list of natural numbers.
Digits = List ℕ
We would like to write a function addOne, that (as the name suggests) adds one to a number represented by a list of digits, that is:
addOne : Digits → Digits
For this, we'll use the primitive pen & paper method: add one to the least significant digit; if the result is less than 10, we are done; if it isn't, write 0 and carry the 1 to the next digit. So, here's our carry:
data Carry : Set where
+0 : Carry
+1 : Carry
And here's the function that performs the addition - the second Carry argument can be thought of as a carry from the addition of previous two digits.
ripple-carry : Digits → Carry → Digits
ripple-carry ns +0 = ?
ripple-carry [] +1 = ?
ripple-carry (n ∷ ns) +1 with suc n ≤? 9
... | yes _ = ?
... | no _ = ?
The actual implementation is an exercise - use the description given above. Just note that we store digits in reverse order (this allows for more efficient and easier implementation). For example, 123 is represented by 3 ∷ 2 ∷ 1 ∷ [] and 0 by [].
We can recover the addOne function:
addOne : Digits → Digits
addOne n = ripple-carry n +1
The rest is just plumbing.
toDigits : ℕ → Digits
toDigits zero = []
toDigits (suc n) = addOne (toDigits n)
show : ℕ → String
show 0 = "0"
show n = (fromList ∘ map convert ∘ reverse ∘ toDigits) n
where
convert : ℕ → Char
convert 0 = '0'
convert 1 = '1'
convert 2 = '2'
convert 3 = '3'
convert 4 = '4'
convert 5 = '5'
convert 6 = '6'
convert 7 = '7'
convert 8 = '8'
convert 9 = '9'
convert _ = ' ' -- Never happens.
Used modules:
open import Data.Char
open import Data.List
open import Data.Nat
open import Data.String
open import Function
open import Relation.Nullary
I did some testing and it turns out that this method is actually fairly effective (especially when compared to the function from standard library).
The algorithm presented above needs to access O(n) digits (addOne needs to access only one digit in 90% of cases, two digits in 9%, three in 0.9%, etc) for a given number n. Unless we have some faster primitive operations (such as _+_ using Haskell's Integer behind the scenes), this is about the fastest we can get - we are working with unary numbers after all.
Standard library uses repeated division mentioned above, which is also (unless my math is wrong) O(n). However, this does not count handling of proofs, which adds enormous overhead, slowing it down to halt. Let's do a comparison:
open import Data.Nat
open import Data.Nat.Show
open import Function
open import IO
main = (run ∘ putStrLn ∘ show) n
And here are times for the compiled code (using C-c C-x C-c in Emacs). show from standard library:
n time
———————————————
1000 410 ms
2000 2690 ms
3000 8640 ms
If we use show as defined above, we get:
n time
———————————————
100000 26 ms
200000 41 ms
300000 65 ms
