Increasing the amount of re-exporting in `Data.X`

[mechvel]

Suppose that one has to use _+_, divMod, gcd, +-comm -- all for Nat.
One is forced to write

open import Data.Nat ...
open import Data.Nat.DivMod ...
open import Data.Nat.GCD ...
open import Data.Nat.Properties ...

But normally, of a common reason, it needs to be only
open import Data.Nat using (_+_; divMod; gcd; +-comm).

A similar approach is desirable to other domain constructors: Integer, Bin, List, Maybe, and so on.
Can standard library organize this?
May be, to import Data.Nat.Properties to Data.Nat as public
(with hiding unneeded items)
-- ?

[gallais]

Is this #153?

[mechvel]

Is this #153?

Not precisely.
#153 suggests a single module Data that exports "everything of Data" -- which looks strange to me, something like joining all the standard library into one module.
I suggest
Data.Nat to export all the main items for the domain Nat,
Data.Bin to export all the main items for the domain Bin,
Data.Maybe to export all the main items related to the domain constructor Maybe,
and so on.

[mechvel]

Suppose that you join all the standard Data export,
and that you need +-comm for Integer.
Will Data.+-comm be for Integer._+_, for Nat._+_, or for Bin._+_ ?
In my suggestion, it will be written as
Data.Integer.+-comm, or as
open import Data.Integer using (+-comm).

[HuStmpHrrr]

instead of re-exporting Properties, I'd prefer the following

import Data.Nat.Properties
module ℕₚ = Data.Nat.Properties

this keeps the name space clean while provide access to the properties in a desired way while not introducing any name collision.

[JacquesCarette]

I think what @mechvel is after is what Bill Farmer and I called high level theories. Consider "Group Theory": this denotes two things, 1) the 'presentation of a Group', given by the record in the module Algebra, and 2) a large set of tools and definitions, as defined in most books called "Group Theory".

From a library-structuring and maintenance points of view, it makes a lot of sense to have one hierarchy that is quite fine-grained, which promotes re-use. It also makes sense to create "large bundles" that are mainly public re-exports (possibly with renames, etc) of stuff scattered all over the library into a coherent whole.

It would make sense to have a Theory or Bundle directory which contained a NaturalNumbers module that was the "high level theory" of natural numbers, related to what @mechvel is suggesting.

As @HuStmpHrrr points out, it does make sense to not necessarily have 100% short names, even in the high level theory -- it does make sense to me that properties be segregated away; I rather like the name ℕₚ.

I would, of course, make it a hard rule that the fine-grained library never import the high-level theories. That would just create way too many opportunities for import cycles. I definitely view these as a separate layering, explicitly and solely for convenience/usability.

[mechvel]

JacquesCarette:

what @mechvel is after is what Bill Farmer and I called high level theories.
[..]

Not necessary "high level" . I meant some "theory" related to the given domain (type, structure),
so that its items to be (re)exported from a single module.
For example, the theory for ℕ is described in lib-0.17 in several modules. And it will be good to be able to import all its parts from a single module, say, from Data.Nat.