如何在agda中将数字转换为字符串？

Question

我需要写一些东西用 agda 将数字转换为字符串。之前发现有人问过string转agda的方法。

Agda：解析带有数字的字符串

我想过反过来使用它，

row-to-stringh : (m : ?) ? string
row-to-stringh 0 = "0"
row-to-stringh 1 = "1"
row-to-stringh 2 = "2"
row-to-stringh 3 = "3"
row-to-stringh 4 = "4"
row-to-stringh 5 = "5"
row-to-stringh 6 = "6"
row-to-stringh 7 = "7"
row-to-stringh 8 = "8"
row-to-stringh 9 = "9"
row-to-stringh _ = ""

但它不够好。当数字大于 9 时，它只会将其转换为“”，而不是“（那个数字）”。有人可以帮我弄这个吗？

Answer 1

如果你不想自己实现这个功能，show标准库中有一个功能。

如果您想自己编写：将数字转换为字符串的常用方法是通过重复除以余数来提取数字。例如（余数写在括号中）：

7214 / 10 = 721 (4)
721  / 10 = 72  (1)
72   / 10 = 7   (2)
7    / 10 = 0   (7)

然后，您只需将余数收集到列表中，将其反转并将数字转换为字符。在 Agda 中尝试此操作可能也很诱人，但是，您会遇到终止检查器的问题。

首先，您必须说服它divMod（即，除以余数 - 模数）终止。您可以将除数硬编码到函数中，并且说服终止检查器变得容易。

困难的部分表明，重复将数字除以 10 实际上会终止。这很可能会涉及一些相当复杂的技巧（例如有根据的递归）。

如果您想知道它是如何以这种方式完成的，请查看上面链接的实现。无论如何，这样做效率稍低但更简单。

让我们用自然数列表来表示数字。

Digits = List ?

我们想写一个函数addOne，它（顾名思义）给由数字列表表示的数字加一，即：

addOne : Digits ? Digits

为此，我们将使用原始的纸笔方法：在最低有效数字上加一；如果结果小于 10，我们就完成了；如果不是，则写 0 并将 1 带到下一位。所以，这是我们的携带：

data Carry : Set where
  +0 : Carry
  +1 : Carry

这是执行加法的函数 - 第二个Carry参数可以被认为是前两位数字相加的进位。

ripple-carry : Digits ? Carry ? Digits
ripple-carry ns       +0 = ?
ripple-carry []       +1 = ?
ripple-carry (n ? ns) +1 with suc n ?? 9
... | yes _ = ?
... | no  _ = ?

实际的实现是一个练习 - 使用上面给出的描述。请注意，我们以相反的顺序存储数字（这允许更有效和更容易实现）。例如，123 由 表示3 ? 2 ? 1 ? []，0 由表示[]。

我们可以恢复addOne函数：

addOne : Digits ? Digits
addOne n = ripple-carry n +1

其余的只是管道。

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.

使用的模块：

open import Data.Char
open import Data.List
open import Data.Nat
open import Data.String
open import Function
open import Relation.Nullary

我做了一些测试，结果证明这种方法实际上相当有效（尤其是与标准库中的函数相比时）。

对于给定的数字 n，上述算法需要访问O (n) 个数字（addOne在 90% 的情况下只需要访问一位，在 9% 的情况下只需要访问两位，在 0.9% 的情况下需要访问三位，等等）。除非我们有一些更快的原始操作（例如在幕后_+_使用 Haskell 的Integer），否则这是我们能得到的最快的 - 毕竟我们正在处理一元数。

标准库使用上面提到的重复除法，这也是（除非我的数学错了）O (n)。但是，这不包括处理证明，这会增加巨大的开销，使其慢下来以至停止。我们来做个对比：

open import Data.Nat
open import Data.Nat.Show
open import Function
open import IO

main = (run ? putStrLn ? show) n

这是编译代码的时间（C-c C-x C-c在 Emacs 中使用）。show来自标准库：

n       time
———————————————
1000     410 ms
2000    2690 ms
3000    8640 ms

如果我们show按照上面的定义使用，我们得到：

n         time
———————————————
100000    26 ms
200000    41 ms
300000    65 ms