Определите, делится ли сумма Vect n Nat равномерно на 5?

Cactus продемонстрировал, как ответить на мой вопрос: Вспомогательная функция для определения, если Nat` mod` 5 == 0.

Он написал:

onlyModBy5 : (n : Nat) -> {auto prf : n `modNat` 5 = 0} -> Nat
onlyModBy5 n = n

Затем я попытался использовать эту функцию, чтобы применить onlyModBy5 к сумме Vect n Nat.

foo : (n : Nat) -> Vect n Nat -> Nat
foo n xs = onlyModBy5 $ sum xs

Но я получил эту ошибку времени компиляции:

When checking right hand side of foo with expected type
        Nat

When checking argument prf to function Main.onlyModBy5:
        Can't find a value of type 
                Prelude.Nat.modNatNZ, mod' (foldrImpl (\meth =>
                                                         \meth =>
                                                           plus meth meth)
                                                      0
                                                      id
                                                      xs)
                                           4
                                           SIsNotZ
                                           (foldrImpl (\meth =>
                                                         \meth =>
                                                           plus meth meth)
                                                      0
                                                      id
                                                      xs)
                                           (foldrImpl (\meth =>
                                                         \meth =>
                                                           plus meth meth)
                                                      0
                                                      id
                                                      xs)
                                           4 =
                0
Holes: Main.foo

Как я могу использовать указанную выше функцию onlyModBy5 с foo?


idris
person Kevin Meredith    schedule 12.04.2016    source источник

Ответы (1)


arrow_upward
2
arrow_downward

Это зависит от того, чего вы хотите достичь. foo : (n : Nat) -> Vect n Nat -> Nat говорит, что вы можете применить любой Nat к foo и любой Vect из Nat (если Vect имеет размер n), и foo вернет Nat.

Во-первых, вам не нужен явный аргумент (n : Nat). Если вы напишете просто foo : Vect n Nat -> Nat, Идрис внутренне превратит n в неявный аргумент: foo : {n : Nat} -> Vect n Nat -> Nat.

В аргументах ничего не говорится об элементах Vect, и поэтому ничего о sum этого. Вы можете применить [1,2,2] также [1,1], в то время как последний не имеет доказательства prf : (sum [1,1]) `modNat` 5 == 0), поэтому очевидно, что вы не можете применить сумму к onlyModBy5.

Вы можете потребовать доказательства этого в качестве аргумента, как и раньше:

bar : (xs : Vect n Nat) -> {auto prf : (sum xs) `modNat` 5 = 0} -> Nat
bar xs = onlyModBy5 (sum xs)

Или пусть решит исходя из суммы:

foo : Vect n Nat -> Maybe Nat
foo xs = foo' (sum xs)
  where
    foo' : Nat -> Maybe Nat
    foo' k with (decEq (k `modNat` 5) 0)
      | Yes prf = Just (onlyModBy5 k {prf})
      | No _ = Nothing

decEq решает, равны ли два значения (в данном случае, если они одинаковые Nat), и либо возвращает Yes с (prf : n `modNat` 5 = 0), что они равны, либо No с доказательством того, что они не равны. Это доказательство может быть затем передано onlyModBy5 с {prf}. Это распространяется на {prf=prf}, что дает неявному аргументу доказательство Yes, поскольку оба названы prf.

person xash    schedule 12.04.2016
comment
Я думаю, вы могли бы немного улучшить foo, явно передав prf в onlyModBy5 k, чтобы подчеркнуть тот факт, что доказательство исходит именно отсюда. - person Cactus; 13.04.2016