[Add] takeNat for Vec in Data.Vec.Base

[e-mniang]

The current take in Data.Vec.Base is defined as:

take : ∀ m {n} → Vec A (m + n) → Vec A m
take m xs = proj₁ (splitAt m xs)

This is a useful total function, but it requires that the input vector has exactly m + n elements. While this is type-safe, it makes many natural theorems difficult or verbose to express—especially when working with partial takes on vectors of unknown or unrestricted size.

For example, the following becomes difficult, requiring rewrites and equalities just to satisfy the type of take:

take-++-more : ∀ {A : Set} {m n k : ℕ} → (xs : Vec A m) → (ys : Vec A n) → (p : ℕ) → (m≤p : m ≤ p) → (m+n≡p+k∸n : m + n ≡ p + (n ∸ k)) →  (n≡k+n-k : n ≡ k + (n ∸ k)) → 
 toList (Data.Vec.Base.take p (cast m+n≡p+k∸n (xs Data.Vec.Base.++ ys))) ≡ toList (xs Data.Vec.Base.++  (Data.Vec.Base.take k (cast n≡k+n-k ys)))

So, maybe we could add a less restrictive version of take, named takeNat, defined as:

takeNat : ∀ {A : Set} {m : ℕ} → (k : ℕ) → Vec A m → Vec A (k ⊓ m)
takeNat zero     xs        = []
takeNat (suc k)  []        = []
takeNat (suc k)  (x ∷ xs)  = x ∷ takeNat k xs

This definition behaves like List.take, and avoids the need for index coercion or auxiliary equalities.
With takeNat, the same lemma becomes:

takeNat-++-more : ∀ {A : Set} {m n : ℕ} → (xs : Vec A m) → (ys : Vec A n) → (p : ℕ) → m ≤ p
                  → toList (takeNat p (xs Data.Vec.Base.++ ys)) ≡ toList (xs Data.Vec.Base.++ takeNat (p ∸ m) ys)

---

Feedback on this suggestion, definition, naming, and placement is welcome.

[jamesmckinna]

IIRC, there is an extended discussion of splitAt in an earlier issue/PR... in the context of view-based programming... which I'll need to hunt down before posting more. Shoutouts to @Taneb @gallais and @JacquesCarette who were also involved...

... see #2057

[jamesmckinna]

Regarding your example (pre- the fix via takeNat):

• your preconditions amount to: m ≤ p which you have, and the conditions on k to k ≤ n, from which n ≡ k + (n ∸ k) is then provable...
• so, restating them in a more symmetric form, you have m + n ≡ p + k, which can then be used by cast to coerce a (type-correct) xs Vec.++ ys into one of length p + k from which you may then take p elements... (UPDATED to clarify: I've flipped k and n ∸ k from your example, which two enjoy an 'obvious' symmetry, in order to draw out what I think is going on in your version... but happy to be corrected if I've misunderstood something there, but notice that in this symmetric reformulation, there's no prior commitment to m ≤ p, or otherwise...)

Post- the fix via takeNat, I would worry about what reasoning is needed to correctly operate on one of the form Vec (k ⊓ m) (green slime re-appears!)?

In each case, the fact that the example is phrased in terms of toList moreover suggests, to me at least, that really, if you do want to deal with vectors of indeterminate length, then maybe List is in fact a better API?

One of the not-yet-concluded discussion points of #2057 was that some form of cast coercion seemed inevitable with (lots of) Vec operations which pass their lengths around in 'green slime'-y ways, and your proposed solution seems to generate... more of the same?

Interested to hear others' take on this; the views above are my own alone.

[e-mniang]

@jamesmckinna I totally see what you mean — the example is far from being the most efficient way to do that proof.
It's more of a background to explain what sparked the idea of takeNat, i.e., whether there could be a way to use take without having to rewrite the vector as (m + n), as required by the current definition. Of course, if it doesn’t bring any real improvement — or even makes the use of take more complicated than necessary — it might be better to revisit take-++-more using the restating of the symmetries you suggested.

[jamesmckinna]

I'm all for 'think out loud' experiments to stimulate discussion ahead of possible PRs... so good to have done so! As I wrote, #2057 doesn't resolve things one way or the other, but tends towards 'cast considered annoying but hard-to-avoid' ... but there's always space for fresh thinking on these tricky topics.

[e-mniang]

Thanks a lot for the thoughtful response! I completely agree that experiments like this are most useful when they provoke discussion and fresh thinking, even if they don’t lead to a PR.
I see what you mean about the 'green slime' creeping back in, even with takeNat, some of the coercion pain just shifts around rather than disappearing.
I’ll keep digging into #2057 and the view-based discussions you mentioned.

[jamesmckinna]

Shall we close this now @e-mniang and redirect back to #2057 ? Feel free to re-open if you think otherwise!