Add dependent folds in `Data.Vec.Functional`

[jacquescomeaux]

It seems like it would be nice for Vector to have the same (or as close as possible) interface as Vec. Currenly Vector has only a non-dependent foldr and foldl. It would be easy to define dependent foldr / foldl and specialize them to the non-dependent foldr' / foldl', like the way it is handled for Vec. Moreover, there are some properties, foldr-universal, foldr-fusion, etc, which are altogether missing for Vector (in dependent or non-dependent form), and would be nice to have in Data.Vec.Functional.Properties. Here's a dependent foldr for Vector:

foldr
    : {a b : Level} {A : Set a} (B : ℕ → Set b)
    → ({k : ℕ} → A → B k → B (suc k))
    → B zero
    → {n : ℕ}
    → Vector A n
    → B n
foldr _ _ e {zero} v = e
foldr B f e {suc n} v = f (head v) (foldr B f e (tail v))

The foldr-congs in Data.Vec.Functional.Relation.Binary.Pointwise.Properties and Data.Vec.Functional.Relation.Binary.Equality.Setoid could also be dependent-ized.

I wanted to make sure some changes along these lines would be welcome before starting work on a pull request. I'm realizing as I write this, though, that using the same naming scheme as Vec would be a breaking change, since all the uses of foldr would then expect an extra argument.

[JacquesCarette]

I certainly would think this would be an improvement. The naming is a problem... we can certainly use the 'right' names for v3.0, but for v2.4, we'll be stuck with something sub-optimal.

Maybe, for now, a sub-module Dependent that has the right names?

[jamesmckinna]

I'd suggest punting this to v3.0, which we can hopefully start making progress on soon?
Making these additions now, but in the 'wrong' place, with the 'wrong' names, seems like a worse maintenance headache than postponing for the time being?