在 Idris2 中转置具有依赖类型的向量矩阵

Question

我很难弄清楚我的 Idris2 类型或编译错误是关于什么的，所以我想我可以请一些 Idris2 退伍军人或爱好者给我一些解释，说明如何使我的方法发挥作用，或者为什么它不能那样发挥作用。 任何额外的信息和深入的建议总是受到高度赞赏，因为我想利用这些知识将东西从 Haskell 转换为 Idris2 以获得可证明的结构等。

我已经知道的通用解决方案是这个（带有所有辅助函数）：

data Vect : (len : Nat) -> (a : Type) -> Type where
  Nil  : Vect 0 a
  (::) : (x : a) -> (xs : Vect n a) -> Vect (S n) a

zipWith : (a -> b -> c) -> Vect n a -> Vect n b -> Vect n c
zipWith f []        []         = []
zipWith f (x :: xs) (y :: ys)  = f x y :: zipWith f xs ys


replicate : (n : Nat) -> a -> Vect n a
replicate 0     _  = []
replicate (S k) va = va :: replicate k va

replicate' : {n : _} -> a -> Vect n a
replicate' = replicate n


transpose : {m : _} -> Vect n (Vect m a) -> Vect m (Vect n a)
transpose [] = replicate' []
transpose (xs::xss) = zipWith (::) xs (transpose xss)

这是我正在学习的 GitHub 指南中的解决方案。

现在我的方法：

transLines : Vect n (Vect (S m) a) -> Vect n a
transLines [] = []
transLines ((x :: _) :: xss) = x :: transLines xss

dropLines : Vect n (Vect (S m) a) -> Vect n (Vect m a)
dropLines [] = []
dropLines ((_ :: xs) :: xss) = xs :: dropLines xss


transpose' : {m : _} -> Vect n (Vect m a) -> Vect m (Vect n a)
transpose' {m = 0} [] = []
transpose' ([]:: _) = []
transpose' ma = (transLines ma) :: transpose' (dropLines ma)

我知道具体什么不起作用，当我在转置函数中调用“droplines ma”时，“Vect n (Vect m a)”和“Vect ?n (Vect (S ?m) a)”中的类型无法匹配，但是这就是我陷入困境的地方，我不知道是否可以更改某些定义以使其起作用，或者整个方法是否不适用于依赖类型。

提前感谢您并干杯

Answer 1

如果你的模式匹配正确，你的方法就可以正常工作：

transpose' : {m : _} -> Vect n (Vect m a) -> Vect m (Vect n a)
transpose' {m = 0} ma = []
transpose' {m = S m'} ma = (transLines ma) :: transpose' (dropLines ma)