Idris: Force vector sums to be equal

Question

I am trying to learn Idris by rebuilding (in a more simple manner) some stuff we recently did at work.

I would like to have a data type that models a general ledger with a vector of credits and a vector of debits. I have gotten this far:

data GL : Type where
MkGL : (credits : Vect n Integer) ->
       (debits : Vect m Integer) ->
       (sum credits = sum debits) ->
       GL

emptyGL : GL
emptyGL = MkGL [] [] Refl

but I am not sure how to add records to an already existing GL.

With a function like

addTransactions : GL -> (Vect j Integer) -> (Vect k Integer) -> Maybe GL

How do I check/enforce that the new GL plays by the rules?

Answer 1

I think the way I would handle this situation would be to create a new datatype to represent vectors of integers with a given total value, like so:

||| A Vector of Integers with a given sum total
data iVect : Nat -> Integer -> Type where
  iZero : iVect 0 0
  iAdd  : (x : Integer) -> iVect n y -> iVect (S n) (y + x)

data GL : Type where
  MkGL : (credits : iVect n s) ->
         (debits  : iVect m s) ->
         GL

emptyGL : GL
emptyGL = MkGL iZero iZero

You may want to define an additional function for more convenient updating of a GT but you get the idea. Now the equality of the credits and debits is enforced by the type system without creating a burdensome obligation to explicitly prove that the sums of two arbitrary vectors are in fact equal every time you want to construct a GL. They amount to the same thing anyway, but what I'm describing is a much more practical way to do it.