idris - Concatenation of two vectors - why are lengths not treated as commutative?

Question

I'm playing around with Idris and I came across something which confuses me a little:

The following type checks:

conc : Vect n a -> Vect m a -> Vect (n+m) a
conc [] ys = ys
conc (x :: xs) ys = x :: (conc xs ys)

but this doesn't:

conc : Vect n a -> Vect m a -> Vect (m+n) a
conc [] ys = ys
conc (x :: xs) ys = x :: (conc xs ys)

with the following error:

When checking right hand side of conc with expected type
        Vect (m + 0) a

Type mismatch between
        Vect m a (Type of ys)
and
        Vect (plus m 0) a (Expected type)

Specifically:
        Type mismatch between
                m
        and
                plus m 0

Equivalently xs++ys type checks but ys++xs doesn't even though they would both match the type definition of having length n+m.

This surprises me a little as addition is commutative. Is there anything I can do (perhaps with constraints?) to the function signature to get both xs++ys and ys++xs expressions type checking?

Answer 1

This is a common topic of confusion for beginners in Idris. The problem in this case in second conc version:

conc : Vect n a -> Vect m a -> Vect (m+n) a
conc [] ys = ys

Idris cannot apply addition commutativity because Nat plus commutativity is a theorem from the compiler point of view. Here its type:

Idris> :t plusCommutative 
plusCommutative : (left : Nat) -> (right : Nat) -> left + right = right + left

There're no general rules to tell you which theorem to choose and to apply. Of course, some heuristics can be made for some simple cases, like Nat commutativity. But this also can make difficult to understand some other cases.

The other thing you need to consider is definition of plus:

Idris> :printdef plus 
plus : Nat -> Nat -> Nat
plus 0 right = right
plus (S left) right = S (plus left right)

Function plus defined in a such way that is does pattern matching on its first argument. Idris actually can perform this pattern matching in types. So in first version, where

conc : Vect n a -> Vect m a -> Vect (n+m) a
conc [] ys = ys

you have (0 + m) in type and Idris can replace plus 0 m with m and everything typechecks. plus m 0 would work if you define your + operator by pattern matching on second argument. For example, this compiles:

infixl 4 +.
(+.) : Nat -> Nat -> Nat
n +. Z = n
n +. (S m) = S (n +. m)

conc : Vect n a -> Vect m a -> Vect (m +. n) a
conc [] ys = ys
conc (x :: xs) ys = x :: (conc xs ys)

But it's obvious that writing new operator for every case you need is horrible. So to make your second version compilable you should use rewrite ... in syntax in Idris. You need next theorems:

Idris> :t plusZeroRightNeutral 
plusZeroRightNeutral : (left : Nat) -> left + 0 = left
Idris> :t plusSuccRightSucc 
plusSuccRightSucc : (left : Nat) -> (right : Nat) -> S (left + right) = left + S right
Idris> :t sym
sym : (left = right) -> right = left

And here is version which compiles:

conc : Vect n a -> Vect m a -> Vect (m + n) a
conc         {m} []        ys = rewrite plusZeroRightNeutral m        in ys
conc {n=S k} {m} (x :: xs) ys = rewrite (sym $ plusSuccRightSucc m k) in x :: (conc xs ys)

I'm not explaining here how rewriting and theorem proving works here. This is a topic of another question if you don't understand something. But you can read about that in tutorial (or wait for The Book release :) .