RFC: namespaces

[gares]

@JasonGross feel free to take over this PR

[aspiwack]

I've got to say that I really like the idea of separating, at least in part, the notion of namespace from the notion of modules (some may remember me championing this sort of idea years ago).

On the other hand, this proposal still feels a bit half-baked. And I would guess this is because the motivations are a bit narrow. (also let me remark that namespace and mixins are fairly different concepts, I would advise against equating them in the proposal). Let me share some of my own thoughts as a way forward:

• One use of namespace that I find appealing is to associate a namespace to every constant/inductive where plugins such as the inductive scheme generator can put the constant they define. Or Program can put its obligations there too. This, however, goes against two assumptions in the proposal:
  • Namespace must be able to be nested (with the semantics being that namespace compose)
  • Namespaces must be able to be declared in a functor (in which case they would be composed with the namespace of the module resulting from a complete application)
• I like to think of modules as extensible records which incidentally define a namespace (making the namespace thing more primitive)
• Another thing we may want to do with namespace is manipulate them. For instance we could do, in the style of Haskells import qualified, something like this: Import Foo.Bar as Baz introducing a new namespace Baz in which all of Foo.Bar is accessible. But you can also do that several time for the same Baz. Typical use is that you have several modules declaring functions for a data-structure, say lists (either from different libraries, or maybe from a single library that declares functions and specification separately), and you want to say « meh, this is all just List-s ».

I'm probably missing other good motivations, so I'll come back here when I have more.

[herbelin]

One use of namespace that I find appealing is to associate a namespace to every constant/inductive where plugins such as the inductive scheme generator can put the constant they define. Or Program can put its obligations there too.

Yes, I miss this.

Import Foo.Bar as Baz introducing a new namespace Baz in which all of Foo.Bar is accessible.

+1. I don't know well Haskell but I can see how Agda is much more flexible than Coq in structuring name spaces.

To be able replicate to the directory structure within a file is also something to achieve.

What syntax do we need for these features? For instance, would it be enough, as proposed in BZ#3171 to extend the Module syntax so that it can set an arbitrary prefix, as in, e.g., Root Module Coq.MyTypes, or Module ../MyTypes, or Module Init.MyTypes, or Extend Root Module Coq.Init.Datypes. As well as an Import ... as Root Foo, Import ... as ../Foo, Import as Foo.Bar?

[CohenCyril]

I think this CEP is too important to be stalled like that for 3 years. Who wants to have a working group about it?

[herbelin]

Who wants to have a working group about it?

Why not. This is indeed important.

[ppedrot]

Who wants to have a working group about it?

Count me in.

[JasonGross]

Who wants to have a working group about it?

I'd be interested in joining

[gares]

I'm happy to join. Who is leading? (I mean, pinpointing the problems/differences... it may help to jump start the discussion).

[CohenCyril]

I could lead somehow, I had a look at Lean namespaces and agda modules recently. We also led a small experiment with Enrico recently (LPCIC/coq-elpi#177). Should we use a coq call slot or another slot? We could perhaps meet September Wednesday 2nd or Thursday 3rd?

[herbelin]

Should we use a coq call slot or another slot? We could perhaps meet September Wednesday 2nd or Thursday 3rd?

My own feeling is that a slot different than the call slot might be more comfortable (specific audience, different time constraints) but that's only my own view. Wednesday or Thursday are fine to me.

A related question in passing: in PR rocq-prover/rocq#12890, there is a need to generate names morally private to a tactic. Would it make sense as part of the discussion to consider private name spaces, or private name subspaces where it is ensured that no collision with user names will happen, e.g., here for ring, a subspace like pwd.Private.ring_lemma? Or is it overkill?

[herbelin]

Is the idea of associating a name space to inductive types part of the proposal? It is in the air for long (and finally something of that sort is implemented in Lean), but it seems to me that it would be rather natural to have nat, nat.O, nat.S, nat.rect, nat.add, nat.add.assoc, etc. without having to explicitly define a module (which would not support writing nat, requiring instead the nat.t workaround conventionally used in OCaml), nor having to see the module non-extensible after End is given.

Somehow, this is also starting to give more structure to the identifiers, observing that _ plays too many rules and introducing a specific symbol to indicate the idea of specialization.

[aspiwack]

Is the idea of associating a name space to inductive types part of the proposal?

I'm rather an outsider these days, but for the record I'd very much like that.

[gares]

I think the discussion should separate the mechanism and it's adoption in the common practice.

I do like the idea of inductive as namespaces, and the derive command in Elpi already hacks it with modules, see
https://github.com/LPCIC/coq-elpi/blob/master/apps/derive/examples/usage.v for an example.

But what is more important to me are the details of the mechanism. For example the last line of
https://github.com/LPCIC/coq-elpi/blob/master/apps/NES/examples/usage_NES.v
Shows something you can't implement on top of modules, since they play the role of metadata containers, while I believe namespaces should only contain data.

Imo we should focus on these details first.

[CohenCyril]

Let's try to meet: https://framadate.org/MmlNR3wImPHtDLqX

[CohenCyril]

The best date is Thursday, September 10, 2020 - 16:00-17:00 CEST. Let's meet then. @JasonGross @gares @herbelin does https://visio.inria.fr work for you all?

[JasonGross]

I think visio works---that's what Coq calls use, right?

[CohenCyril]

I just sent @JasonGross @herbelin and @gares an invitation by mail

[ppedrot]

@CohenCyril can I get one as well?

[CohenCyril]

@CohenCyril can I get one as well?

sure, wait a sec

[CohenCyril]

Here are my notes:

• Clarify the difference between kernel name and user name
  • kernel names should be fresh identifiers outside of the user namespace
  • how to deal with kernel names with no user name? We need to display kernel names in a robust way.
  • this decorrelation is also a cheap way to have abstraction (you'd have to go as far as pattern match on unbound kernel name to break abstraction barriers)
• How do namespaces compare to modules?
  • What is a namespace? What should it contain? Inductive Definitions for sure, what about hints, arguments, notations canonical structures?
  • Should we choose on import whether to get side-effects?
  • Ltac and Definition namespace do not collide, should it be the same for modules (the consensus seems to be yes)
  • Achieve separation of concern by taking out of modules the job of handling names. In this view namespaces should solely be a way to access the context. Hence opening a namespace should just shorten the names, importing side-effects should be independent from the namespacing system. As such side-effects should have a name, and getting the side effect is not about opening/shortening the names, but adding the designated side effects to the current environement.
  • Should namespaces be global? (Cyril: I am not sure I understood this part of the conversation)
  • What is a file? Still a module, the namespace being populated on import?

[gares]

Should namespaces be global? (Cyril: I am not sure I understood this part of the conversation)

Should namespaces be global entities, always visible, or be contained in modules? (I can open a namespace N defined in a module A only after having imported A).

To my recollection, namespaces are global in all the PL I've used.

[CohenCyril]

Should namespaces be global? (Cyril: I am not sure I understood this part of the conversation)

Should namespaces be global entities, always visible, or be contained in modules? (I can open a namespace N defined in a module A only after having imported A).

To my recollection, namespaces are global in all the PL I've used.

Ah I see, however, it cannot be the case for functors, first you do not have a symbol before you apply it, and you may not want to automatically populate a name space by a mere application (e.g. Module A := F B, unless this automatically opens namespace A?), but rather wait for import to get them... Somehow, isn't namespacing population a side effect?

[silene]

you may not want to automatically populate a name space by a mere application (e.g. Module A := F B)

I think you do. As soon as a new named symbol is created, it has to live in a namespace. I don't see the point of delaying the existence of this name. (Note that populating a namespace might be a lazy operation, but that is just an implementation detail. It should not be observable by the user.)

To my recollection, namespaces are global in all the PL I've used.

For the record, C++ has the notion of anonymous namespaces. Symbols in such namespaces can only be accessed by the current translation unit. In Coq parlance, it means that they have no fully qualified name, or rather, their fully qualified name is random.

[CohenCyril]

you may not want to automatically populate a name space by a mere application (e.g. Module A := F B)

I think you do. As soon as a new named symbol is created, it has to live in a namespace. I don't see the point of delaying the existence of this name. (Note that populating a namespace might be a lazy operation, but that is just an implementation detail. It should not be observable by the user.)

If we decorrelate modules and namespaces, it means Module A := F B is not only

1. attributing a new kernel name (fresh) and username A to the resulting module F B (with many fresh kernel names for the objects of A), but also
2. adding all the user names of F B to the namespace A

And these seem to be two distinct primitives, which make sense to combine together for users of the Module := command, but not in the API, and there might be more elaborate commands to only do 1. or 2. WDYT?

[silene]

For me, these two cases are the same primitive ("create a given name in a given namespace"), but it can indeed be called numerous times: once for creating the module name A in the enclosing namespace Foo, then several times to create the symbols bar, baz, etc, in the namespace Foo.A.

There is, however, another primitive for creating the namespace Foo.A, which is independent from the creation of module symbol Foo.A. Either of those can happen first. But obviously, namespace Foo.A needs to exist before symbols are added to it.

[CohenCyril]

But obviously, namespace Foo.A needs to exist before symbols are added to it.

Not obvious to me, I think the opposite actually, namespace x exist iff there is a definition which prefix is x.

[silene]

Not obvious to me, I think the opposite actually, namespace x exist iff there is a definition which prefix is x.

This looks like a footgun:

Module A. End A.
Import Namespace A. (* Module A is empty, and so is the namespace. Should it fail because the namespace does not exist? *)
Import Namespace A'. (* A' is a typo. Should it succeed? *)

[CohenCyril]

Not obvious to me, I think the opposite actually, namespace x exist iff there is a definition which prefix is x.

This looks like a footgun:

Module A. End A.
Import Namespace A. (* Module A is empty, and so is the namespace. Should it fail because the namespace does not exist? *)
Import Namespace A'. (* A' is a typo. Should it succeed? *)

If we are talking about namespaces and not modules anymore, doing Namespace A. End A. is a noop (like Section foo. End foo. is). And both commands should have the same output. In my opinion, it should be a warning "namespace is empty" or something like that.

[CohenCyril]

To be more precise, there is a difference between

Namespace A. End A.
Open Namespace A. (* raises a warning "empty namespace" *)
Open Namespace A'. (* warning  "empty namespace" *)

And

Module A. End A. (* assuming this create both the module and name `A` in the root namespace *)
Open Namespace A. (* warning "empty namespace"  *)
Open Namespace A'. (* warning "empty namespace"  *)
Import A. (* no warning, usual behavior *)
Import A'. (* error: no module A in the root namespace *)

[gares]

I'm still a bit puzzled

JustModule A. (* the low level primitive *)  (* \____  Module A   *)
Namespace A.                                 (* /                 *)
Definition x.
End Namespace A.
JustEnd A.

When one writes A.x what do we mean?

To me it is A::x (the term x in the namespace A) and when I write Module B := A, the A is the module named A in the empty namespace, namely ::A. It happens that module A contains a pointer to x, but it is not that x is in A because of a "matching prefix". If the namespace was named B, then B::x would still be inside module ::A.

Do we all agree on that?

[Blaisorblade]

In case it wasn't brought up: Namespaces should also differ regarding (super)global effects — #[export]/#[global] does not do the right thing for effects inside a namespace. I'd want #[export] effects to be visible when the containing module is imported, regardless of whether the namespace is open.

Module address.
  Definition t := N.
  #[global] Bind Scope N_scope with t. (* Not superglobal *)
End address.
(* Here [address.t] isn't bound to N_scope. *)

https://coq.zulipchat.com/#narrow/stream/237977-Coq-users/topic/Superglobal.20effects.20and.20namespaces

[herbelin]

With a 3-years hindsight, has someone an idea of why it stalled? Is it that the design space is still too large to start an experimentation?

E.g. why not starting stepwise, e.g. by reusing the existing implementation of modules and adding a tag to modules to tell which of them have to be considered as name spaces? Then adding gradually features to these "namespaces"?

[Blaisorblade]

E.g. why not starting stepwise, e.g. by reusing the existing implementation of modules and adding a tag to modules to tell which of them have to be considered as name spaces? Then adding gradually features to these "namespaces"?

Has this stalled? IMHO, Elpi's Namespace Emulation System (NES) lets you try the feature today, so there's no need for a gradual migration — we know what works and doesn't work, and implementing that experience into core Coq would avoid the encoding artifacts we see today. We already use NES at Bedrock and have contributed improvements; NES is already adequate for evaluation.

General downsides of a gradual migration on the Coq side:

• gradual evolution without a coherent design often lead to an inconsistent design — such as seen in C++, Scala, and many parts of Coq itself.
• With the migration for #[export], at each release on the way Coq had a strange half-way design. Worse (but hopefully not applicable), warnings forced to migrate hints eagerly for some constructs (adding explicit specifiers), when migration wasn't supported for others.

OTOH, supporting gradual migration of clients is welcome, and often necessary.

[herbelin]

Assume we implement the following:

• a command Declare Namespace MyNameSpace which declare a global namespace name, say MyLibrary.MyFile.MyNameSpace (or maybe just MyLibrary.MyNameSpace, as suggested by @gares) (and we could even support long names as in Declare Namespace This.Is.A.Long.Namespace)
• support for blocks Namespace qid. ... declarations ... End qid., which, when rooted in global location Foo.Bar.Etc, and when qid resolves to say MyLibrary.MyFile.MyNameSpace, do the following for any logical name id(or abbreviation) in the block:
  • declares absolute kernel (and nametab) names Foo.Bar.Etc.id
  • also declare nametab names MyLibrary.MyFile.MyNameSpace.id (with mandatory qualification) (this can possibly shadow other names of the namespace, but the absolute names remain at worst available)
  • activate the non-logical declarations of the block (or at least a selection of them)
• when qid refers to a namespace in Import qid, make the names of the name space available w/o the MyNameSpace qualification

Would that fit the needs?

Compared to Elpi emulation, that would give a proper official global name to the namespace instead of implicit wrapper names of the form This_aux_1 (see coq-elpi examples here).

Compared to what @gares wrote above:

decorrelate file/dir structure with the qualified name used to denote a thing

This would give two names to a same thing: the (unshadowable) physical name Foo.Bar.Etc.id and the (shadowable) namespace name MyLibrary.MyFile.MyNameSpace.id.

"opening" a name space does have no side effects, e.g. it only contains names, not metadata such as coercions, notations, ...

As advocated by @Blaisorblade, side effects (or at least selectable side effects) would be possible.

[herbelin]

An alternative to having both a "physical" unshadowable name and a "namespace" shadowable name is to have only an unshadowable "namespace" name (and then the kernel name is forged on the namespace name).

This means that loading two distinct modules populating the same namespace with a same name is rejected. I guess that this typically assumes namespaces to be registered to a central place: e.g. for a namespace living under a library root, there would be a way to know all names declared in the given name space by all libraries living under that root.

[gares]

• declares absolute kernel (and nametab) names Foo.Bar.Etc.id

This breaks many invariants we have today, but I don't get what it would bring.

[herbelin]

Let's explore the idea that the kernel name of a declaration in a namespace, say, Root.MyNameSpace, is forged from the namespace name, that is, are of the form Root.MyNameSpace.id, that is that a name space acts as the primary container of its contents.

[Added: what I describe below does not seem right: the extension of a namespace should be "stored" in the library file being built. So, that should rather be like an ordinary module except that 1) the prefix for naming the contents of the module is different from the one of the module 2) the module should not be considered a member of its own surrounding module/library. Regarding the env, it is anyway already a flat map, so nothing to do, besides using the namespace name as prefix. Regarding the nametab, this is controlled at caching/loading, so nothing special to do besides using the namespace name as prefix. So, shortly, it would just be about adding an optional "alternative prefix" in SFBmodule and ModuleObject (??).

We would also need a table of namespace (as a summary but also in the kernel so that we can rebuild a module out of its components dispatched in different files).]

Trying to prepare an implementation, this means, at the time of the command Namespace qid:

• suspending the construction of the ongoing stack of modules, reinstalling the corresponding sequence of OpenedModule/CompilingLibrary (in lib.ml) and STRUCT/LIBRARY (in safe_typing.ml); making the declarations of the ongoing stack of modules visible as specified in the module type of the modules

At the time of the End of a name space:

• same as for the End of a module, closing the stack of OpenedModule/CompilingLibrary and STRUCT/LIBRARYcorresponding to the name space, but using some new Modops.extend_module rather than Modops.add_module for logical declarations
• reinstalling the previous stack of ongoing modules being built

At the time of loading a Namespace block:

• similarly adding the leaves of the block at the appropriate location, traversing the stack of corresponding ModuleObject nodes, again using Modops.extend_module rather than Modops.add_module

Other remarks:

• when building a namespace, no reopening of a namespace external to this namespace (that would look otherwise quite convoluted)
• we should also fail if currently building a functor and the name space refers to the outside of the functor (since then the name space would escape the scope of the parameters of the functor)

[herbelin]

So, my previous proposal not being right, here is another (simpler) proposal for shadowing-free name spaces:

• provide a Declare Namespace qid command bound to a NAMESPACE object and to a corresponding summary collecting the list of declared namespaces (of the form Root.MyNameSpace or Root.MySubRoot.MyNameSpace, etc.)
• add to SFBmodule (kernel) and ModuleObject (non-logical objects) an optional field referring to a declared namespace, so that the command Namespace modpath opens a module with this field set to modpath
• whenever a declaration id is cached or loaded in the namespace-as-module, use the kernel name modpath.id; if a declaration of same kernel name exists, this is an error; register also the name to the nametab
• at the end of this namespace-as-module, it seems we want to export all non-logical declarations

@gares: does this correspond to what you have in mind? Does it satisfy the invariants you have in mind?

To implement name spaces allowing shadowing, use instead the "physical" kernel name as handle in the global env (but declare both the namespace-based name and the physical name to the nametab, so that shadowed names remain at least accessible using their physical name).

[herbelin]

Summary of Coq call (11 Nov 2023): @CohenCyril and @gares think that the ability to shadow is important. There are however different views on what the status of shadowed names should be. As far as I could understand:

• For some people, shadowed names should be printable but not parsable, so, they should be printed with a special non reparsable key (e.g. #Foo) or using a random number changing from one session to another so that the user cannot put it in a document in a robust way.
• For other people, leaving the ability to the user to refer to any name, even shadowed, is more important and there should always exist a way to refer to a name one way or another.

Maybe a compromise would be to allow referring to a shadow name when working interactively, but not in a document intended to serve as a library?

[gares]

• For other people, leaving the ability to the user to refer to any name, even shadowed, is more important and there should always exist a way to refer to a name one way or another.

What about to reserve a namespace root for kernel names, e.g. CIC.Coq.Init.Datatypes.nat or CIC.mathcomp.ssrnat.addn and disable shadowing there?

In a sense it would not be a real namespace, but just a way to use a Kernel Name to address a constant by its, well, kernel name. The current kernel invariants will ensure there is no collision there, and the pretty printer can always fall back to that namespace if needed.

Maybe a compromise would be to allow referring to a shadow name when working interactively, but not in a document intended to serve as a library?

It may be important to be able to "resurrect" a shadowed concept, but I think it is also important to discourage this.
One the advantages of namespaces is that you can (easily) change the files layout without any user visible change. Which is not the case if one mentions kernel names (which do include file names).
I don't think batch/interactive should be different, after all we use "interactive mode" for our batch tests.

[herbelin]

What about to reserve a namespace root for kernel names, e.g. CIC.Coq.Init.Datatypes.nat or CIC.mathcomp.ssrnat.addn and disable shadowing there?

Why not.

It may be important to be able to "resurrect" a shadowed concept, but I think it is also important to discourage this.
One the advantages of namespaces is that you can (easily) change the files layout without any user visible change. Which is not the case if one mentions kernel names (which do include file names).

This is also how I see it.

I don't think batch/interactive should be different, after all we use "interactive mode" for our batch tests.

We could also provide a command Set Interactive Document/Unset Interactive Document which tells to accept/reject a number of features (like Require in a section, or nested goals, or Undo, etc.) independently on whether the file is processed by coqc, coqtop or a UI server.

[ejgallego]

Maybe something like other languages do ::Foo to refer to the root namespace could be useful here?

[herbelin]

Maybe something like other languages do ::Foo to refer to the root namespace could be useful here?

It requires a syntax change, and :: may clash with list concatenation, but why not.

[herbelin]

Actually, I'm still confused about shadowing. In the long discussion above and in particular in this comment, only shadowing of partially qualified names is mentioned, but this is already supported since the fully qualified handle on the name is not hidden. Still browsing the discussion above, the motivation for shadowing (and actually even of simply removing from the scope) seems only to discourage users to use, or even see, a name that is not part of the intended abstraction. But this is not a question different from the question of abstraction we already have with modules and I believe it can be treated separately (*). So, is there really a typical case where shadowing a fully qualified name would be needed, that is, is there a typical case where two files define the same absolute name, say Root.Dir.x, and we want to load both files together without erroring?

(*) e.g. with module types as they are now, or with lighter, more implicit ways, to specify module types.

A second question is: @gares, @CohenCyril, how do you imagine a namespace to be initiated? E.g. to declare a name space, say, mathcomp.fingroup, do you imagine a file mathcomp/fingroup.v starting with a command, say, Use Library Name as Namespace indicating that mathcomp.fingroup is a name space? Or do you imagine the presence of a file of the form Root/Foo/Foo.v (e.g. mathcomp/fingroup/fingroup.v) to conventionally start a namespace Root.Foo? Or do you imagine a file loaded before all other files, e.g. mathcomp/fingroup/namespace.v with in it a command Declare Namespace mathcomp.fingroup.? Or maybe a single file mathcomp/namespaces.v that declares all namespaces registered by mathcomp? Or do you imagine namespaces to be defined implicitly, e.g. using say Module fully.qualified.name to mean a global namespace, and if another file refers to the name name they implicitly share the contents? Or do you imagine namespaces to be populated implicitly definition per definition, e.g. using declarations of the form Definition fully.qualified.name := ...? Etc.

[gares]

If we keep the current syntax for denoting things, eg A.B.c then one can create a namespace called Coq.Init.Datatypes and put another nat in there, so the fully qualified name of nat can't be used to refer to it. This is, to me, the only reason to keep a safety net and be able to print/parse the nat in the prelude in this weird cornercase.

Similar collision may arise by importing two libraries which independently add the same name in the same namespace, eg list.map3 which is not in the stdlib but you may have added in your corner. you want to be able to load the two libraries. The shadowed copy may show up in a print, or you may want to unshadow it by giving it another name.

[gares]

If we don't keep the same syntax (which I don't like, but helps explaining), then Coq.Init.Datatypes.nat will always point to the nat we know, and Coq#Init#Datatypes#nat would be something from a namespace. No collision here, no need for a safety net...

[gares]

Since we want the new mechanism to have the nice, usual, syntax, it was proposed to use the ugly one for kernel names, and I proposed another way to skin the cat by saying that CIC.x.y.z really means x#y#z as a kernel name. No need to touch the parser in this case. I don't have a strong opinion about this specific aspect.

[herbelin]

one can create a namespace called Coq.Init.Datatypes

Indeed, there is the underlying question of whether names of namespaces live in the same space or not as names of modules. I was assuming that they would live in the same name space, i.e. that Coq.Init.Datatypes was considered either as a name space or as a module but not both. My assumption was that using the same name space was simpler to explain (no need e.g. to rename all current Nat.foo into Nat#foo, or no need to turn all Foo for which Foo.bar is used into a namespace so that the syntax Foo.bar can be used), and simpler to implement (reusing the current module infrastructure) but indeed, the question has to be raised.

Unfortunately, I don't know how to solve the question. What would be the pros and cons of each approach?

[gares]

I think that Module X should both start the container X and push X on top of the name space machinery.
In this way we get a lot of retro compatibility, since modules are used both as containers and as name-qualification artifact. Similarly Require Import would both open the container and the namespace. If we do so, Coq.Init.Datatypes will be both a module/kernel-name and a namespace.

I really see this as separating two existing concepts, and giving access to both independently. As I was saying the nametab already does roughly what we need, but there is no way to operate on it without also creating a container or opening it.

But I think I'm just repeating my summary up there.

[herbelin]

If we do so, Coq.Init.Datatypes will be both a module/kernel-name and a namespace.

I see. Then, the question of whether every Module incantation opens a namespace is yet another question to decide.

But first, how do you define, say, a mathcomp.fingroup name space? Do you mean that the mere existence of a file fingroup.v in a directory bound to the root mathcomp is enough to create a namespace?

I'm now also a bit confused about the objective to provide a naming layout which is not necessarily the same as the one of files. Letting every file, and every module of a file be a namespace, etc., seems to compete with the objective to discourage users to refer to names which we may want to keep internal. So, it seems that an arbitration between the different objectives is needed.

[gares]

Just compiling the current files will give you a set of name spaces which is identical to the current module structure. No magic. But one can change that in a library and take advantage of the new feature. I let @CohenCyril give examples about MC.