Understanding `k : Nat ** 5 * k = n` Signature

Question

The following function compiles:

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

But what does k represent with its Nat ** 5 * k = n syntax?

Also, how can I call it? Here's what I tried, but I don't understand the output.

*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

source of answer - https://groups.google.com/d/msg/idris-lang/ZPi9wCd95FY/eo3tRijGAAAJ

Cactus Cactus · Accepted Answer · 2016-04-07T02:09:21

(k : Nat) ** (5 * k = n) is a dependent pair consisting of

A first element k : Nat
A second element prf : 5 * k = n

In other words, this is an existential type that says "there exists some k : Nat such that 5 * k = n". To be constructive, you must give such a k and a proof that it indeed satisfies 5 * k = n.

In your example, if you partially apply onlyModByFive to 5, you get something of type

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

so the second argument has to be of type (k : Nat) ** (5 * k = 5). There is only one choice of k we can make here, by setting it to 1, and proving that 5 * 1 = 5:

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

This works because 5 * 1 reduces to 5, so we have to prove 5 = 5, which can be trivially done by using Refl : a = a directly (unifying a ~ 5).

Understanding `k : Nat ** 5 * k = n` Signature

1 Answers