Idris:强制向量和相等

Question

我正在尝试通过重建(以更简单的方式)我们最近在工作中所做的一些事情来学习 Idris。

我想要一个数据类型，它用贷方向量和借方向量对总账进行建模。我已经走到这一步了:

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

emptyGL : GL
emptyGL = MkGL [] [] Refl

但我不确定如何将记录添加到现有的 GL。

有类似的功能

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

我如何检查/强制执行新 GL 是否遵守规则？

Answer 1

我认为我处理这种情况的方法是创建一个新的数据类型来表示具有给定总值的整数向量，如下所示:

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

您可能想要定义一个附加函数以便更方便地更新 GT，但您明白了。现在，贷方和借方的相等性由类型系统强制执行，而无需在每次构造 GL 时明确证明两个任意向量的总和实际上相等。不管怎样，它们的作用是一样的，但我所描述的是一种更实用的方法。