Idris型印章
Idris型印章
提问于 2019-02-13 23:11:35
我试图用Idris编写一个chop函数。Haskell等价物看起来像：
chop :: Int -> [t] -> [[t]]
chop n [] = []
chop n v = take n v : chop n (drop n v)我在Idris的最初尝试看上去如下：
chop : (n : Nat) -> Vect (k * n) a -> Vect k (Vect n a)
chop n Nil = Nil
chop n v = (take n v) :: (chop n (drop n v))类型检查错误：
Type mismatch between
Vect 0 a (Type of [])
and
Vect (mult k n) a (Expected type)
Specifically:
Type mismatch between
0
and
mult k nStack Overflow用户
回答已采纳
发布于 2019-02-14 01:31:10
k仍然可以设置为参数，即chop {k=3} Z []将导致[[], [], []] : Vect 3 (Vect Z a)。您的实现将返回chop n Nil = []，因此Idris的类型系统会正确地发出抱怨。:-)
你需要考虑一下k
chop : (n : Nat) -> Vect (k * n) a -> Vect k (Vect n a)
chop {k} n v = ?hole如果您想要实际的实现，下面是一个扰流器：
这和你的很相似。因为
mult在第一个参数上递归(在本例中是k)，所以chop的递归也应该遵循k：chop {k = Z} n v = []chop {k = (S k)} n v = take n v :: chop n (drop n v)
另一种方法是指定需要多少块，而不是每个块有多大。
chop' : (k : Nat) -> Vect (k * n) a -> Vect k (Vect n a)
chop' Z v = []
chop' {n} (S k) v = take n v :: chop k (drop n v)n需要在作用域内调用take和drop。
页面原文内容由Stack Overflow提供。腾讯云小微IT领域专用引擎提供翻译支持
原文链接：
https://stackoverflow.com/questions/54680863
复制相关文章
相似问题
腾讯云开发者
