Cleaning up the various hierarchies

[MatthewDaggitt]

Having just re-defined the function hierarchy, and as I'm just about to contribute a hierarchy for metric spaces under Function.Metric, I'm keen to standardise the files involved in each hierarchy. Currently we have:

• Functions
  • Function.Core
  • Function.Definitions
  • Function.Structures
  • Function.Packages
  • Function (empty, but re-exports all of the above)
• Algebra
  • Algebra.FunctionProperties.Core
  • Algebra.FunctionProperties (re-exports the above)
  • Algebra.Structures
  • Algebra
• Binary relations
  • Relation.Binary.Core
  • Relation.Binary (full, and re-exports all of the above)

To straighten this out I propose that every hierarchy X should have the following files

• X.Core - contains very basic definitions, e.g. Op, Op₂, Rel, REL, Fun as well as basic combinators if applicable (e.g. function composition)
• X.Definitions - contains named properties, e.g. Transitive, Commutative, Injective
• X.Structures - self-explanatory
• X.Packages - self-explanatory
• X which publicly re-exports all of the above, parameterised by equality relations if applicable.

As the proposed top-level X module re-exports the contents of the previous modules, this should be doable in an entirely backwards compatible manner.

The only reservation I have is perhaps the name Definitions. I'd definitely prefer Properties but that name is already reserved for a certain class of files. Anyone have any thoughts?

[JacquesCarette]

Is Packages self-explanatory? I'm not quite sure what is in there -- and in my usage, I've sometimes had conflicts between the version in X and X.Packages (I'll report a bug when it occurs again).

In any case, about Definitions vs Properties. Here a little bit of theory might help: when extending a theory (of X) with ground terms, i.e. definable in the background type theory, this creates a "conservative extension" of that theory. It doesn't matter if the things being defined turn out to be 'Properties' or anything else. So I think that Definitions is a better name.

Furthermore, when I see X.Properties, I think that this is going to contain proofs of properties that X has, not definitions of properties of X.

In other words, I prefer the current naming scheme.

[mechvel]

I'm just about to contribute a hierarchy for metric spaces under Function.Metric,
[]

Metric space theory for standard library?

[MatthewDaggitt]

Metric space theory for standard library?

Well a little bit of it. The basic metric hierarchy at least (which has proven deceptively difficult to get right).

[MatthewDaggitt]

Is Packages self-explanatory? I'm not quite sure what is in there -- and in my usage, I've sometimes had conflicts between the version in X and X.Packages (I'll report a bug when it occurs again).

Packages are the name the library gives to the structures that hide all their components, i.e. Magma, Semigroup etc. as opposed to the structures IsMagma, IsSemigroup.

In other words, I prefer the current naming scheme.

Okay, great!

[mechvel]

Metric space theory for standard library?

Well a little bit of it. The basic metric hierarchy at least (which has proven deceptively difficult
to get right).

A metric is a map of type X -> RealNumberField satisfying certain properties.
So one needs to define real numbers in Agda and somehow to operate with them ...

[MatthewDaggitt]

No need for the codomain of the function to be the reals. Any totally ordered set with a bottom element will do. Indeed part of the challenge has been to come up with a design that is easy to generalise to a specific codomain.

[mechvel]

• X.Structures - self-explanatory
• X.Packages - self-explanatory

I suggest to use PreStructure as a common word for is-structures
IsMagma, IsSemigroup, IsMonoid, and such,
and to use Structure as a common word for Magma, Semigroup, Monoid, and such.
And to call the corresponding folders respectively PreStructures/, Structures/.

The motivation is as follows.

• In mathematics the notions of Magma, Semigroup, Monoid, VectorSpace, ... are often called by a
  common word structure, and are never called package.
• In programming, the word package most often means something like a parametric module.
• An is-structure in lib-1.1 is actually almost a structure (IsGroup is almost a Group, ...).
• Separating an is-structure has not any scientific meaning, it is a technical detail related to a
  particular programming language and a particular library design.