реализация BigDecimal в idris

Question

Я пытаюсь реализовать 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" выше. Тем не менее, я просто изучаю Идрис, поэтому я даже не уверен, что это ограничение - хорошая идея или нет.

В общем, я пытаюсь создать инструмент расчета налогов, способный вычислять несколько (крипто) валют с использованием произвольной точности. Я бы хотел, чтобы потом попытался использовать этот метод, чтобы доказать некоторые свойства программы.

Итак, мои вопросы:

• Является ли это хорошее дизайнерское решение, чтобы попытаться обеспечить соблюдение ограничений я заданные?
• Возможно ли это ограничение в Идрисе?
• Является ли это хорошей реализацией BigDecimal в Идрисе?

Edit: Я думал, что-то вроде "BD: (п: Integer) -> ((п = 0) = Void) -> (d: Integer) -> BigDecimal-й", так что вы должны доказательство того, что 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
• Единственное представление п * 10 ^маг является BD n mag: BD (n * 10) (mag - 1) отвергается, потому что n * 10 делится на 10, и так как п сам не делится на 10, BD (n/10) (mag + 1) не будет работать.

EDIT: Оказывается, because Integer division is non-total, Идрис не уменьшает n `mod` 10 в типе конструктора BD, так что даже что-то же просто, как, например, BD 1 3 не работает.

Вот новая версия, которая использует Nat Уральской цифру и 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 

EDIT 2: Вот попытка при преобразовании Nat сек в BigNatimal с. Он работает, но Идрис не видит 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))