Refactoring Data.Nat.Properties

[JacquesCarette]

I'm partway through refactoring Data.Nat.Properties by breaking it up into smaller files but leaving Data.Nat.Properties externally "the same" via import public.

The point is that the .agdai file for this module is the largest in stdlib, i.e. any other module that imports it will cause a lot of disk and memory use, often for getting a handful of properties. This has a cascading effect. It has has a mildly bad effect on the dependency graph.

What this should enable is the refactoring of lots of other modules (in stdlib) to be more 'surgical' in what properties they need. In the mean time, nothing would break, as Data.Nat.Properties would externally stay as is.

The purpose for opening this issues is: if I'm wasting my time, and it is desired that Data.Nat.Properties is both a huge source file and a huge .agdai file, I'll stop! I'll assume not, but just in case...

[jamesmckinna]

I'm broadly in favour, given our shared concerns about the 'minimalist/maximalist' tensions in the library design generally (but I think you are more of a 'miniaturist' than I am), and this is certainly the 'big' one. Other issues might fall after work on this one (and similar, for Integer and Rational) but I am equally strongly tempted to say: is the the right thing to be focused on at this time, compared to a (more broad, both in scope of discussion, and of participants) discussion of

• what needs/would be desirable to happen before the, and for the, v2.0 milestone and release (2.6.3 caused the 1.7.2 bump, in part I guess because we hadn't pushed v2.0 over the line)
• what happens after, in the short, and medium, term?

Nothing in the above precludes work on the issue at hand, but I would be worried about committing your precious resource (that sabbatical won't last for ever) to this kind of thing now, as opposed to setting out a route map for what (might) happen later.

As for resource-usage, the thing that seems most hurt by this is the GitHub CI/post-commit checking cycle for PRs, which have noticeably slowed down recently (they have a bit on my local machines, but ~10minutes is an acceptable latency from my point of view, and that's been fairly constant for a while; memory footprint is of course gross, but careful tuning of the RTS parameters seems to have helped there). But again there is another more urgent issue: the GitHub scheduled brownouts designed to draw attention to the end-of-life of the 18.04LTS which our test regime currently executes under. Is there a migration policy/plan in place for that?

[jamesmckinna]

There's a separate issue, which cuts across the whole library, especially for new users (never mind developers wanting to join the PR circus): navigability. Small modules are great from an internal perspective, and having a large 'umbrella' module which gathers things together, also (mostly) helpful from an external perspective, but as we have discussed before, the Agda ecosphere as regards 'traditional' HCI concerns about navigability, surveyability, Green/Blackwell cognitive dimensions etc. leaves... much to be desired.

Small modules would, I worry, for the user trying to find out 'where things are defined, how, and what are related concepts' has a hard time at the moment with M-. etc. and the prospect now of there being a proliferation of (nevertheless more manageable, because smaller) such answers strikes me as... a different kind of scaling problem (but now for the user, having to construct&hold a much more fine-grained map in their head). Much as I hate VSCode solutions to this kind of thing, the lack of a 'theory browser' in the emacs ecosystem is something I regret. Working on a definition-by-definition basis is... well, slow degree by slow degree. System-level issues such as (better) exposure to the interfaces exported by a module, or better, that together with the interface offered by a particular qualified import of a module, would also be... helpful, I think.

But as you always say: better solve problems you can now, than wait for solutions to bigger problems tomorrow, but against that, local search for optima doesn't always pay off... and more global/less local attacks on the problem might also be necessary.

EDITED I'm not singling out Agda here, either. Despite having an attractive and highly usable jEdit-hosted interaction surface, I find that I still get no productivity benefit from the theory browsing tools in Isabelle; by contrast, I find sledgehammer often to be a much better 'browser', because it shows me things that I didn't even know to look for on the way to a proof...

[MatthewDaggitt]

Hmm so while I'm in favour of the change eventually, I'm dubious about this particular refactor at this time for the reason that @jamesmckinna outlines above. One of the major complaints we get by new users is that the library is impossible to navigate, and to find things in. Until we have a decent search facility, ala Hoogle, I'm very reluctant to split things up further....

[JacquesCarette]

Various bits:

• my focus/time: I worked on this because 1) huge modules irritate me greatly, 2) doing such refactor work require very little brain and yet can't be done by just anyone.
• I'm fine if this doesn't land in 2.0, it can be in 2.1
• I agree that issues like Github CI are quite a bit more urgent; I just have so little expertise here, it doesn't feel like it would make sense for me to plunge in

But the big one: Navigability. That's a big one. Because I firmly believe that the end-user experience should weigh in a fair bit, and certainly can at times trump the developer experience, I'm resigned to the fact that this infrastructure improvement is not timely. [There is a reason I created this issue in parallel with working on this, rather than just landing a big PR!]

So the question is: who is going to work on search tools? I am not. But I would be happy to drum up some demand for it.

[JacquesCarette]

I think we should close this issue. A new one can be opened when we have decent search tools (or even this one re-opened). Right now, this is just noise.