[ add ] Data.Vec.Recursive.Relation.Binary.Pointwise

[jkopanski]

Recently I've came across Data.Vec.Recursive which seemed interesting enough for me to play with it. However there is lackluster support for it. So I thought this would be some grunt work that I could contribute to the library. Everything here is pretty mechanical translation from
Data.Vec.Relation.Binary.Pointwise.Inductive with only splitAt being included for completeness. I couldn't get append because of the indices _+ 0. Perhaps when I add cast next this would budge.

[jamesmckinna]

In lieu of an actual review, two quick observations

• [ add ] Pointwise lifting of algebra to Data.Vec.Functional #3077 and its antecedents are 'really' about reframing (algebraic structure on) Data.Vec.Functional as special cases of 'pointwise' constructions/properties on I → A for the index set I = Fin n
• similarly, here, should we understand Data.Vec.Recursive as special cases of Function.Nary.NonDependent.Base where the types are 'all the same'?

Eg. splitAt could be seen to 'really' be about special instances of (order-preserving) associativity isomorphisms relating A₁ × ... × Aₘ₊ₙ and (A₁ × ... × Aₘ) × (Aₘ₊₁ × ... × Aₘ₊ₙ), and perhaps better for the library if it were analysed at that level of generality?

I think there is a reason that Data.Vec.Functional and Data.Vec.Recursive are relatively underdeveloped compared to the inductively defined Data.Vec.Base.Vec, over and above the ambient stdlib design principle that we don't needlessly multiply equivalent representations of the same concept.

[jkopanski]

Indeed I've found Data.Product.Nary.NonDependent.HomoProduct which seems to be the recursive Vec (module levels). Just to be clear what you are saying is redefining recursive vec like:

infix 8 _^_
_^_ : Set a → (n : ℕ) → Set (lconst n a)
A ^ n = HomoProduct n A

and all the operations with more generic ones from the Product.Nary, like:

lookup : ∀ {n} → A ^ n → (k : Fin n) → Projₙ _ k
lookup {n = n} as k = projₙ n k as

?

If that is the case I followed your suggestion and try to tackle the assoc but It seems I'm failing at the very first step of even stating the type of it:

assocʳ : ∀ m n {lsa lsb} {as : Sets m lsa} {bs : Sets n lsb} →
        Product (m + n) (sappend m n as bs) → {!(Product m as) × (Product n bs)!}

the _×_ doesn't really work here for m ≡ 0, for example.

Anyway it seems I should define all the different functions for Sets/Levels accordingly.

btw. There is really no other point to this comment just that: "I'm looking into what you have said" and it's probably gonna take a while :)