您可以在构造函数类型中明确说明不变量:
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
这样简单的东西也行不通。
这是一个使用Nat
ural数字和Data.Nat.DivMod
进行完全可除性测试的新版本:
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))