CODEWITHSUNDEEP
idris
user483036
user483036

Reputation:

type mismatch between inferred value and length of vector

Trying to solve the exercise about matrix multiplication in Type driven development with Idris has led me into an annoying problem.

So far I've ended up defining a set of helper functions like this:

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)

However, the typechecker complaints that there is a "Type mismatch between the inferred value and given value" in 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

why does this mismatch occur? ys is length n and I replicate n times, so I don't see the problem :/

Originally I defined my function like this:

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

but got following error:

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

I tried running through all the steps with some test data in the repl and everything worked fine... The code, however, refuses to go through the type checker

Upvotes: 1

Views: 361

Answers (1)

xash
xash

Reputation: 3722

length has the type of

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

It returns some Nat. The type checker does not know that the Nat is actually n - so it cannot unify between both values. Actually, you don't even need length. The documentation says

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.

So instead of length we can match on the implicit argument.

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)

Upvotes: 3

Related Questions