推断值和向量长度之间的类型不匹配

Question

试图解决 Type driven development with Idris 中关于矩阵乘法的练习让我陷入了一个恼人的问题。

到目前为止，我已经定义了一组像这样的辅助函数：

morexs : (n : Nat) -> Vect m a -> Vect n (Vect m a)
morexs n xs = replicate n xs

mult_cols : Num a => Vect m (Vect n a) -> Vect m (Vect n a) -> Vect m (Vect n a)
mult_cols xs ys = zipWith (zipWith (*)) xs ys

mult_mat_helper : Num a => Vect m a -> Vect n (Vect m a) -> Vect n a
mult_mat_helper xs ys =
    let len = the Nat (length ys) in
    map sum (mult_cols (morexs len xs) ys)

但是，类型检查器抱怨 replicate (length ys) xs 中有一个 "Type mismatch between the inferred value and given value":

When checking right hand side of mult_mat_helper with expected type
        Vect n a

When checking argument n to function Main.morexs:
        Type mismatch between
                n (Inferred value)
        and
                len (Given value)

        Specifically:
                Type mismatch between
                        n
                and
                        length ys

为什么会出现这种不匹配？ ys 是长度 n 并且我复制了 n 次，所以我没看到问题：/

最初我这样定义我的函数：

mult_mat_helper : Num a => Vect m a -> Vect n (Vect m a) -> Vect n a
mult_mat_helper xs ys =
    let
        xs2 = replicate (length ys) xs
        zs = zipWith (zipWith (*)) xs2 ys
    in
    map sum zs

但出现以下错误：

When checking right hand side of mult_mat_helper with expected type
        Vect n a

When checking argument m to function Prelude.Functor.map:
        a is not a numeric type

我尝试运行通过 repl 中的一些测试数据完成所有步骤，一切正常......然而，代码拒绝通过类型检查器

Answer 1

length 的类型为

Data.Vect.length : Vect n a -> Nat

它returns一些Nat。类型检查器不知道 Nat 实际上是 n - 因此它无法统一两个值。实际上，你甚至不需要 length。文档说

Note: this is only useful if you don't already statically know the length and you want to avoid matching the implicit argument for erasure reasons.

所以我们可以匹配隐式参数而不是 length。

mult_mat_helper : Num a => Vect m a -> Vect n (Vect m a) -> Vect n a
mult_mat_helper {n} xs ys = map sum (mult_cols (morexs n xs) ys)

推断值和向量长度之间的类型不匹配

type mismatch between inferred value and length of vector

idris