Slimming down Data.X

[JacquesCarette]

Data.Bool imports a huge amount of stuff because it does

open import Data.Bool.Properties public
  using (T?; _≟_; _≤?_; _<?_)

That Data.Bool.Properties imports a lot of stuff is not surprising (although it probably should be split in the same way many other things are). The main thing here is that those 4 re-exports should really be in Data.Bool.Properties.Core, which could then have minimal dependencies, and thence letting Data.Bool have way fewer as well.

[MatthewDaggitt]

Hmm so I was actually planning on going in the opposite direction for the Data.X modules, see #619. My current view is that the Data.X modules should be for those people who don't care about dependencies and only care about convenience and not having to import a ton of stuff. I was actually planning to increase the dependencies of Data.X in v2.0. If you do care about dependencies then I was imagining that you should import Data.X.Base.

From the sound of it, you want to Data.X to take on the current roll of Data.X.Base. What do you envisage the difference between the two modules being?

[JacquesCarette]

Actually, I'm totally fine with a "fat" Data.X, as long as I can get a thin Data.X.Base, and a thin way to get as some relations as well. As long as the convention is clear and uniform, I'm happy to do it as you suggest. [And happy to participate in the refactor.]

[MatthewDaggitt]

Great 👍 So apart from #1489 what are the current dependency problems with the Data.X.Base files?

(Going to keep this issue open as a reminder to document this convention more clearly in README.agda)

[JacquesCarette]

The Data.X.Base files seem to be good in general. The problem is that there are currently some useful relations defined in Data.X that come from giant Data.X.Properties files. I would like to have some slim Data.X.Properties.Base files too.

[MatthewDaggitt]

When you say "useful relations", you really mean the decidability proofs don't you? 😆 This is a discussion that comes up every 6 months or so. We keep making tweaks to it, but we haven't yet settled on a solution that satisfies everyone.

The basic problem is that many decidability proofs require "properties" such as injectivity of constructors to get the recursive case through. This means that they can't live in Data.X.Base, and so we moved them to Data.X.Properties. However, @laMudri pointed out that in #929 many of the places where they are used we only need a decision and not the actual proof. In #932 they split up the definition of Dec into a boolean part and a proof part, and we added boolean based decision procedures in Data.X.Base.

The current state of affairs is therefore that when you only need to make a decision and not actually use the proof then you should use the boolean based decision procedures from Data.X.Base, e.g. _≤ᵇ_ from Data.Nat.Base. If on the other hand you do need the full proof then you can import the full Decidable proofs from Data.X.Properties, the idea being that if you actually need to get a handle on the proof then you almost certainly need other properties as well. Admittedly this story does fall apart a little bit when it comes to things like filter in Data.List.Base which requires a full decidability proof but only uses the boolean component.

Historically I was a little bit reluctant to start adding Data.X.Properties.Base files as it didn't feel like a principled solution and I felt that it was a slipperly slope and we'd soon be looking at Base.Base modules. However I seem to have already lost that battle against you with the introduction of Data.Nat.Properties.Core in #1225, so maybe it really is the best way to go.

[JacquesCarette]

I certainly wouldn't look at it as "lost the battle"... just bowed to the inevitable! 😆 [I forget the convention between .Core and .Base, I'll need to relearn it...]

Inside the library, I feel that it ought to be possible to use certain very basic things without incurring a large transitive dependency burden. I'm not advocating for a systematic breaking down of everything into small pieces (I'd like to... but it's unrealistic). Just a few select ones that are used a lot, and thus contribute a fair bit of 'skew' to the dependency graph.

[JacquesCarette]

Re-looking at this, it might be that this is largely moot - I was really thinking about the relations underlying the decidable ones, but these seem to already be exported from .Base in the places where I looked.

Now, one could make the case that there are properties that are more basic than others (such as the ones that underlie decidability). But that can be punted to the future. This particular issue doesn't really have anything outstanding to do, so I'm going to close it. We can let the issue around decidability predicates resurface organically.