ceps
ceps copied to clipboard
coq
RFC: namespaces
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
Programcan 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 Bazintroducing a new namespaceBazin which all ofFoo.Baris accessible. But you can also do that several time for the sameBaz. 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 justList-s ».
I'm probably missing other good motivations, so I'll come back here when I have more.
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
Programcan put its obligations there too.
Yes, I miss this.
Import Foo.Bar as Bazintroducing a new namespaceBazin which all ofFoo.Baris 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?
I think this CEP is too important to be stalled like that for 3 years. Who wants to have a working group about it?
Who wants to have a working group about it?
Why not. This is indeed important.
Who wants to have a working group about it?
I'd be interested in joining
I'm happy to join. Who is leading? (I mean, pinpointing the problems/differences... it may help to jump start the discussion).
I could lead somehow, I had a look at Lean namespaces and agda modules recently. We also led a small experiment with Enrico recently (https://github.com/LPCIC/coq-elpi/pull/177). Should we use a coq call slot or another slot? We could perhaps meet September Wednesday 2nd or Thursday 3rd?
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 coq/coq#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?
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.
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.
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.
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?
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?
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.
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?
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.
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
- attributing a new kernel name (fresh) and username
Ato the resulting moduleF B(with many fresh kernel names for the objects ofA), but also - adding all the user names of
F Bto the namespaceA
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?
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.
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.
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? *)
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.
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 *)
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?
raises a warning "empty namespace"
The fact that Namespace A. End A. Open Namespace A. can cause a warning is just awful, in my opinion.
Do we all agree on that?
I agree that the semantics should be to try to add the symbol B::X to module A. Whether Coq should loudly complain in that case is a different question. I would tend toward making it an error, but perhaps there is a clever use case for it that I am not seeing right now.