Agda Type-Checking and Commutativity / Associativity of +

Question

Since the _+_-Operation for Nat is usually defined recursively in the first argument, its obviously non-trivial for the type-checker to know that i + 0 == i. However, I frequently run into this issue when I write functions on fixed-size Vectors.

One example: How can I define an Agda-function

swap : {A : Set}{m n : Nat} -> Vec A (n + m) -> Vec A (m + n)

which puts the first n values at the end of the vector?

Since a simple solution in Haskell would be

swap 0 xs     = xs
swap n (x:xs) = swap (n-1) (xs ++ [x])

I tried it analogously in Agda like this:

swap : {A : Set}{m n : Nat} -> Vec A (n + m) -> Vec A (m + n)    
swap {_} {_} {zero} xs          = xs 
swap {_} {_} {suc i} (x :: xs)  = swap {_} {_} {i} (xs ++ (x :: []))

But the type checker fails with the message (which relates to the the {zero}-case in the above swap-Definition):

.m != .m + zero of type Nat
when checking that the expression xs has type Vec .A (.m + zero)

So, my question: How to teach Agda, that m == m + zero? And how to write such a swap Function in Agda?

For what it's worth, I would not make the naturals (at least n) implicit in your signature of swap, since Agda won't be able to infer it. — copumpkin
@copumpkin: Well I could be wrong, but I thought that the type checker could infer both in some situations (depending on the context where swap is used)? — phynfo
not as far as I know. Say you have a Vec Nat (5 + 3). That addition will reduce the type immediately to Vec Nat 8, which Agda will then try to unify with Vec A (n + m) and will then throw its hands up in the air (i.e., make your term yellow) because it can't magically do subtraction. I'm reasonably sure that even with Agda's fancy Miller pattern unification, there won't be any cases where it can infer n and m from context. — copumpkin

hammar hammar · Accepted Answer · 2012-10-18T16:00:57

Teaching Agda that m == m + zero isn't too hard. For example, using the standard type for equality proofs, we can write this proof:

rightIdentity : (n : Nat) -> n + 0 == n
rightIdentity zero = refl
rightIdentity (suc n) = cong suc (rightIdentity n)

We can then tell Agda to use this proof using the rewrite keyword:

swap : {A : Set} {m n : Nat} -> Vec A (n + m) -> Vec A (m + n)    
swap {_} {m} {zero} xs rewrite rightIdentity m = xs 
swap {_} {_} {suc i} (x :: xs) = ?

However, providing the necessary proofs for the second equation is a lot more difficult. In general, it's a much better idea to try to make the structure of your computations match the structure of your types. That way, you can get away with a lot less theorem proving (or none in this case).

For example, assuming we have

drop : {A : Set} {m : Nat} -> (n : Nat) -> Vec A (n + m) -> Vec A m
take : {A : Set} {m : Nat} -> (n : Nat) -> Vec A (n + m) -> Vec A n

(both of which can be defined without any theorem proving), Agda will happily accept this definition without any fuss:

swap : {A : Set} {m n : Nat} -> Vec A (n + m) -> Vec A (m + n)
swap {_} {_} {n} xs = drop n xs ++ take n xs

Agda Type-Checking and Commutativity / Associativity of +

1 Answers