Функция для определения деления Nat на 5 во время компиляции

Question

Используя полезный ответ Cactus, я попытался написать функцию, которая, учитывая Nat, вернем что Nat если это делится на 5,

onlyModBy5Helper : (n : Nat) -> (k : Nat ** k `mod` 5 = 0) -> Nat
onlyModBy5Helper n k = n

И тогда основная функция:

onlyModBy5 : Nat
onlyModBy5 = onlyModBy5Helper 10 (10 ** Refl)

Однако это не удалось с ошибкой во время компиляции:

When checking right hand side of onlyModBy5 with expected type
        Nat
When checking argument pf to constructor Builtins.MkDPair:
        Type mismatch between
                0 = 0 (Type of Refl)
        and
                (\k =>
                   Prelude.Nat.Nat implementation of Prelude.Interfaces.Integral, method mod k
                                                                                             5 =
                   0) 10 (Expected type)

        Specifically:
                Type mismatch between
                        0
                and
                        Prelude.Nat.Nat implementation of Prelude.Interfaces.Integral, method mod 10
                                                                                                  5

Что я делаю неправильно?

Answer 1

Этот случай немного странный: Integral реализация Nat является:

partial
Integral Nat where
  div = divNat
  mod = modNat

И если вы используете modNat вместо mod в вашей подписи типа, это работает. У объединителя типов все еще есть некоторые проблемы. Я думаю, что это не разрешает дальше, потому что это видит реализацию как частичную, а не как полную.

Тем не менее, ваш onlyModBy5Helper не совсем то, что вы пытаетесь достичь, как onlyModBy5Helper 4 (10 ** Refl) вернется 4, как n а также k зависимой пары не должно быть одинаковым значением. Эта функция, которая занимает n : Nat и доказательство для n, это, вероятно, то, что вы хотите:

onlyModBy5Helper : (n : Nat) -> n `modNat` 5 = 0 -> Nat
onlyModBy5Helper n prf = n

Обратите внимание, что это похоже на зависимую пару, и вы могли бы (но не должны, так как она добавляет ненужную абстракцию) написать функцию как:

onlyModBy5Helper : (n : Nat ** n `modNat` 5 = 0) -> Nat
onlyModBy5Helper pair = fst pair