在Idris中实现BigDecimal

Question

我正在尝试在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，所以我甚至不确定这种限制是否是一个好主意。

总的来说，我试图创建一个能够使用任意精度计算多（加密）货币的税务计算工具。我想尝试使用证明器来证明程序的某些属性。

因此，我的问题是：

1. 尝试强制执行我指定的限制是否是一个好的设计决策？ 2. 在Idris中是否可能进行这种类型的限制？ 3. 这是Idris中BigDecimal的一个好实现吗？

编辑：我在考虑类似于“BD：（n：Integer） ->（n = 0）= Void） ->（d：Integer）-＆gt; BigDecimal n d”这样的东西，所以您必须传递一个证明n不为零的证明。但我真的不知道这是一个好主意还是不是。

编辑2：针对Cactus的评论，这个方案是否更好？

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

- redfish64

---

通常，BigDecimals由一个BigInteger（用于未缩放值的数字）和一个标度或指数组成，指示小数点应该在哪里（这也可以是负值，因此您也可以表示非常大的值）。不幸的是，我不知道Idris，所以我无法告诉您如何在该语言中实现。您提出的分子的想法更像是BigFraction或BigRational。在我看来，这会使事情变得有些复杂。 - Rudy Velthuis

实际上我正在使用你所说的相同想法。我可能不应该称其为分子，但我在想（分子）/（10 **（分母指数））。 - redfish64

然后命名确实很奇怪。你的分子是我指的未缩放值，而你的分母指数是比例尺。因此，值1.000表示为未缩放值1000和比例尺3。在加法或减法时，请确保适当地缩放上下文，并在乘法或除法时调整比例尺。此外，如果进行除法运算，请将分子按所需精度放大并正确舍入结果。例如，使用精度为10，将分子乘以10 ** 10，然后再除以分母，否则1/10可能会导致结果为0而不是0.1000000000。 - Rudy Velthuis

你目前的设计意味着每个数字都由单独的单例类型表示 - 我认为这不是你想要的。为什么你把分子和幅度作为索引？ - Cactus

@"Rudy Velthuis" 的意思是让 1000 不是有效的分子。这就是“TODO，它不能被10整除”所限制的，如果我能弄清楚的话。 - redfish64

Answer 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）也不起作用。

编辑：事实证明，由于整数除法是非总的，因此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：这里尝试将Nat转换为BigNatimal。它可以工作，但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))

- Cactus

---

那是一个开始的地方。谢谢。 - redfish64