Implicit arguments and applying a function to the tail-part of fixed-size-vectors

Question

I wrote an Agda-function applyPrefix to apply a fixed-size-vector-function to the initial part of a longer vector where the vector-sizes m, n and k may stay implicit. Here's the definition together with a helper-function split:

split : ∀ {A m n} → Vec A (n + m) → (Vec A n) × (Vec A m) 
split {_} {_} {zero}  xs        = ( [] , xs )
split {_} {_} {suc _} (x ∷ xs) with split xs 
... | ( ys , zs ) = ( (x ∷ ys) , zs )


applyPrefix : ∀ {A n m k} → (Vec A n → Vec A m) → Vec A (n + k) → Vec A (m + k)
applyPrefix f xs with split xs
... | ( ys , zs ) = f ys ++ zs

I need a symmetric function applyPostfix which applies a fixed-size-vector-function to the tail-part of a longer vector.

applyPostfix ∀ {A n m k} → (Vec A n → Vec A m) → Vec A (k + n) → Vec A (k + m)
applyPostfix {k = k} f xs with split {_} {_} {k} xs
... | ( ys , zs ) = ys ++ (f zs)

As the definition of applyPrefix already shows, the k-Argument cannot stay implicit when applyPostfix is used. For example:

change2 : {A : Set} → Vec A 2 → Vec A 2
change2 ( x ∷ y ∷ [] ) = (y ∷ x ∷ [] )

changeNpre : {A : Set}{n : ℕ} → Vec A (2 + n) → Vec A (2 + n)
changeNpre = applyPrefix change2

changeNpost : {A : Set}{n : ℕ} → Vec A (n + 2) → Vec A (n + 2)
changeNpost = applyPost change2 -- does not work; n has to be provided

Does anyone know a technique, how to implement applyPostfix so that the k-argument may stay implicit when using applyPostfix?

What I did is proofing / programming:

lem-plus-comm : (n m : ℕ) → (n + m) ≡ (m + n)

and use that lemma when defining applyPostfix:

postfixApp2 : ∀ {A}{n m k : ℕ} → (Vec A n → Vec A m) → Vec A (k + n) → Vec A (k + m)
postfixApp2 {A} {n} {m} {k} f xs rewrite lem-plus-comm n k | lem-plus-comm k n |     lem-plus-comm k m | lem-plus-comm m k = reverse (drop {n = n} (reverse xs))  ++ f (reverse (take {n = n} (reverse xs)))

Unfortunately, this didnt help, since I use the k-Parameter for calling the lemma :-(

Any better ideas how to avoid k to be explicit? Maybe I should use a snoc-View on Vectors?

Answer 1

What you can do is to give postfixApp2 the same type as applyPrefix.

The source of the problem is that a natural number n can be unified with p + q only if p is known. This is because + is defined via induction on the first argument.

So this one works (I'm using the standard-library version of commutativity on +):

+-comm = comm
  where
    open IsCommutativeSemiring isCommutativeSemiring
    open IsCommutativeMonoid +-isCommutativeMonoid

postfixApp2 : {A : Set} {n m k : ℕ}
            → (Vec A n → Vec A m)
            → Vec A (n + k) → Vec A (m + k)
postfixApp2 {A} {n} {m} {k} f xs rewrite +-comm n k | +-comm m k =
  applyPostfix {k = k} f xs

Yes, I'm reusing the original applyPostfix here and just give it a different type by rewriting twice.

And testing:

changeNpost : {A : Set} {n : ℕ} → Vec A (2 + n) → Vec A (2 + n)
changeNpost = postfixApp2 change2

test : changeNpost (1 ∷ 2 ∷ 3 ∷ 4 ∷ []) ≡ 1 ∷ 2 ∷ 4 ∷ 3 ∷ []
test = refl