Cactus demonstrated how to address my question: Helper Function to Determine if Nat `mod` 5 == 0.
He wrote:
onlyModBy5 : (n : Nat) -> {auto prf : n `modNat` 5 = 0} -> Nat
onlyModBy5 n = n
Then, I attempted to use that function to apply onlyModBy5 to the sum of a Vect n Nat's.
foo : (n : Nat) -> Vect n Nat -> Nat
foo n xs = onlyModBy5 $ sum xs
But I got this compile-time error:
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
How can I use the above onlyModBy5 function with foo?
It depends on what you want to achieve. foo : (n : Nat) -> Vect n Nat -> Nat says that you can apply any Nat to foo, and any Vect of Nat (if the Vect is of size n) and foo will return a Nat.
First off, you don't need the explicit (n : Nat) argument. If you write just foo : Vect n Nat -> Nat, Idris would turn n internally into an implicit argument: foo : {n : Nat} -> Vect n Nat -> Nat.
In the arguments is nothing about the elements of the Vect, and therefor nothing about the sum of it. You could apply [1,2,2] as well [1,1], whereas the latter doesn't have a proof of prf : (sum [1,1]) `modNat` 5 == 0), so obviously you can't apply the sum to onlyModBy5.
You could either demand a proof of this as an argument as before:
bar : (xs : Vect n Nat) -> {auto prf : (sum xs) `modNat` 5 = 0} -> Nat
bar xs = onlyModBy5 (sum xs)
Or let it decide based on the sum:
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 decides whether two values are propositionally equal (in this case, if they are the same Nat), and either returns Yes with a (prf : n `modNat` 5 = 0) that they are equal, or No with a proof that they aren't equal. This proof can be then given to onlyModBy5 with {prf}. This extends to {prf=prf}, which gives the implicit argument the proof of Yes, as both are named prf.