Понимание `к: Nat ** 5 * к = n` Подпись

Question

Следующая функция компилируется:

onlyModByFive : (n : Nat) -> (k : Nat ** 5 * k = n) -> Nat 
onlyModByFive n k = 100 

Но что k представляет с синтаксисом Nat ** 5 * k = n?

Также, как я могу назвать это? Вот что я пробовал, но я не понимаю выход.

*Test> onlyModByFive 5 5 
When checking an application of function Main.onlyModByFive: 
     (k : Nat ** plus k (plus k (plus k (plus k (plus k 0)))) = 5) is not a 
     numeric type 

источник ответа - https://groups.google.com/d/msg/idris-lang/ZPi9wCd95FY/eo3tRijGAAAJ

Answer 1

(k : Nat) ** (5 * k = n) является зависимым пара, состоящая из

• первый элемент k : Nat
• Второй элемент prf : 5 * k = n

Другими словами,это экзистенциальный тип, который гласит: «Существует k : Nat, такое, что 5 * k = n». Чтобы быть конструктивным, вы должны дать такой k и доказательство того, что оно действительно удовлетворяет 5 * k = n.

В вашем примере, если вы частично применить onlyModByFive к 5, вы получите что-то типа

onlyModModByFive 5 : ((k : Nat) ** (5 * k = 5)) -> Nat 

поэтому второй аргумент должен быть типа (k : Nat) ** (5 * k = 5). Существует только один выбор k мы можем сделать здесь, установив его в 1, и доказать, что 5 * 1 = 5:

foo : Nat 
foo = onlyModByFive 5 (1 ** Refl) 

Это работает, потому что 5 * 1 сводится к 5, поэтому мы должны доказать 5 = 5, который может быть тривиальным сделано напрямую используя Refl : a = a (унификация a ~ 5).