Implicit length arguments in fixed-length vector functions in Agda

Question

I wrote an prefixApp function prefixApp that applies a vector function to a vector prefix:

 split : {A : Set}{mn : Nat} -> 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 ) prefixApp : {A : Set}{nmk : Nat} -> (Vec A n -> Vec A m) -> Vec A (n + k) -> Vec A (m + k) prefixApp f xs with split xs ... | ( ys , zs ) = f ys ++ zs 

I like the fact that prefixApp can be used without explicitly specifying a length argument, for example.

 gate : Vec Bool 4 -> Vec Bool 3 gate = prefixApp xorV 

(where xorV : Vec Bool 2 -> Vec Bool 1 - Xor-vector function)

Unfortunately, I do not know how to write a postfixApp function that can be used without an explicit length argument. The definition of my function so far is as follows:

 postfixApp : {A : Set}{nmk : Nat} -> (Vec A n -> Vec A m) -> Vec A (k + n) -> Vec A (k + m) postfixApp {_} {_} {_} {k} f xs with split {_} {_} {k} xs ... | ( ys , zs ) = ys ++ (f zs) 

It seems, however, that postfixApp always needs a length argument. For instance.

 gate : Vec Bool 4 -> Vec Bool 3 gate = postfixApp {k = 2} xorV 

Does anyone know how to eliminate this asymmetry, i.e. how to write a postfixApp function that works without an argument with an explicit length. Think I need another split function?

Answer 1

Using prefixApp you have

 prefixApp : {A : Set}{nmk : Nat} -> (Vec A n -> Vec A m) -> Vec A (n + k) -> Vec A (m + k) 

and you pass it the function Vec Bool 2 -> Vec Bool 1 , so it knows that n = 2 and m = 1 simple union. Then, since the addition is determined by recursion on the left arguments, the remainder of the type of function decreases from Vec A (2 + k) -> Vec A (1 + k) to Vec A (suc (suc k)) -> Vec A (suc k) . Then Agda can apply direct concatenation (expanding the number of literals):

 Vec A (suc (suc k)) -> Vec A (suc k) Vec Bool (suc (suc (suc (suc zero)))) -> Vec Bool (suc (suc (suc zero))) 

to conclude that k = 2 .

Looking at another:

 postfixApp : {A : Set}{nmk : Nat} -> (Vec A n -> Vec A m) -> Vec A (k + n) -> Vec A (k + m) 

The only difference is that the known values ​​that your xorV make n and m equal to 2 and 1, but this only makes the remainder of your function type in Vec A (k + 2) -> Vec A (k + 1) . This type does not decrease even more, because the addition is determined by recursion on the first argument k , which is currently unknown. Then you try to combine k + 2 with 4 and k + 1 with 3 , and Agda splashes yellow. “But clearly k = 2 ” you say! You know this because you know the mathematics and you can apply subtraction and other simple principles, but Agda does not know this. _+_ is another function, and combining applications of an arbitrary function is difficult. What if I asked you to combine (2 + x) * (2 + y) with 697 , for example? Should typechecker be expected to account for quantity and complain that there is no unique factorization? I assume that since multiplication is commutative, it usually will not, unless you restrict the parties, but should Agda know that multiplication is commutative?

In any case, Agda knows how to make unification, which basically corresponds to the "structural" values ​​to each other. Data constructors have such structural quality for them as type constructors, so they can all be unified uniquely. When it comes to something more interesting, you are faced with the problem of “higher order unification,” which cannot be resolved as a whole. Agda implements a fantastic algorithm called Miller Pattern Combination that allows it to solve some limited types of fancier-related situations, but there are some things that it simply cannot do, and your function application is one of them.

If you look in the standard library, you will find that in most cases when the type includes the addition of naturals, one of the terms (left) will usually not be implicit, unless the other argument indicates it completely (as is the case in your prefixApp ).

As for what to do with this, the problem as a whole has not been resolved. After a while, you have a sense of what Agda can output and what cannot, and then stop making unexplored arguments implicit. You can define a "symmetric" version of _+_ , but in the end it becomes equally painful for working with both sides, so I also do not recommend it.

Answer 2

Actually, you can define this function with almost one type.

 postfixApp : {A : Set}{nmk : ℕ} -> (Vec A n -> Vec A m) -> Vec A (n + k) -> Vec A (k + m) postfixApp f xs with splitAt' (reverse xs) ... | ys , zs = reverse zs ++ f (reverse ys) test-func : Vec Bool 3 -> Vec Bool 2 test-func (x1 ∷ x2 ∷ x3 ∷ []) = (x1 ∧ x2) ∷ (x2 ∨ x3) ∷ [] test : postfixApp test-func (false ∷ false ∷ true ∷ false ∷ true ∷ []) ≡ false ∷ false ∷ false ∷ true ∷ [] test = refl 

All code: http://lpaste.net/107176