idris中BigDecimal的实现 [英] implementation of BigDecimal in idris

问题描述

我正在尝试在Idris中实现一个十进制.到目前为止，我已经知道了:

I'm trying to implement a bigdecimal in Idris. I have this so far:

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

I would like to force the restrictions marked by "TODO" above. However, I'm am just learning Idris, so I'm not even sure if this sort of restriction is a good idea or not.

通常，我正在尝试创建一种税收计算工具，该工具能够以任意精度使用多种(加密)货币进行计算.然后，我希望能够尝试并使用证明者来证明有关该程序的某些属性.

In general I'm trying to create a tax calculation tool capable of computing with multiple (crypto)currencies using arbitrary precision. I'd like to be able to then try and use the prover to prove some properties about the program.

所以，我的问题是:

• 尝试执行我指定的限制是否是一个好的设计决定?
• 是否有可能在Idris中进行这种限制?
• 这是Idris中BigDecimal的良好实现吗?

我在想类似"BD:(n:Integer)->((n = 0)= Void)->(d:Integer)-> BigDecimal nd"之类的东西，因此您必须通过一个证明那n不为零.但是我真的不知道这是否是个好主意.

I was thinking of something like "BD : (n : Integer) -> ((n = 0)=Void) -> (d : Integer) -> BigDecimal n d", so you have to pass a proof that n isn't zero. But I really don't know if this is a good idea or not.

针对仙人掌的评论，这样会更好吗?

Edit 2: In response to Cactus's comment, would this be better?

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

推荐答案

您只需在构造函数类型中拼出不变量即可:

You could just spell out your invariants in the constructor types:

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

在这里，prf将确保n不能被10整除(这也意味着它将不等于0)，从而确保正则性:

Here, prf will ensure that n is not divisible by 10 (which also means it will not be equal to 0), thereby ensuring canonicity:

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

• The only representation of 0 is BDZ
• The only representation of n * 10^mag is BD n mag: BD (n * 10) (mag - 1) is rejected because n * 10 is divisible by 10, and since n itself is not divisible by 10, BD (n / 10) (mag + 1) would not work either.

编辑:事实证明，

EDIT: It turns out, because Integer division is non-total, Idris doesn't reduce the n `mod` 10 in the type of the constructor BD, so even something as simple as e.g. BD 1 3 doesn't work.

这是一个使用Nat ural number和Data.Nat.DivMod进行总可分性测试的新版本:

Here's a new version that uses Natural numbers, and Data.Nat.DivMod, to do total divisibility testing:

-- 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表示形式:

Using this, we can use a Nat-based representation of 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:

which is easy to work with when constructing BigNatimal values; e.g. here's 1000:

bn : BigNatimal
bn = BN Positive 1 3

编辑2 :这是将Nat转换为BigNatimal的一种尝试.它可以工作，但是Idris看不到fromNat'的总数.

EDIT 2: Here's a try at converting Nats into BigNatimals. It works, but Idris doesn't see fromNat' as total.

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))

这篇关于idris中BigDecimal的实现的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！