Idris 中 Vect 的 splitEvery 函数答案

【问题标题】：splitEvery function for Vect in IdrisIdris 中 Vect 的 splitEvery 函数
【发布时间】：2019-11-23 20:55:06
【问题描述】：

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

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 dependent-type

【解决方案1】：

Idris 只是因为某种原因无法推断 REPL 中 k 的值。如果你用

修改你的代码

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

一切类型检查 - 因为类型是已知的并且可以推断出k。您可以在 REPL 上通过使用 the 提供类型提示来实现相同的目的：

the (Vect 5 (Vect 2 Nat)) (splitEvery 2 (fromList [1..10])) 也可以。

【讨论】：