agda-stdlib

agda-stdlib copied to clipboard

I haven't benchmarked this yet. I also want to add something corresponding to the standard Vec's _[_]=_, and properties relating head, tail, and lookup.

Only just looking at this now. Three quick remarks:

• all for having more Okasaki data structures in the library;

• I confess I found the development hard going in spite of the preceding discussion;

• I couldn't help but think that for some people it might be easier were it to be restructured, or at least reexpressed with the additional observations, as a series of views...

Ie:

• ℕᵇ as a view of ℕ;
• Finᵇ as a view of Fin;
• Vecᵇ as a view of Vec;

where in each case, the views from the preceding layer are being correlated in the types of subsequent views...

... so that what you end up with is a collection of functions for efficient decomposition of Vec, going via the Vecᵇ view...

That might make the representation overly coupled, but at least establishing the correspondence with the underlying 'unary' semantics might help a lot in understanding/explaining what's going on...?

Cf. Sozeau's analysis of finger trees in his first presentation of the Program machinery in Coq roughly 15years ago...

There hasn't been any movement on this for 9 months, in terms of evaluating whether the performance of this is any better than the standard definition. There were also some discussion in the library developers' meeting of whether this belonged better in a separate library.

For these reasons, I'm going to close this PR. However, @Taneb feel free to reopen if you believe it should live in the standard library and you have some data to suggest it does indeed perform better.