Deprecating `Data.Table` in favour of `Data.Vec.Functional`

[MatthewDaggitt]

@gallais if you get to use James' blog post to argue for adding Reflects into the library, I'm going to use it to argue for fixing Data.Table 😝

I share @james's opinion that the record structure doesn't add anything for inference. Furthermore it's fairy difficult to work with. I've tried twice now to integrate into my own library and failed because:

• it makes it makes it very difficult to define recursive functions over it because you have to keep removing and adding the record constructor.
• it makes it much more difficult to compose them together to define matrices as again the record constructor gets in the way.

I propose leaving Data.Table in place, deprecating it, and add the non-record version as Data.Vec.Functional

[gallais]

I agree that insisting on making Table a record was a mistake on my part.
As james highlights, it would have made sense for a dependent function space
but the current definition is just needlessly painful to work with.

[laMudri]

I'd be happy to work on Data.Vec.Functional before AIM. For backwards compatibility, it might make sense to reimplement all of the definitions in the Data.Table hierarchy to just unwrap/wrap all Tables and then call stuff from Data.Vec.Functional. Minor matters: what should the type be called? Table? Vec? Something else?

[MatthewDaggitt]

I'd be happy to work on Data.Vec.Functional before AIM

That'd be great, thanks!

For backwards compatibility, it might make sense to reimplement all of the definitions in the Data.Table hierarchy to just unwrap/wrap all Tables and then call stuff from Data.Vec.Functional

Hmm I'm not sure about that. The idea with backwards compatibility is not to change any observable behaviour. The problem with reimplementing Data.Table in terms of the new Data.Vec.Functional is that it'll probably change the reduction behaviour. To be honest I'd just leave Data.Table as is and slap a deprecated warning on it.

Minor matters: what should the type be called? Table? Vec? Something else?

I've gone off Table. How about Vector as i) it distinguishes it from Vec and ii) I like Matrix better than Mat. Open to other suggestions though?

[laMudri]

Initial issues: though it's nice to define Matrix A m n as Vector (Vector A n) m, when you get to pointwise lifting of relations, a record wrapper does help with inference. So we (might) want this definition:

record Pointwise (R : REL A B ℓ) (u : Vector A n) (v : Vector B n) : Set ℓ where
  constructor mk
  field get : ∀ i → R (u i) (v i)
open Pointwise public

But with this, lifting relations pointwise over Matrix by using this Pointwise twice becomes annoying.

Something I've been considering is introducing this definition.

Indexed : ∀ {i u} {I : Set i} (U : I → Set u) {a} (A : Set a) → I → Set _
Indexed U A i = U i → A

For Vector, U = Fin, and for Matrix, U (m , n) = Fin m × Fin n. It feels a bit like containers, but with only one shape (avoiding lots of tt , [...] and [...] .proj₂), and more focus on I (the dimensions). The intention is that U is injective to make things work out. I haven't tried this out yet, though.

[MatthewDaggitt]

Initial issues: though it's nice to define Matrix A m n as Vector (Vector A n) m, when you get to pointwise lifting of relations, a record wrapper does help with inference.

Really, that's disappointing... Can you give an example? I've got quite a full set of definitions in my library: Pointwise, Equality, DecEquality etc. and for matrices Pointwise, and I don't remember anywhere where inference fell down unexpectedy.

I'd definitely prefer to avoid introducing records if at all possible, for exactly the reason that it makes lifting to matrices unpleasant. If the price to pay is that we need to include a couple of arguments explicitly then I think I'd be happy to pay it.

[laMudri]

To be honest, the only library definition I tripped up on was ++⁺.

++⁺ : ∀ {xs ys xs′ ys′} →
      Pointwise {n = m} R xs ys → Pointwise {n = n} R xs′ ys′ →
      Pointwise R (xs ++ xs′) (ys ++ ys′)

R could be given explicitly to this, so maybe that's the way to go.

[wenkokke]

I've gone off Table. How about Vector as i) it distinguishes it from Vec and ii) I like Matrix better than Mat. Open to other suggestions though?

If we're calling this Vector, why not put the code in Data.Vector? With Data.Vec.Functional the module names get really long.

[MatthewDaggitt]

We did have a very similar conversation recently (#805 (comment)) about where to put Kleene lists. The general consensus seemed to be to group isomorphic types together under one folder.

To aid discovery, I plan to add references to other implementations in the top level files, e.g. Data.Vec will have a comment pointing to the existence of Data.Vec.Functional. I agree that long modules names are still kind of problem though. What do people feel about Data.Vec.Func?

[wenkokke]

That leaves us in a bit of a pickle regarding matrices, though. You seemed pretty happy with Data.Matrix (see here)... but that'd be rather inconsistent with Data.Vec.Functional.

[MatthewDaggitt]

Hmm I see your point that it's inconsistent, but it doesn't explicitly go against the policy that isomorphic types should be grouped together. It's just that the primary implementation would be different...

I don't know. I don't really have any good answers... I don't think exploding the every implementation out into its own top level folder is the right way to go, but at the moment we don't have a consistent scheme for when a datatype should or shouldn't be in a subfolder. If you do have a proposal for such a scheme we'd definitely be all ears? A few example subtypes such a policy should cover is:

• Data.Nat & Data.Nat.Binary
• Data.Vec & Data.Vec.Functional
• Data.List & Data.DifferenceList
• Data.List & Data.FreshList (constrained, not isomorphic)
• Data.Vec & Data.Vec.Bounded (contrained, not isomorphic)

[JacquesCarette]

I've been meaning to comment for a while: I am very much in favour of the Indexed approach. The other approaches (such as Pointwise) are fundamentally 1-dimensional and don't generalize well. They are very convenient and less noisy when dealing with 1D things. It also makes it easier to deal with the case where the index set is structured (think symmetric matrices) or sparse. In fact, a whopping 14 years ago I wrote a long post to the Haskell mailing list about this very design space.

It is also worth remembering Parnas' admonition to not venerate Hierarchies too much! Math and CS are not hierarchical, the 'dependency graph' is indeed a graph. No single tree will ever quite capture the real structure.

To me, it would actually make sense to pick an arbitrary spot in the tree (but in a deterministic way) to put the principal source, but then put in 'links' in the other just-as-good spots to where to find the actual source. This makes human findability much better!