BigDecimal 在 idris 中的实现

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，所以我什至不确定这种限制是否是个好主意。

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

那么，我的问题是：

尝试执行我指定的限制是否是一个好的设计决定？
是否可以在 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

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

编辑：事实证明，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))

BigDecimal 在 idris 中的实现

implementation of BigDecimal in idris

decimal

bigdecimal

idris