3

我正在尝试通过重建（以更简单的方式）我们最近在工作中所做的一些东西来学习 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 是否遵守规则？

4

1 回答 1

3

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

||| 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 时明确证明两个任意向量的总和实际上相等。无论如何，它们等同于同一件事，但我所描述的是一种更实用的方法。

于 2014-11-30T16:52:01.597 回答