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 を構築するたびに、任意の 2 つのベクトルの合計が実際に等しいことを明示的に証明するという面倒な義務を発生させることなく、型システムによって貸方と借方の等価性が強制されるようになりました。とにかく同じことになりますが、私が説明しているのは、それを行うためのはるかに実用的な方法です。

于 2014-11-30T16:52:01.597 に答える