implementation of BigDecimal in 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

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.

So, my questions are:

Is it a good design decision to try to enforce the restrictions I have specified?
Is it possible to do this kind of restriction in Idris?
Is this a good implementation of a BigDecimal in Idris?

Edit: 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

Solution

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

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

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.

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

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

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

bn : BigNatimal
bn = BN Positive 1 3

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