Closed MatthewDaggitt closed 4 years ago
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.
I'm just about to contribute a hierarchy for metric spaces under Function.Metric, []
Metric space theory for standard library?
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).
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!
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 ...
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.
- 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.
@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".
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.
Hmm so Algebra.Bundles
, Relation.Binary.Bundles
etc.? I could get on board with that...
I favor "bundle" over "package" since "bundle" does not have a strong connotation. A package is usually a "big" organizational structure (collection of modules).
Closing as now completed, thanks to everyone for their input!
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:Function.Core
Function.Definitions
Function.Structures
Function.Packages
Function
(empty, but re-exports all of the above)Algebra.FunctionProperties.Core
Algebra.FunctionProperties
(re-exports the above)Algebra.Structures
Algebra
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 filesX.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-explanatoryX.Packages
- self-explanatoryX
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 preferProperties
but that name is already reserved for a certain class of files. Anyone have any thoughts?