splitEvery function for Vect in Idris

Question

In Idris I am trying to write a type-safe(r) version of a splitEvery function for Vect, that on Lists looks like this:

splitEvery : Nat -> List a -> List (List a)
splitEvery _ [] = []
splitEvery n xs = (take n xs) ++ splitEvery n (drop n xs)

So far I've got:

splitEvery : {k : Nat} -> (n : Nat) -> Vect (k * n) a -> Vect k (Vect n a)
splitEvery {k = Z} _ [] = []
splitEvery {k = (S j)} n xs = (take n xs) :: splitEvery {k = j} n (drop n xs)

which will type-check and load in the REPL alright, but when I try to invoke it, it will fail:

*Main> splitEvery 2 (fromList [1..10])
(input):1:1-31:When checking an application of function Main.splitEvery:
        Type mismatch between
                Vect (length (enumFromTo 1 10))
                     Integer (Type of fromList (enumFromTo 1 10))
        and
                Vect (k * 2) Integer (Expected type)

        Specifically:
                Type mismatch between
                        length (enumFromTo 1 10)
                and
                        mult k 2

So obviously Idris isn't seeing that a valid choice of k here would be 5. A way to make it work would be to explicitly give it the implicit parameter k, but that's ugly:

*Main> splitEvery {k = 5} 2 (fromList [1..10])
[[1, 2], [3, 4], [5, 6], [7, 8], [9, 10]] : Vect 5 (Vect 2 Integer)

So my question is: is there a way to make this work that isn't ugly, or is more idiomatic than what I've produced so far?

Markus Markus · Accepted Answer · 2019-11-25T09:28:01

Idris is only failing to infer the value of k in the REPL for some reason. If you amend your code with

result: Vect 5 (Vect 2 Nat)
result = splitEvery 2 (fromList [1..10])

everything typechecks - as the type is already known and k can be infered. You can achieve the same on the REPL by providing a type hint using the:

the (Vect 5 (Vect 2 Nat)) (splitEvery 2 (fromList [1..10])) works as well.

splitEvery function for Vect in Idris

1 Answers