What is the reason for the p.(f)
syntax? I seem to remember p.f
had an issue with parsing, but I can't find the discussion on it.
That's the same syntax as module qualification.
Contrarily to OCaml, which has different syntactic classes for modules vs term variables, we don't have that in Coq so we must separate qualification syntax from projection syntax.
Is there a good reason for not having different syntactic classes?
History.
Time to learn from it, maybe? :)
I don't know. Did lean make the same error?
(One reason we have so much syntactic cruft in Coq is that our parser is too malleable. If we had to adhere to strict LALR, we wouldn't be randomly hacking our way through this mess.)
Pierre-Marie Pédrot said:
I don't know. Did lean make the same error?
they don't have primitive projections
Not yet, but what about qualifiers?
AFAIK they don't have a syntactic difference between modules and term variables, so it's like in Coq.
(it's not completely crazy though, since in presence of unicode getting a reasonable notion of caps is non-trivial.)
Changing the definition of literally the most basic syntactic class is not going to play well for us, so we'll have to live with it.
https://leanprover.github.io/reference/expressions.html#constructors-projections-and-matching
The anonymous projector notation can used more generally for any objects defined in a namespace (see Chapter 5). For example, if l has type list α then l.map f abbreviates list.map f l, in which l has been placed at the first argument position where list.map expects a list.
Changing the definition of literally the most basic syntactic class is not going to play well for us
Due to the amount of work or a different reason?
you'll break 200% of the developments and the fix is going to be a PITA for the end-users.
Pierre-Marie Pédrot said:
Contrarily to OCaml, which has different syntactic classes for modules vs term variables, we don't have that in Coq so we must separate qualification syntax from projection syntax.
I don't follow. As long as module qualifiers and projection share a common grammar, there is absolutely no need to separate them. In other words, whether foo
is a module or a variable changes nothing as to the fact that foo.bar
is a term.
@Guillaume Melquiond no, because then you can't separate between a projection and a module field
there is an ambiguity
let me write down an example
Module foo.
Module bar.
Definition qux := tt.
End bar.
End foo.
Record Qux := { qux : unit }
Record Bar := { bar : Qux }.
consider foo.bar.qux
do you mean the projection or the module field?
You can mix this in fancy ways, and I am pretty sure you can encode post correspondence problem with it.
This has nothing to do with the parser. The parser has no trouble with foo.bar.qux
. What you then do of it is a different matter. But again, there is no issue on the syntax side.
I haven't said it was a problem with the parser specifically.
but in OCaml the two are discriminated at parsing time by syntactic classes
So, what? We do not even distinguish constructors from pattern variables in Coq?
if something on the LHS of a dot starts with an upper case it's a module qualification, otherwise it's a projection.
so it's ambiguous.
given how fragile name resolution is, mixing both syntaxes is gonna hurt
we don't even have a way to refer to an absolute name.
IIRC there are also issues with associativity of dot
(ftr, the confusion in patterns between constructors and variables has bitten me too many times for me to believe this is feature)
this is a poor design choice
we can make it worse, yes.
As far as I am concerned, choosing a syntax for projections different from all the other programming languages is what I call making it worse.
If you can't reliably resolve names, you're looking for trouble. Coq is not your average programming language.
That is a mistake. Coq should be an average programming language. No need to aggravate users. There is no good reason to make Coq an elitist language.
It's too late anyways.
Do you claim that we should change the syntax for module qualification?
Another issue with the dot syntax for projections is that it plays badly with non-primitive projections when you have to specify parameters
if you unset implicit arguments for non-primitive pairs for instance, you'd have to write p.(fst _ _)
What is wrong with p.fst _ _
?
that does not mean the same
p.fst _ _
would be the first projection of p
applied to some arguments
if we had primitive projections since the beginning I agree we wouldn't have had this issue
No, I say we should change the syntax for projections. Sure, once foo.bar.qux
has been parsed, you need to take a decision on whether you want to interpret both foo
and bar
as variables or modules (assuming both interpretations are available), but that is nothing fundamentally new. Also, there is nothing wrong in having to write p.(fst _ _)
when you need to pass implicit arguments to a projection.
Do we have examples of projects not using primitive projections on purpose? It seems to me (perhaps naively) that there is no reason not to use PP?
@Guillaume Melquiond but then I don't understand your argument, if we already have to write parentheses in the applied case
something I learned from the primitive projection mess is that you need to have a faithful way to print the contents of a term
@Ali Caglayan backwards compat and some parts of the code handling badly pp
@Guillaume Melquiond I am actively advocating for a third syntax to really mean pp
we have currently a hodgepodge of bugs because there is a confusion between pp and the definition wrapper
this is another reason for a syntax difference actually
if you allow defining a constant with the same name as a pp, then there is no way to differentiate them in foo.bar
did you mean bar
the pp? the wrapper constant?
(all of this mess was introduced in the first place to "ease" backwards compatibility, but imo we've just created an order of magnitude more issues with that)
Users should almost never have to explicitly write implicit arguments to projections. If they do, then it is a failure. The syntax with parentheses should be reserved for very rare instances. The general case should not need parentheses.
OK, but then what about pp vs definition?
you need to be able to display the difference to the user
in OCaml it's clear what is a projection and what is a constant, once again because of syntactic classes
Foo.bar is a constant, foo.bar is a projection
but in Coq, I've lost hours of my life due to the ambiguity between both
(I'd have preferred that defining a constant with the same name as a projection would be prohibited, but that's not the path we've taken, and there is no way back)
so I have doubts that allowing to confuse both in more general cases is going to be helpful to the user
(at least not without a way to print it faithfully)
So separating the classes would be a good thing to do?
You wrote before:
you'll break 200% of the developments and the fix is going to be a PITA for the end-users.
I don't see what the end user would notice?
uh
anybody using lower case constructors must now rewrite their devs
same thing for modules
what if you used non-ascii letters in them?
(at least for the leading one)
you probably don't pass Coq.Init
Oh, I see so the idea is to use case to distinguish modules and terms
that's what OCaml does, I am not suggesting this has a micro-ounce of realism in Coq
OK, so here is a dumb idea: What if record terms became modules themselves? Sort of unifying the dot syntax?
nope
nope nope nope
module typing is a minefield
outside of term typing
the last thing you want is more modules
(I mean, this does not even make sense, module typing lives above term typing.)
(you can't quantify over modules in a term, and functors are probably ridden with soundness issues anyways)
But isn't it precisely the idea behind the Lean statement that was quoted? The general notion of "namespace" would encompass many things, among them modules, records, etc.
This doesn't mean making records modules though :smile:
A functor blocks your path.
Where do people use module functors?
You mean, in general as a design pattern, or in particular developments,
The latter
the stdlib uses it
color abuses functors in creative ways
I think iris also relies on them
they're good "weapons of mass abstraction" but they're really outlandish in Coq
there are many non-kernel "issues" with functors (they can become features if you squint enough)
I use functors for generativity. This is useful for reflective automation which usually needs common datatypes (lists, options, etc) and functions on them and wants to perform simplification. I can't risk reducing occurrences of these functions that I didn't introduce. So instead I have fresh copies of all the datatypes and functions. This way I can simplify/reduce freely.
yes, typical use of functors as workarounds to unrelated issues :/
out of curiosity, what reduction are you using?
Funnily, functors are not supposed to be generative in Coq except if you wrap them in a signature, so you might be relying on bugs
Usually cbn
with infrequent calls to simpl
inbetween because cbn
doesn't quite suffice.
My functors have signatures
ok, so that's the safe fragment
for the uninformed, there is a huge confusion in the upper layers regarding the so-called "canonical names"
canonical names are a way to guarantee some form of name quotient resulting from functor application / module inclusion
so, precisely a way to be applicative, not generative
this is ill-designed because it does not work for higher-order functors, but for Pi 0 1 it's reasonable enough
the problem is that it relies on kernel names being implemented as a pair of names canonical / user
canonical is the "root name" of the object, i.e. the place it was originally defined, when user is the one resulting from inclusion / functor application
some parts of the code use user, some use canonical
so we have a borken quotient
even without taking soundness into considerations, this is very problematic for tactics, unification and whatnot
hints, for instance
Pierre-Marie Pédrot said:
Funnily, functors are not supposed to be generative in Coq except if you wrap them in a signature, so you might be relying on bugs
wut
All my functor bodies are actually Include SIGNATURE.
so I am sure that I am relying on bugs somewhere.
@Gaëtan Gilbert the whole canonical mess is an attempt at applicativity
@Janno you live dangerously
I like to think of it as living succinctly.
but the whole point of using functors is so the reduction is reliable?
That seems like not an honest use of functors :innocent:
Yeah as far as motivations go it's pretty OK I suppose.
But I do agree with @Pierre-Marie Pédrot in that my use of functors is a workaround for missing features in Coq; although it's not quite clear what the best fix is, I think.
Pierre-Marie Pédrot said:
Gaëtan Gilbert the whole canonical mess is an attempt at applicativity
but canonical is about include and module aliases, not functor application
nope it's also about application
you apply a name substitution to the functor argument at application time
?
functor application is an indirect way to alias
I don't have a minimal example here, but it's easy to do if you define a module inside a functor that refers to an argument or a submodule of it
Coq will be able to tell you that applying the functor twice will result in convertible terms except if you hide the content
but it won't be able to track HO application
Théo Zimmermann said:
But isn't it precisely the idea behind the Lean statement that was quoted? The general notion of "namespace" would encompass many things, among them modules, records, etc.
How is this possible, without requiring unique identifiers everywhere?
I was just throwing ideas around. But I'm not sure I understand the issue you raise.
@janno I am curious. do you always use include Signature.
? It reminds me of the phd of Elie soubiran where he defines a module system where there is no difference between module signatures and module implementations (which makes sense in a dependently typed setting I suppose). https://tel.archives-ouvertes.fr/tel-00679201/document
For the record, and as far as I remember, the primary reason for parentheses was that projections were expected to possibly take explicit parameters (initial commit was 11a923b21b669d1a, for Coq version 8.0). For comparison, modules and qualified names were introduced earlier (in Coq 7.3.1). I don't think
As said above, there would have been no parsing issue but what rule to use for interpreting foo.bar
in general when foo
is both a variable and a module name would have been a bit delicate. With this respect, I'm particularly satisfied with the .(f)
syntax, which is moreover reminiscent of the selection of a component in an array or a string.
About parsing/printing primitive projections, the confusion will hopefully soon be resolved.
I meant: what restrictions on namespaces are necessary, to always be able to uniquely determine what a string foo0.foo1.foo2.foo3.foo4
refers to?
Adding primitive projections extends the set of possible strings "on the right" and adding modules extends the set of possible strings "on the left". And somewhere in the middle of such a string sits the identifier of a definition.
More fleshed out example:
Module A.
Record R :=
{ C : unit }.
Axiom foo : R.
End A.
Check (A.foo.(A.C)).
Definition A := nat.
As far as I can tell (which is just what was discussed) its impossible to "correctly" interpret A.foo.A.C
. The solution I thought of (I didn’t explain it clearly) is, that all definitions, modules and projections should have different identifiers. For example the definition of A := nat
wouldn’t be accepted. In this situation the interpretation of a string foo.foo.foo
would always be unique.
Right. I agree that this restriction would be needed, and IMHO it is a reasonable restriction to introduce. Just consider that every object, module, etc. defined in the same "namespace" must have a different name.
Stupid question: what's the overlap that's allowed today?
AFAIR the namespaces are [module, module type], [constant, inductive, constructor], [projection]
e.g. you can have a constant with the same name as a module, but not as an inductive
projections are handled a bit specially, but there is nothing in the kernel that prevents having a conflict
Pierre Courtieu said:
@janno I am curious. do you always use
include Signature.
? It reminds me of the phd of Elie soubiran where he defines a module system where there is no difference between module signatures and module implementations (which makes sense in a dependently typed setting I suppose). https://tel.archives-ouvertes.fr/tel-00679201/document
I also think this constructs is an (extremely inconvenient and half-baked) instance of mixin modules, on which there’s lots of literature, including Scala (in academia and now industry, like Coq) and MixML (a “cleaner” version of Scala’s idea, from researcher of the SML tradition).
The main limitation: Include
gives an error if you try combining an Axiom
with a Definition that instantiates it, instead of linking them together. The workaround is to split your code into lots of very small modules, but it’s very inconvenient. I’ll admit that if this worked like in Scala, you’d need to do termination-checking at Include
time.
For examples of this technique, see how the stdlib defines nat, N and Z.
Pierre-Marie Pédrot said:
AFAIR the namespaces are [module, module type], [constant, inductive, constructor], [projection]
projections are mixed with constants in practice, regardless of where in the code that's implemented
but the user can’t exploit this because projection also generate top-level constants, right?
so maybe your point is that the “primitive” projections live in a different namespace than their wrapper constants?
<this is why we can’t have nice things>
Last updated: Jun 05 2023 at 09:01 UTC