Stream: Coq devs & plugin devs

Topic: What is the reason for the `p.(f)` syntax?


view this post on Zulip Matthieu Sozeau (Jul 05 2021 at 14:14):

Time to learn from it, maybe? :)

view this post on Zulip Pierre-Marie Pédrot (Jul 05 2021 at 14:17):

I don't know. Did lean make the same error?

view this post on Zulip 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.)

view this post on Zulip 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

view this post on Zulip Pierre-Marie Pédrot (Jul 05 2021 at 14:19):

Not yet, but what about qualifiers?

view this post on Zulip 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.

view this post on Zulip 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.)

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Pierre-Marie Pédrot (Jul 05 2021 at 14:33):

there is an ambiguity

view this post on Zulip Pierre-Marie Pédrot (Jul 05 2021 at 14:33):

let me write down an example

view this post on Zulip 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 }.

view this post on Zulip Pierre-Marie Pédrot (Jul 05 2021 at 14:36):

consider foo.bar.qux

view this post on Zulip Pierre-Marie Pédrot (Jul 05 2021 at 14:36):

do you mean the projection or the module field?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Pierre-Marie Pédrot (Jul 05 2021 at 14:38):

I haven't said it was a problem with the parser specifically.

view this post on Zulip Pierre-Marie Pédrot (Jul 05 2021 at 14:38):

but in OCaml the two are discriminated at parsing time by syntactic classes

view this post on Zulip Guillaume Melquiond (Jul 05 2021 at 14:39):

So, what? We do not even distinguish constructors from pattern variables in Coq?

view this post on Zulip 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.

view this post on Zulip Pierre-Marie Pédrot (Jul 05 2021 at 14:39):

so it's ambiguous.

view this post on Zulip Pierre-Marie Pédrot (Jul 05 2021 at 14:40):

given how fragile name resolution is, mixing both syntaxes is gonna hurt

view this post on Zulip Pierre-Marie Pédrot (Jul 05 2021 at 14:40):

we don't even have a way to refer to an absolute name.

view this post on Zulip Pierre-Marie Pédrot (Jul 05 2021 at 14:41):

IIRC there are also issues with associativity of dot

view this post on Zulip 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)

view this post on Zulip Pierre-Marie Pédrot (Jul 05 2021 at 14:42):

this is a poor design choice

view this post on Zulip Pierre-Marie Pédrot (Jul 05 2021 at 14:42):

we can make it worse, yes.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Pierre-Marie Pédrot (Jul 05 2021 at 14:52):

It's too late anyways.

view this post on Zulip Pierre-Marie Pédrot (Jul 05 2021 at 14:53):

Do you claim that we should change the syntax for module qualification?

view this post on Zulip 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

view this post on Zulip 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 _ _)

view this post on Zulip Ali Caglayan (Jul 05 2021 at 14:55):

What is wrong with p.fst _ _ ?

view this post on Zulip Pierre-Marie Pédrot (Jul 05 2021 at 14:56):

that does not mean the same

view this post on Zulip Pierre-Marie Pédrot (Jul 05 2021 at 14:56):

p.fst _ _ would be the first projection of p applied to some arguments

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Pierre-Marie Pédrot (Jul 05 2021 at 14:59):

@Ali Caglayan backwards compat and some parts of the code handling badly pp

view this post on Zulip Pierre-Marie Pédrot (Jul 05 2021 at 15:00):

@Guillaume Melquiond I am actively advocating for a third syntax to really mean pp

view this post on Zulip 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

view this post on Zulip Pierre-Marie Pédrot (Jul 05 2021 at 15:00):

this is another reason for a syntax difference actually

view this post on Zulip 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

view this post on Zulip Pierre-Marie Pédrot (Jul 05 2021 at 15:01):

did you mean bar the pp? the wrapper constant?

view this post on Zulip 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)

view this post on Zulip 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.

view this post on Zulip Pierre-Marie Pédrot (Jul 05 2021 at 15:02):

OK, but then what about pp vs definition?

view this post on Zulip Pierre-Marie Pédrot (Jul 05 2021 at 15:02):

you need to be able to display the difference to the user

view this post on Zulip 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

view this post on Zulip Pierre-Marie Pédrot (Jul 05 2021 at 15:03):

Foo.bar is a constant, foo.bar is a projection

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip Pierre-Marie Pédrot (Jul 05 2021 at 15:05):

(at least not without a way to print it faithfully)

view this post on Zulip 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?

view this post on Zulip Pierre-Marie Pédrot (Jul 05 2021 at 15:06):

uh

view this post on Zulip Pierre-Marie Pédrot (Jul 05 2021 at 15:06):

anybody using lower case constructors must now rewrite their devs

view this post on Zulip Pierre-Marie Pédrot (Jul 05 2021 at 15:06):

same thing for modules

view this post on Zulip Pierre-Marie Pédrot (Jul 05 2021 at 15:06):

what if you used non-ascii letters in them?

view this post on Zulip Pierre-Marie Pédrot (Jul 05 2021 at 15:06):

(at least for the leading one)

view this post on Zulip Pierre-Marie Pédrot (Jul 05 2021 at 15:07):

you probably don't pass Coq.Init

view this post on Zulip Ali Caglayan (Jul 05 2021 at 15:07):

Oh, I see so the idea is to use case to distinguish modules and terms

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip Pierre-Marie Pédrot (Jul 05 2021 at 15:09):

nope

view this post on Zulip Pierre-Marie Pédrot (Jul 05 2021 at 15:10):

nope nope nope

view this post on Zulip Pierre-Marie Pédrot (Jul 05 2021 at 15:10):

module typing is a minefield

view this post on Zulip Pierre-Marie Pédrot (Jul 05 2021 at 15:10):

outside of term typing

view this post on Zulip Pierre-Marie Pédrot (Jul 05 2021 at 15:11):

the last thing you want is more modules

view this post on Zulip Pierre-Marie Pédrot (Jul 05 2021 at 15:12):

(I mean, this does not even make sense, module typing lives above term typing.)

view this post on Zulip 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)

view this post on Zulip 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.

view this post on Zulip Théo Zimmermann (Jul 05 2021 at 15:17):

This doesn't mean making records modules though :smile:

view this post on Zulip Pierre-Marie Pédrot (Jul 05 2021 at 15:24):

A functor blocks your path.

view this post on Zulip Ali Caglayan (Jul 05 2021 at 15:30):

Where do people use module functors?

view this post on Zulip Pierre-Marie Pédrot (Jul 05 2021 at 15:31):

You mean, in general as a design pattern, or in particular developments,

view this post on Zulip Ali Caglayan (Jul 05 2021 at 15:31):

The latter

view this post on Zulip Pierre-Marie Pédrot (Jul 05 2021 at 15:31):

the stdlib uses it

view this post on Zulip Pierre-Marie Pédrot (Jul 05 2021 at 15:32):

color abuses functors in creative ways

view this post on Zulip Pierre-Marie Pédrot (Jul 05 2021 at 15:32):

I think iris also relies on them

view this post on Zulip Pierre-Marie Pédrot (Jul 05 2021 at 15:33):

they're good "weapons of mass abstraction" but they're really outlandish in Coq

view this post on Zulip 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)

view this post on Zulip 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.

view this post on Zulip Pierre-Marie Pédrot (Jul 05 2021 at 15:35):

yes, typical use of functors as workarounds to unrelated issues :/

view this post on Zulip Pierre-Marie Pédrot (Jul 05 2021 at 15:35):

out of curiosity, what reduction are you using?

view this post on Zulip 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

view this post on Zulip Janno (Jul 05 2021 at 15:36):

Usually cbn with infrequent calls to simpl inbetween because cbn doesn't quite suffice.

view this post on Zulip Janno (Jul 05 2021 at 15:36):

My functors have signatures

view this post on Zulip Pierre-Marie Pédrot (Jul 05 2021 at 15:37):

ok, so that's the safe fragment

view this post on Zulip 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"

view this post on Zulip 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

view this post on Zulip Pierre-Marie Pédrot (Jul 05 2021 at 15:38):

so, precisely a way to be applicative, not generative

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Pierre-Marie Pédrot (Jul 05 2021 at 15:40):

some parts of the code use user, some use canonical

view this post on Zulip Pierre-Marie Pédrot (Jul 05 2021 at 15:40):

so we have a borken quotient

view this post on Zulip 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

view this post on Zulip Pierre-Marie Pédrot (Jul 05 2021 at 15:41):

hints, for instance

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Pierre-Marie Pédrot (Jul 05 2021 at 15:44):

@Gaëtan Gilbert the whole canonical mess is an attempt at applicativity

view this post on Zulip Pierre-Marie Pédrot (Jul 05 2021 at 15:44):

@Janno you live dangerously

view this post on Zulip Janno (Jul 05 2021 at 15:44):

I like to think of it as living succinctly.

view this post on Zulip Ali Caglayan (Jul 05 2021 at 15:44):

but the whole point of using functors is so the reduction is reliable?

view this post on Zulip Ali Caglayan (Jul 05 2021 at 15:45):

That seems like not an honest use of functors :innocent:

view this post on Zulip Janno (Jul 05 2021 at 15:46):

Yeah as far as motivations go it's pretty OK I suppose.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Pierre-Marie Pédrot (Jul 05 2021 at 15:49):

nope it's also about application

view this post on Zulip Pierre-Marie Pédrot (Jul 05 2021 at 15:49):

you apply a name substitution to the functor argument at application time

view this post on Zulip Gaëtan Gilbert (Jul 05 2021 at 15:50):

?

view this post on Zulip Pierre-Marie Pédrot (Jul 05 2021 at 15:51):

functor application is an indirect way to alias

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Pierre-Marie Pédrot (Jul 05 2021 at 15:53):

but it won't be able to track HO application

view this post on Zulip Columbus (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?

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Columbus (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.

view this post on Zulip 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.

view this post on Zulip Paolo Giarrusso (Jul 06 2021 at 15:06):

Stupid question: what's the overlap that's allowed today?

view this post on Zulip Pierre-Marie Pédrot (Jul 06 2021 at 15:13):

AFAIR the namespaces are [module, module type], [constant, inductive, constructor], [projection]

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Paolo Giarrusso (Jul 06 2021 at 15:30):

For examples of this technique, see how the stdlib defines nat, N and Z.

view this post on Zulip 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

view this post on Zulip Paolo Giarrusso (Jul 06 2021 at 15:39):

but the user can’t exploit this because projection also generate top-level constants, right?

view this post on Zulip 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?

view this post on Zulip Paolo Giarrusso (Jul 06 2021 at 15:40):

<this is why we can’t have nice things>


Last updated: Oct 21 2021 at 20:02 UTC