18

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?

3
  • 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
    Oct 19, 2012 at 3:49
  • @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
    Oct 19, 2012 at 13:14
  • 1
    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
    Oct 19, 2012 at 14:24

1 Answer 1

15

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
3
  • Thanks for your very helpful answer! It still seems strange for me, that the type of a function cuts down the set of possible ways to implement a function; or in other words: being used to program in haskell, I never took types so serious. Now, I use your suggested implementation. However, could you just sketch how to teach agda, that m == m + zero?
    – phynfo
    Oct 19, 2012 at 13:10
  • 1
    @phynfo: I already did in the first part of my answer. If you mean "without having to tell Agda when to use it", then I don't think you can. Also, I never said that it was impossible to define it your way, just that it's a lot harder to convince Agda that your implementation is correct.
    – hammar
    Oct 19, 2012 at 15:20
  • 3
    There is sort of a way to make m + zero reduce to m magically, but it's pretty advanced and you can't use a lot of the standard machinery with it. The idea is to represent your "monoidish" thing (naturals and addition, here) as a difference structure (like difference lists), so your operation becomes function composition and identity is the identity function. You then carry an irrelevant proof of the difference invariant. You can find more info here: comments.gmane.org/gmane.comp.lang.agda/3259
    – copumpkin
    Oct 19, 2012 at 15:33

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.