(xs : Vect n elem) -> Vect (n * 2) elem

Question

The book Type Driven Development with Idris presents this exercise:

Define a possible method that fits the signature:

two : (xs : Vect n elem) -> Vect (n * 2) elem

I tried:

two : (xs : Vect n elem) -> Vect (n * 2) elem
two xs = xs ++ xs

But I got the following error:

*One> :r
Type checking ./One.idr
One.idr:9:5:When checking right hand side of two:
Type mismatch between
        Vect (n + n) elem (Type of xs ++ xs)
and
        Vect (mult n 2) elem (Expected type)

Specifically:
        Type mismatch between
                plus n n
        and
                mult n 2
Holes: Hw1.two

If I have a Vector of size N, and need a Vector of size N*2, then appending it to itself seems reasonable.

What am I doing wrong?

Answer 1

Short answer

Change the type signature to two : (xs : Vect n elem) -> Vect (n + n) elem.

If you really need it that way

Getting to Vect (n * 2) elem is a bit complicated. Here:

two' : Vect n elem -> Vect (n * 2) elem
two' {n} xs = rewrite multCommutative n 2 in rewrite plusZeroRightNeutral n in xs ++ xs

The reason you got that error message is that equality in typechecking is equality after reduction to normal form. n + n and mult n 2 are equal, but their normal forms aren't. (mult n 2 is what n * 2 reduces to after resolving the typeclass.)

You can see the definition of mult like so:

*kevinmeredith> :printdef mult
mult : Nat -> Nat -> Nat
mult 0 right = 0
mult (S left) right = plus right (mult left right)

It works by pattern matching on the first argument. Since the first argument in the type signature of two is n, mult can't be reduced at all. multCommutative will help us flip it around:

*kevinmeredith> :t multCommutative 
multCommutative : (left : Nat) ->
                  (right : Nat) -> left * right = right * left

Our best tool to apply that equality is rewrite, like in my definition of two'. (run :t replace at the REPL if you want to see how to do it the hard way) In the rewrite foo in bar construction, foo is something of type a = b and bar has the type of the outer expression, but with all as replaced by bs. In my two' above, I first used it to change Vect (n * 2) to Vect (2 * n). This lets mult reduce. If we look at mult above, and apply it to 2 i.e. S (S Z) and n, you get plus n (mult (S Z) n, and then plus n (plus n (mult Z n)), and then plus n (plus n Z). You don't have to work out the reduction yourself, you can just apply the rewrite and put a hole on the end:

two' : Vect n elem -> Vect (n * 2) elem
two' {n} xs = rewrite multCommutative n 2 in ?aaa

Then ask Idris:

*kevinmeredith> :t aaa
  elem : Type
  n : Nat
  xs : Vect n elem
  _rewrite_rule : plus n (plus n 0) = mult n 2
--------------------------------------
aaa : Vect (plus n (plus n 0)) elem

plus n Z doesn't reduce because plus is defined by recursion on its first argument, just like mult. plusZeroRightNeutral gets you the equality you need:

*kevinmeredith> :t plusZeroRightNeutral 
plusZeroRightNeutral : (left : Nat) -> left + 0 = left

I used the same technique with rewrite again.

:search will let you search the library for inhabitants of a given type. You'll often find someone has done the work of proving things for you.

*kevinmeredith> :s (n : Nat) -> n + 0 = n
= Prelude.Nat.multOneLeftNeutral : (right : Nat) ->
                                   fromInteger 1 * right = right


= Prelude.Nat.plusZeroRightNeutral : (left : Nat) ->
                                     left + fromInteger 0 = left


*kevinmeredith> :s (n, m : Nat) -> n * m = m * n
= Prelude.Nat.multCommutative : (left : Nat) ->
                                (right : Nat) -> left * right = right * left

(This answer is for Idris version 0.9.20.1)