Идрис: заставить векторные суммы быть равными

Я пытаюсь изучить Идрис, перестраивая (более простым способом) некоторые вещи, которые мы недавно делали на работе.

Я хотел бы иметь тип данных, который моделирует главную книгу с вектором кредитов и вектором дебетов. Я зашел так далеко:

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 играл по правилам?


idris
person MightyMoose    schedule 30.11.2014    source источник
comment
Посмотрите на модуль prelude/Decidable/Equality. Он содержит разрешимое равенство для Nats. Сопоставление с образцом на decEq (sum credits) (sum debits) дает вам либо доказательство sum credits = sum debits (назовем его equal_sums), чтобы вы могли вернуть Just (MkGl credits debits equal_sums), либо доказательство неравенства сумм, чтобы вы могли вернуть Nothing.   -  person user3237465    schedule 01.12.2014
comment
Спасибо! Это сработало отлично!   -  person MightyMoose    schedule 01.12.2014

Ответы (1)


arrow_upward
3
arrow_downward

Я думаю, что способ, которым я справился бы с этой ситуацией, состоял бы в том, чтобы создать новый тип данных для представления векторов целых чисел с заданным общим значением, например так:

||| 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. В любом случае это одно и то же, но я описываю гораздо более практичный способ сделать это.

person Cliff Harvey    schedule 30.11.2014
comment
Это очень зависит от того, как вы его используете. Во-первых, в стандартной библиотеке нет модуля iVect, поэтому вам нужно будет написать его самостоятельно. Во-вторых, когда компилятору известна длина вектора xs, sum xs сокращается до (x1 + (x2 + ...)), т.е. нет разницы между двумя представлениями для компилятора, поэтому доказательство будет просто Refl. В-третьих, вам все равно придется явно доказывать, что, например, [n, m] и [m, n] имеют одинаковую сумму. - person user3237465; 01.12.2014