Idris中Vect的每个函数

Question

在Idris中，我试图为splitEvery编写Vect函数的类型安全（r）版本，在List上看起来像这样：

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

到目前为止，我有：

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)

它将进行类型检查并加载REPL，但是当我尝试调用它时，它将失败：

*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

因此，显然Idris看不到k的有效选择是5。使它起作用的一种方法是显式地给它提供[[implicit参数k，但这很丑陋：] >

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

所以我的问题是：有没有一种方法可以使这项工作不丑陋，或者比我到目前为止所制作的东西更惯用？

在Idris中，我试图为Vect编写一个splitEvery函数的类型安全（r）版本，在List上看起来像这样：splitEvery：Nat-> List a-> List（List a）splitEvery _ [] = [] ...

Answer 1

Idris仅出于某种原因未能在REPL中推断k的值。如果您使用