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

Попытка выполнить упражнение об умножении матриц в Разработка с использованием типов с помощью 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

Я попытался выполнить все шаги с некоторыми тестовыми данными в ответе, и все сработало нормально ... Однако код отказывается проходить проверку типов


idris
person Michelrandahl    schedule 13.01.2016    source источник

Ответы (1)


arrow_upward
3
arrow_downward

length имеет тип

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

Возвращает Nat. Средство проверки типов не знает, что Nat на самом деле n, поэтому оно не может объединить оба значения. Собственно, вам даже не нужно length. В документации говорится

Примечание: это полезно только в том случае, если вы еще не знаете длину статически и хотите избежать сопоставления неявного аргумента по причинам стирания.

Поэтому вместо 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)
person xash    schedule 13.01.2016