Implicit length arguments in fixed-length-vector-functions in Agda

Question

I wrote an Agda-function prefixApp which applies a Vector-Function to a prefix of a vector:

split : {A : Set}{m n : 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}{n m k : 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 providing a length argument, e.g.

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

(where xorV : Vec Bool 2 -> Vec Bool 1 is the Vector-Xor-Function)

Unfortunately, I dont know how to write a postfixApp-function which can be used without explicitly providing a length argument. My function definition so far looks like this:

postfixApp : {A : Set}{n m k : 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. E.g.

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 function postfixApp which works without an explicit length argument. I guess, I need another split-function?

Answer 1

With your prefixApp, you have

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

and you pass it a function Vec Bool 2 -> Vec Bool 1, so it knows that n = 2 and m = 1 by simple unification. Then, because addition is defined by recursion on the left arguments, the remainder of the function type reduces from Vec A (2 + k) -> Vec A (1 + k) to Vec A (suc (suc k)) -> Vec A (suc k). Agda can then apply straight-up unification (expanding the number literals) of:

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

to infer that k = 2.

Looking at the other one:

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

The only difference is that the known quantities that your xorV forces n and m to be 2 and 1, but this only makes the remainder of your function type into Vec A (k + 2) -> Vec A (k + 1). This type does not reduce further, because addition is defined by recursion on the first argument, k, which is unknown at this point. You then try to unify k + 2 with 4 and k + 1 with 3, and Agda spits out yellow. "But clearly k = 2," you say! You know that because you know math, and can apply subtraction and other simple principles, but Agda does not know that. _+_ is just another function to it, and unifying arbitrary function applications is hard. What if I asked you to unify (2 + x) * (2 + y) with 697, for example? Should the typechecker be expected to factor the number and complain that there isn't a unique factorization? I guess since multiplication is commutative there generally won't be unless you restrict the sides, but should Agda know that multiplication is commutative?

Anyway, so Agda only knows how to do unification, which basically matches "structural" quantities to each other. Data constructors have this structural quality to them, as do type constructors, so those can all be unified unambiguously. When it comes to anything fancier than that, you run into the "higher-order unification" problem, which can't be solved in general. Agda implements a fancy algorithm called Miller pattern unification, that lets it solve some restricted sorts of fancier situations, but there are some things it just can't do, and your kind of function application is one of them.

If you look in the standard library, you'll find that most cases in which a type involves an addition of naturals, one of the addends (the left one) will generally not be implicit, unless another argument specifies it completely (as is the case in your prefixApp).

As far as what to do about it, there isn't much to tackle the problem in general. After a while, you develop a sense for what Agda can infer and what it can't, and then stop making the uninferrable arguments implicit. You can define a "symmetric" version of _+_, but it ends up just being equally painful to work with both sides of it, so I don't recommend that either.

Answer 2

Actually, it's possible to define this function with almost the same type.

postfixApp : {A : Set}{n m k : ℕ} -> (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

The whole code: http://lpaste.net/107176