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

Question

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

 split : ∀ {A mn} → 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 nmk} → (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 applyPostfix function that applies a fixed size vector function to the tail of a longer vector.

 applyPostfix ∀ {A nmk} → (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 already shown in the definition of applyPrefix , k -Argument cannot remain implicit when applyPostfix used. For instance:

 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 can remain implicit when using applyPostfix ?

What I did is check / programming:

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

and use this lemma when defining applyPostfix :

 postfixApp2 : ∀ {A}{nmk : ℕ} → (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 nk | lem-plus-comm kn | lem-plus-comm km | lem-plus-comm mk = reverse (drop {n = n} (reverse xs)) ++ f (reverse (take {n = n} (reverse xs))) 

Unfortunately, this did not help, since I use the k parameter to invoke the lemma: - (

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

Answer 1

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

The source of the problem is that a positive integer n can be unified with p + q only if p known. This is due to the fact that + is determined by induction on the first argument.

So this works (I use the standard library version of switching to + ):

 +-comm = comm where open IsCommutativeSemiring isCommutativeSemiring open IsCommutativeMonoid +-isCommutativeMonoid postfixApp2 : {A : Set} {nmk : ℕ} → (Vec A n → Vec A m) → Vec A (n + k) → Vec A (m + k) postfixApp2 {A} {n} {m} {k} f xs rewrite +-comm nk | +-comm mk = applyPostfix {k = k} f xs 

Yes, I reuse the original applyPostfix here and just give it a different type by rewriting it 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