Несоответствие типа между предполагаемым значением и длиной вектора

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:

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 

Я попытался запустить через все шаги, с некоторыми тестовыми данными в РЕПЛ и все работало нормально ... Код, однако, отказывается пройти проверки типов

Answer 1

length имеет тип

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

Он возвращает 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)