理解`k:Nat**5*k = 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)来完成.