时间戳

首页 > 解决方案 > 伊德里斯印章的类型

types - 伊德里斯印章的类型

问题描述

我正在尝试chop在 Idris 中编写一个函数。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 n

标签： typesfunctional-programmingidrisdependent-type

解决方案

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。

推荐阅读