Ali Caglayan (Jul 05 2021 at 13:39): Ali Caglayan (Jul 05 2021 at 13:39):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.
Pierre-Marie Pédrot (Jul 05 2021 at 13:41):That's the same syntax as module qualification.
Pierre-Marie Pédrot (Jul 05 2021 at 13:42):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.
Ali Caglayan (Jul 05 2021 at 13:44):Is there a good reason for not having different syntactic classes?
Pierre-Marie Pédrot (Jul 05 2021 at 13:48):History.
Matthieu Sozeau (Jul 05 2021 at 14:14):Time to learn from it, maybe? :)
Pierre-Marie Pédrot (Jul 05 2021 at 14:17):I don't know. Did lean make the same error?
Pierre-Marie Pédrot (Jul 05 2021 at 14:18):(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.)
Gaëtan Gilbert (Jul 05 2021 at 14:19):Pierre-Marie Pédrot said:
I don't know. Did lean make the same error?
they don't have primitive projections
Pierre-Marie Pédrot (Jul 05 2021 at 14:19):Not yet, but what about qualifiers?
Pierre-Marie Pédrot (Jul 05 2021 at 14:20):AFAIK they don't have a syntactic difference between modules and term variables, so it's like in Coq.
Pierre-Marie Pédrot (Jul 05 2021 at 14:21):(it's not completely crazy though, since in presence of unicode getting a reasonable notion of caps is non-trivial.)
Pierre-Marie Pédrot (Jul 05 2021 at 14:22):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.
Gaëtan Gilbert (Jul 05 2021 at 14:26):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.
Ali Caglayan (Jul 05 2021 at 14:31):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?
Pierre-Marie Pédrot (Jul 05 2021 at 14:32):you'll break 200% of the developments and the fix is going to be a PITA for the end-users.
Guillaume Melquiond (Jul 05 2021 at 14:32):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.
Pierre-Marie Pédrot (Jul 05 2021 at 14:33):@Guillaume Melquiond no, because then you can't separate between a projection and a module field
Pierre-Marie Pédrot (Jul 05 2021 at 14:33):there is an ambiguity
Pierre-Marie Pédrot (Jul 05 2021 at 14:33):let me write down an example
Pierre-Marie Pédrot (Jul 05 2021 at 14:36):Module foo.
Module bar.
Definition qux := tt.
End bar.
End foo.
Record Qux := { qux : unit }
Record Bar := { bar : Qux }.
consider foo.bar.qux
Pierre-Marie Pédrot (Jul 05 2021 at 14:36):do you mean the projection or the module field?
Pierre-Marie Pédrot (Jul 05 2021 at 14:36):You can mix this in fancy ways, and I am pretty sure you can encode post correspondence problem with it.
Guillaume Melquiond (Jul 05 2021 at 14:37):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.
Pierre-Marie Pédrot (Jul 05 2021 at 14:38):I haven't said it was a problem with the parser specifically.
Pierre-Marie Pédrot (Jul 05 2021 at 14:38):but in OCaml the two are discriminated at parsing time by syntactic classes
Guillaume Melquiond (Jul 05 2021 at 14:39):So, what? We do not even distinguish constructors from pattern variables in Coq?
Pierre-Marie Pédrot (Jul 05 2021 at 14:39):if something on the LHS of a dot starts with an upper case it's a module qualification, otherwise it's a projection.
Pierre-Marie Pédrot (Jul 05 2021 at 14:39):so it's ambiguous.
Pierre-Marie Pédrot (Jul 05 2021 at 14:40):given how fragile name resolution is, mixing both syntaxes is gonna hurt
Pierre-Marie Pédrot (Jul 05 2021 at 14:40):we don't even have a way to refer to an absolute name.
Pierre-Marie Pédrot (Jul 05 2021 at 14:41):IIRC there are also issues with associativity of dot
Pierre-Marie Pédrot (Jul 05 2021 at 14:42):(ftr, the confusion in patterns between constructors and variables has bitten me too many times for me to believe this is feature)
Pierre-Marie Pédrot (Jul 05 2021 at 14:42):this is a poor design choice
Pierre-Marie Pédrot (Jul 05 2021 at 14:42):we can make it worse, yes.
Guillaume Melquiond (Jul 05 2021 at 14:46):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.
Pierre-Marie Pédrot (Jul 05 2021 at 14:49):If you can't reliably resolve names, you're looking for trouble. Coq is not your average programming language.
Guillaume Melquiond (Jul 05 2021 at 14:52):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.
Pierre-Marie Pédrot (Jul 05 2021 at 14:52):It's too late anyways.
Pierre-Marie Pédrot (Jul 05 2021 at 14:53):Do you claim that we should change the syntax for module qualification?
Pierre-Marie Pédrot (Jul 05 2021 at 14:54):Another issue with the dot syntax for projections is that it plays badly with non-primitive projections when you have to specify parameters
Pierre-Marie Pédrot (Jul 05 2021 at 14:55):if you unset implicit arguments for non-primitive pairs for instance, you'd have to write p.(fst _ _)
Ali Caglayan (Jul 05 2021 at 14:55):What is wrong with p.fst _ _ ?
Pierre-Marie Pédrot (Jul 05 2021 at 14:56):that does not mean the same
Pierre-Marie Pédrot (Jul 05 2021 at 14:56):p.fst _ _ would be the first projection of p applied to some arguments
Pierre-Marie Pédrot (Jul 05 2021 at 14:57):if we had primitive projections since the beginning I agree we wouldn't have had this issue
Guillaume Melquiond (Jul 05 2021 at 14:57):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.
Ali Caglayan (Jul 05 2021 at 14:57):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?
Pierre-Marie Pédrot (Jul 05 2021 at 14:57):@Guillaume Melquiond but then I don't understand your argument, if we already have to write parentheses in the applied case
Pierre-Marie Pédrot (Jul 05 2021 at 14:58):something I learned from the primitive projection mess is that you need to have a faithful way to print the contents of a term
Pierre-Marie Pédrot (Jul 05 2021 at 14:59):@Ali Caglayan backwards compat and some parts of the code handling badly pp
Pierre-Marie Pédrot (Jul 05 2021 at 15:00):@Guillaume Melquiond I am actively advocating for a third syntax to really mean pp
Pierre-Marie Pédrot (Jul 05 2021 at 15:00):we have currently a hodgepodge of bugs because there is a confusion between pp and the definition wrapper
Pierre-Marie Pédrot (Jul 05 2021 at 15:00):this is another reason for a syntax difference actually
Pierre-Marie Pédrot (Jul 05 2021 at 15:01):if you allow defining a constant with the same name as a pp, then there is no way to differentiate them in foo.bar
Pierre-Marie Pédrot (Jul 05 2021 at 15:01):did you mean bar the pp? the wrapper constant?
Pierre-Marie Pédrot (Jul 05 2021 at 15:01):(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)
Guillaume Melquiond (Jul 05 2021 at 15:02):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.
Pierre-Marie Pédrot (Jul 05 2021 at 15:02):OK, but then what about pp vs definition?
Pierre-Marie Pédrot (Jul 05 2021 at 15:02):you need to be able to display the difference to the user
Pierre-Marie Pédrot (Jul 05 2021 at 15:02):in OCaml it's clear what is a projection and what is a constant, once again because of syntactic classes
Pierre-Marie Pédrot (Jul 05 2021 at 15:03):Foo.bar is a constant, foo.bar is a projection
Pierre-Marie Pédrot (Jul 05 2021 at 15:03):but in Coq, I've lost hours of my life due to the ambiguity between both
Pierre-Marie Pédrot (Jul 05 2021 at 15:04):(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)
Pierre-Marie Pédrot (Jul 05 2021 at 15:05):so I have doubts that allowing to confuse both in more general cases is going to be helpful to the user
Pierre-Marie Pédrot (Jul 05 2021 at 15:05):(at least not without a way to print it faithfully)
Ali Caglayan (Jul 05 2021 at 15:05):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?
Pierre-Marie Pédrot (Jul 05 2021 at 15:06):uh
Pierre-Marie Pédrot (Jul 05 2021 at 15:06):anybody using lower case constructors must now rewrite their devs
Pierre-Marie Pédrot (Jul 05 2021 at 15:06):same thing for modules
Pierre-Marie Pédrot (Jul 05 2021 at 15:06):what if you used non-ascii letters in them?
Pierre-Marie Pédrot (Jul 05 2021 at 15:06):(at least for the leading one)
Pierre-Marie Pédrot (Jul 05 2021 at 15:07):you probably don't pass Coq.Init
Ali Caglayan (Jul 05 2021 at 15:07):Oh, I see so the idea is to use case to distinguish modules and terms
Pierre-Marie Pédrot (Jul 05 2021 at 15:08):that's what OCaml does, I am not suggesting this has a micro-ounce of realism in Coq
Ali Caglayan (Jul 05 2021 at 15:09):OK, so here is a dumb idea: What if record terms became modules themselves? Sort of unifying the dot syntax?
Pierre-Marie Pédrot (Jul 05 2021 at 15:09):nope
Pierre-Marie Pédrot (Jul 05 2021 at 15:10):nope nope nope
Pierre-Marie Pédrot (Jul 05 2021 at 15:10):module typing is a minefield
Pierre-Marie Pédrot (Jul 05 2021 at 15:10):outside of term typing
Pierre-Marie Pédrot (Jul 05 2021 at 15:11):the last thing you want is more modules
Pierre-Marie Pédrot (Jul 05 2021 at 15:12):(I mean, this does not even make sense, module typing lives above term typing.)
Pierre-Marie Pédrot (Jul 05 2021 at 15:13):(you can't quantify over modules in a term, and functors are probably ridden with soundness issues anyways)
Théo Zimmermann (Jul 05 2021 at 15:16):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.
Théo Zimmermann (Jul 05 2021 at 15:17):This doesn't mean making records modules though :smile:
Pierre-Marie Pédrot (Jul 05 2021 at 15:24):A functor blocks your path.
Ali Caglayan (Jul 05 2021 at 15:30):Where do people use module functors?
Pierre-Marie Pédrot (Jul 05 2021 at 15:31):You mean, in general as a design pattern, or in particular developments,
Ali Caglayan (Jul 05 2021 at 15:31):The latter
Pierre-Marie Pédrot (Jul 05 2021 at 15:31):the stdlib uses it
Pierre-Marie Pédrot (Jul 05 2021 at 15:32):color abuses functors in creative ways
Pierre-Marie Pédrot (Jul 05 2021 at 15:32):I think iris also relies on them
Pierre-Marie Pédrot (Jul 05 2021 at 15:33):they're good "weapons of mass abstraction" but they're really outlandish in Coq
Pierre-Marie Pédrot (Jul 05 2021 at 15:33):there are many non-kernel "issues" with functors (they can become features if you squint enough)
Janno (Jul 05 2021 at 15:34):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.
Pierre-Marie Pédrot (Jul 05 2021 at 15:35):yes, typical use of functors as workarounds to unrelated issues :/
Pierre-Marie Pédrot (Jul 05 2021 at 15:35):out of curiosity, what reduction are you using?
Pierre-Marie Pédrot (Jul 05 2021 at 15:36):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
Janno (Jul 05 2021 at 15:36):Usually cbn with infrequent calls to simpl inbetween because cbn doesn't quite suffice.
Janno (Jul 05 2021 at 15:36):My functors have signatures
Pierre-Marie Pédrot (Jul 05 2021 at 15:37):ok, so that's the safe fragment
Pierre-Marie Pédrot (Jul 05 2021 at 15:37):for the uninformed, there is a huge confusion in the upper layers regarding the so-called "canonical names"
Pierre-Marie Pédrot (Jul 05 2021 at 15:38):canonical names are a way to guarantee some form of name quotient resulting from functor application / module inclusion
Pierre-Marie Pédrot (Jul 05 2021 at 15:38):so, precisely a way to be applicative, not generative
Pierre-Marie Pédrot (Jul 05 2021 at 15:39):this is ill-designed because it does not work for higher-order functors, but for Pi 0 1 it's reasonable enough
Pierre-Marie Pédrot (Jul 05 2021 at 15:39):the problem is that it relies on kernel names being implemented as a pair of names canonical / user
Pierre-Marie Pédrot (Jul 05 2021 at 15:39):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
Pierre-Marie Pédrot (Jul 05 2021 at 15:40):some parts of the code use user, some use canonical
Pierre-Marie Pédrot (Jul 05 2021 at 15:40):so we have a borken quotient
Pierre-Marie Pédrot (Jul 05 2021 at 15:41):even without taking soundness into considerations, this is very problematic for tactics, unification and whatnot
Pierre-Marie Pédrot (Jul 05 2021 at 15:41):hints, for instance
Gaëtan Gilbert (Jul 05 2021 at 15:42):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
Janno (Jul 05 2021 at 15:43):All my functor bodies are actually Include SIGNATURE. so I am sure that I am relying on bugs somewhere.
Pierre-Marie Pédrot (Jul 05 2021 at 15:44):@Gaëtan Gilbert the whole canonical mess is an attempt at applicativity
Pierre-Marie Pédrot (Jul 05 2021 at 15:44):@Janno you live dangerously
Janno (Jul 05 2021 at 15:44):I like to think of it as living succinctly.
Ali Caglayan (Jul 05 2021 at 15:44):but the whole point of using functors is so the reduction is reliable?
Ali Caglayan (Jul 05 2021 at 15:45):That seems like not an honest use of functors :innocent:
Janno (Jul 05 2021 at 15:46):Yeah as far as motivations go it's pretty OK I suppose.
Janno (Jul 05 2021 at 15:47):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.
Gaëtan Gilbert (Jul 05 2021 at 15:47):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
Pierre-Marie Pédrot (Jul 05 2021 at 15:49):nope it's also about application
Pierre-Marie Pédrot (Jul 05 2021 at 15:49):you apply a name substitution to the functor argument at application time
Gaëtan Gilbert (Jul 05 2021 at 15:50):?
Pierre-Marie Pédrot (Jul 05 2021 at 15:51):functor application is an indirect way to alias
Pierre-Marie Pédrot (Jul 05 2021 at 15:52):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
Pierre-Marie Pédrot (Jul 05 2021 at 15:52):Coq will be able to tell you that applying the functor twice will result in convertible terms except if you hide the content
Pierre-Marie Pédrot (Jul 05 2021 at 15:53):but it won't be able to track HO application
Stéphane Desarzens (Jul 05 2021 at 15:53):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?
Théo Zimmermann (Jul 05 2021 at 16:05):I was just throwing ideas around. But I'm not sure I understand the issue you raise.
Pierre Courtieu (Jul 05 2021 at 16:17):@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
Hugo Herbelin (Jul 06 2021 at 08:24):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.
Stéphane Desarzens (Jul 06 2021 at 10:26):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.
Théo Zimmermann (Jul 06 2021 at 11:30):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.
Paolo Giarrusso (Jul 06 2021 at 15:06):Stupid question: what's the overlap that's allowed today?
Pierre-Marie Pédrot (Jul 06 2021 at 15:13):AFAIR the namespaces are [module, module type], [constant, inductive, constructor], [projection]
Pierre-Marie Pédrot (Jul 06 2021 at 15:14):e.g. you can have a constant with the same name as a module, but not as an inductive
Pierre-Marie Pédrot (Jul 06 2021 at 15:16):projections are handled a bit specially, but there is nothing in the kernel that prevents having a conflict
Paolo Giarrusso (Jul 06 2021 at 15:29):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.
Paolo Giarrusso (Jul 06 2021 at 15:30):For examples of this technique, see how the stdlib defines nat, N and Z.
Gaëtan Gilbert (Jul 06 2021 at 15:32):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
Paolo Giarrusso (Jul 06 2021 at 15:39):but the user can’t exploit this because projection also generate top-level constants, right?
Paolo Giarrusso (Jul 06 2021 at 15:40):so maybe your point is that the “primitive” projections live in a different namespace than their wrapper constants?
Paolo Giarrusso (Jul 06 2021 at 15:40):<this is why we can’t have nice things>
Last updated: Apr 19 2024 at 10:02 UTC