[ 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 :)

[jamesmckinna]

Regarding your reply, something like

lappend : ∀ m n → Levels m → Levels n → Levels (m + n)
lappend zero n las lbs = lbs
lappend (suc m) n (l , las) lbs = l , lappend m n las lbs

sappend : ∀ m n {lsa lsb} → Sets m lsa → Sets n lsb → Sets (m + n) (lappend m n lsa lsb)
sappend zero    n as bs = bs
sappend (suc m) n (a , as) bs = a , sappend m n as bs


sassocʳ : ∀ 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)

sassocʳ zero    n {as = as} {bs = bs}       p = _ , p
sassocʳ (suc m) n {as = as} {bs = bs} (a , p) =
  let (x , y) = sassocʳ m n p in (a , x) , y

might do the trick, but yes, exploring the fine details might get complicated (and the Product/Product⊤ distinctions might get... annoying)

But the real intention of my comment was roughly:

• (probably desirable) can we move the definitions you want to add to the 'right' place, as Nary operations?
• (probably undesirable) and if need be, see recursive Vec definitions as specialisations of those?

Glad to offer more feedback as things progress...

[jamesmckinna]

Oh, it's like finding myself in a time-travel drama with added amnesia: see also #1880 !
Maybe this is simply my hobby-horse, and I should avoid advocating for trading simplicity/intelligibility in favour of (the cost of) abstraction.

@gallais would you like to weigh in here?

[jkopanski]

Ok, I think I can articulate better. I was confused with assoc because I thought it should return something like Product 2 ? ?. Given that it returns a binary product should it really be called an assoc?

I've opened #3119 and #3120 to have some more concrete discussion items (I wanted to do a stacked pr, hence 2 different prs, but it seems that won't work for forks).

Anyway the there is split/append and roundtrip identity proof. I've opted to define Product via the Proudct⊤ version because otherwise it becomes kind of messy, with lot of similar but slightly different cases.

However when trying to use it for Vec.Recursive the Levels are becoming an obstacle. Which I think is the point of the issue that you have linked.