在 idris 中实现 BigDecimal答案

【问题标题】：implementation of BigDecimal in idris在 idris 中实现 BigDecimal
【发布时间】：2016-11-12 09:36:02
【问题描述】：

我正在尝试在 Idris 中实现 bigdecimal。到目前为止我有这个：

-- a big decimal has a numerator and a 10^x value
-- it has one type for zero, 
--TODO the numerator can't be zero for any other case
--TODO and it can't be divisible by 10
data BigDecimal : (num : Integer) -> (denExp : Integer) -> Type where
  Zero : BigDecimal 0 0
  BD : (n : Integer) -> (d : Integer) -> BigDecimal n d

我想强制执行上面“TODO”标记的限制。但是，我只是在学习 Idris，所以我什至不确定这种限制是否是个好主意。

一般来说，我正在尝试创建一个能够使用任意精度计算多种（加密）货币的税收计算工具。我希望能够尝试使用证明者来证明程序的一些属性。

所以，我的问题是：

尝试强制执行我指定的限制是一个好的设计决策吗？
是否可以在 Idris 中进行这种限制？
这是 Idris 中 BigDecimal 的良好实现吗？

编辑：我在想类似“BD : (n : Integer) -> ((n = 0)=Void) -> (d : Integer) -> BigDecimal n d”的东西，所以你必须通过证明那 n 不为零。但我真的不知道这是否是个好主意。

编辑 2：针对 Cactus 的评论，这样会更好吗？

data BigDecimal : Type where
    Zero : BigDecimal
    BD : (n : Integer) -> (s : Integer) -> BigDecimal

【问题讨论】：

一般来说，BigDecimals 由一个 BigInteger 表示数字（用于未缩放的值）和一个表示小数点应该在哪里的比例或指数（这也可以是一个负值，所以你可以也代表非常大的值）。不幸的是，我不认识 Idris，所以我无法用那种语言告诉你如何做到这一点。您的分子想法听起来更像是 BigFraction 或 BigRational。 IMO，这会让事情变得有点复杂。
实际上我使用的是与您所说的相同的想法。我可能不应该称它为分子，但我在想（分子）/（10 **（分母指数））。
那么命名确实很奇怪。您的分子是我的意思的未缩放值，您的分母指数是比例。所以值 1.000 表示为未缩放的值 1000 和比例 3。只需确保在加减时正确放大或缩小，并在乘法或除法时调整比例。此外，如果您除以，请将分子按您想要的精度放大并正确舍入结果。 IE。精度为 10，将分子乘以 10**10 然后除，否则 1 / 10 可能会导致 0 而不是 0.1000000000。
您当前的设计意味着每个数字都由一个单独的单例类型表示——我认为这不是您想要的。为什么你有分子和大小作为指标？
@"Rudy Velthuis" 重点是让 1000 不是有效的分子。如果我能弄清楚的话，这就是“TODO 并且它不能被 10 整除”应该限制的内容。

标签： decimal bigdecimal idris

【解决方案1】：

你可以在构造函数类型中拼出你的不变量：

data BigDecimal: Type where
     BDZ: BigDecimal
     BD: (n : Integer) -> {auto prf: Not (n `mod` 10 = 0)} -> (mag: Integer) -> BigDecimal

这里，prf 将确保 n 不能被 10 整除（这也意味着它不会等于 0），从而确保规范性：

0 的唯一表示是BDZ
n * 10^mag 的唯一表示是BD n mag： BD (n * 10) (mag - 1) 被拒绝，因为 n * 10 可以被 10 整除，并且由于 n 本身不能被 10 整除，BD (n / 10) (mag + 1) 也不起作用。

编辑：事实证明，because Integer division is non-total，Idris 并没有减少构造函数 BD 类型中的 n `mod` 10，所以即使是简单的事情，例如BD 1 3 不起作用。

这是一个新版本，它使用Natural 数字和Data.Nat.DivMod 来进行全除性测试：

-- Local Variables:
-- idris-packages: ("contrib")
-- End:

import Data.Nat.DivMod
import Data.So

%default total

hasRemainder : DivMod n q -> Bool
hasRemainder (MkDivMod quotient remainder remainderSmall) = remainder /= 0

NotDivides : (q : Nat) -> {auto prf: So (q /= 0)} -> Nat -> Type
NotDivides Z {prf = Oh} n impossible
NotDivides (S q) n = So (hasRemainder (divMod n q))

使用它，我们可以使用基于Nat 的BigDecimal 表示：

data Sign = Positive | Negative

data BigNatimal: Type where
     BNZ: BigNatimal
     BN: Sign -> (n : Nat) -> {auto prf: 10 `NotDivides` n} -> (mag: Integer) -> BigNatimal

在构造BigNatimal 值时很容易使用；例如这里是 1000：

bn : BigNatimal
bn = BN Positive 1 3

编辑 2：这里尝试将 Nats 转换为 BigNatimals。它有效，但 Idris 并没有看到 fromNat' 的全部内容。

tryDivide : (q : Nat) -> {auto prf : So (q /= 0)} -> (n : Nat) -> Either (q `NotDivides` n) (DPair _ (\n' => n' * q = n))
tryDivide Z {prf = Oh} n impossible
tryDivide (S q) n with (divMod n q)
  tryDivide _ (quot * (S q)) | MkDivMod quot Z _ = Right (quot ** Refl)
  tryDivide _ (S rem + quot * (S q)) | MkDivMod quot (S rem) _ = Left Oh

fromNat' : (n : Nat) -> {auto prf: So (n /= 0)} -> DPair BigNatimal NonZero
fromNat' Z {prf = Oh} impossible
fromNat' (S n) {prf = Oh} with (tryDivide 10 (S n))
  fromNat' (S n) | Left prf = (BN Positive (S n) {prf = prf} 1 ** ())
  fromNat' _ | Right (Z ** Refl) impossible
  fromNat' _ | Right ((S n') ** Refl) with (fromNat' (S n'))
    fromNat' _ | Right _ | (BNZ ** nonZero) = absurd nonZero
    fromNat' _ | Right _ | ((BN sign k {prf} mag) ** _) = (BN sign k {prf = prf} (mag + 1) ** ())

fromNat : Nat -> BigNatimal
fromNat Z = BNZ
fromNat (S n) = fst (fromNat' (S n))

【讨论】：

无论如何，这是一个开始的地方。谢谢