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.

[MatthewDaggitt]

@andreasabel wrote:

A "package" is usually a collection modules bundled together by a mechanism outside of the programming language.

We should look for a different name for Function.Packages.

What is the intended meaning of "package" in the context of the std-lib?

The packages refer to the record types that hide all their components:

record Magma c ℓ : Set (suc (c ⊔ ℓ)) where
  field
    Carrier : Set c
    _≈_     : Rel Carrier ℓ
    _∙_     : Op₂ Carrier
    isMagma : IsMagma _≈_ _∙_

whereas "structures" refer to those that expose their components:

record IsMagma (∙ : Op₂ A) : Set (a ⊔ ℓ) where
  field
    isEquivalence : IsEquivalence _≈_
    ∙-cong        : Congruent₂ ∙

The name "packages" was already being used before I took over, and I just continued to use it. I always imagined that it just referred to them being all "packaged up". I'm not wedded to it particular. If the community can come up with an alternative name for them then it wouldn't be a problem to adopt it. We should do it before the next release though, as I'm just introducing the first modules named "Packages".

[JacquesCarette]

We've started to use "bundled" instead. See the paper accepted to GPCE A Language Feature to Unbundle Data at Will, with the full prototype having its own web site documenting our ideas.

The current prototype is implemented in emacs Lisp, but that's a playground for ideas meant to be eventually implemented without meta-programming.

[MatthewDaggitt]

Hmm so Algebra.Bundles, Relation.Binary.Bundles etc.? I could get on board with that...

[andreasabel]

I favor "bundle" over "package" since "bundle" does not have a strong connotation. A package is usually a "big" organizational structure (collection of modules).

[MatthewDaggitt]

Closing as now completed, thanks to everyone for their input!