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?
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)
