Document on primitive projections

[herbelin]

This CEPS is to adopt a strategy with respect to the different paths followed by primitive projections.

Rendered here

Feel free to edit, refine, extend.

[maximedenes]

Thanks for initiating a CEP on this topic! Here's some feedback.

Issue 1: I'd introduce a specific syntax for Proj-based projections. It could be x.(f) or something else. Side question: why do you write params? I though they were not present in the term, for primitive projections.

So essentially, something very close to design choice 1.

Issue 2: Indeed, dropping the unfold boolean seems good. Why not error on attempts to unfold projections, rather than a noop?

Issue 3: Can you elaborate on "it is enough to extend the conversion with eta-expansions of match into projections"? I'm wondering if we shouldn't forbid matches over primitive records.

Issue 4: I would simply forbid the projection syntax for general applications. As I wrote above, this syntax could be different from t.(f args)

Issue 5: the motivation wasn't clear to m e when I first read. How about adding an example type?

[SkySkimmer]

Side question: why do you write params? I though they were not present in the term, for primitive projections.

They can be useful in the input syntax for inference. For instance Definition f' params x := x.(f params) works even tough there are no type annotations.

[maximedenes]

Why not write Definition f' params (x : R params) := x.(f) in this case? I.e. putting type annotations should work reasonably ok, no?

I had the feeling that having discrepancies between user syntax and terms, like here ghost subterms had proven often painful in the past.

[SkySkimmer]

What does positive/negative mean precisely?

[Alizter]

I guess the constructor vs destructor variants of coinductive types. I'm not really sure primitive projections make sense for positive coinductive types? They don't make sense for inductive types right?

[herbelin]

Projections make sense for positive records as macro-definitions, as it has been for a long time in Coq. So, the answer depends on which component of "primitive" projections you are talking about. If you are talking about the compact representation, it makes sense to represent the defined projections of positive record types using a dedicated compact Proj node, even if thought as macros, i.e. not as a primitive ingredient of positive record types.

[SkySkimmer]

Keep in mind that if the record has eta then

Record R := r { A : Type; B : Type }.
Check fun x (f : match x with r a b => a -> b end) a b => f a b.

must somehow reduce the match on a variable. ie we cannot have Case be a normal form when it is on a type which has eta.

Conversely we can have projections with omitted parameters for types without eta, this is already the case for some coinductives. AFAIK it would work fine to allow both primitive projections and primitive match for non-eta inductives, they just wouldn't be convertible with each other.

[herbelin]

Record R := r { A : Type; B : Type }.
Check fun x (f : match x with r a b => a -> b end) a b => f a b.

must somehow reduce the match on a variable.

Ah, interesting, this is a place where reduction rather than conversion is needed. So, something special to take care of match commutation would have to be done here.

Conversely we can have projections with omitted parameters for types without eta, this is already the case for some coinductives. AFAIK it would work fine to allow both primitive projections and primitive match for non-eta inductives, they just wouldn't be convertible with each other.

Then, is the equational theory of record types without eta but with projections and match clear to you? Is it just about removing t ≣ (fst t, snd t) but keeping the commutation match t as z return P with (x,y) => v end ≣ v[x:=fst t][y:=snd t]?

[SkySkimmer]

Then, is the equational theory of record types without eta but with projections and match clear to you? Is it just about removing t ≣ (fst t, snd t) but keeping the commutation match t as z return P with (x,y) => v end ≣ v[x:=fst t][y:=snd t]?

No, this commutation is not well-typed without eta.

[herbelin]

Ah, right. Do we then need baclofen-style restrictions on the form of P?

[SkySkimmer]

Why not write Definition f' params (x : R params) := x.(f) in this case? I.e. putting type annotations should work reasonably ok, no?

It's also a rather simple example compared to some of the terms people write.

BTW Definition f' params x := (x : R params).(f) is a closer translation (in general we don't project variables so this is the only place to put the type annotation). I guess that looks reasonably convenient?

[herbelin]

Thanks for initiating a CEP on this topic!

Thanks for the feeback!

Issue 1: I'd introduce a specific syntax for Proj-based projections. It could be x.(f) or something else. Side question: why do you write params? I though they were not present in the term, for primitive projections.

There are the reasons given by @SkySkimmer.

There is also the question of compatibility. It is years that the notation x.(f params) is provided and that would be a serious change to now expect only x.(f).

Additionally, with implicit arguments, it is easy to simulate x.(f). So, what can the more can also the less.

Issue 2: Indeed, dropping the unfold boolean seems good. Why not error on attempts to unfold projections, rather than a noop?

If we want to be as compatible as possible with the developments using non primitive records so that they behave as much as possible like before when the primitive attribute is activated, it might be convenient not to error on existing unfolds (but see below).

Issue 3: Can+ you elaborate on "it is enough to extend the conversion with eta-expansions of match into projections"? I'm wondering if we shouldn't forbid matches over primitive records.

I suspect that there would be no harm in providing a Case node also in the case of negative records (i.e. types with destructor-based normal forms). This Case node, i.e. typically match t as z return P with (x,y) => v end, could be thought as a shortening for v[x:=fst t][y:=snd t], and that's how it would behave in the conversion.

By beta, match (t,u) as z return P with (x,y) => v end would primitively reduce to v[x:=t][y:=u] as its intended expansion would.

An advantage is that code working without the primitive attribute would work more similarly when the primitive attribute is set. Note that it is not a compatibility mode though. No flags are involved, it is just that a match kernel node is also supported for negative records.

Issue 4: I would simply forbid the projection syntax for general applications. As I wrote above, this syntax could be different from t.(f args)

We could do that. With a script, it would probably be easy to change the existing occurrences of t.(f args) when f is not a projection into a different syntax.

Issue 5: the motivation wasn't clear to me when I first read. How about adding an example type?

The point here is that I suspect that there is no reason at the end to bind the attribute primitive to the concept of negative record rather than to the concept of compact representation of enough-applied projections. We are already used to having projections in positive record types and there is no reason not to represent the enough-applied projections in positive records in a compact way too.

The logical view at negative types is that they are based on pairing and projections but match is definable with the same reduction rules as in positive records. The logical view at positive types is that they are based on pairing and a destructing let but projections are definable with the same reduction rules as in negative records.

So, there is a unifying view where positive and negative records have both pairing (a Construct node), have both compact enough-applied projections (a Proj node), have both partially applied projections (a Const node of same name), have both a destructing let (a Case node), have both the beta rule match (t,u) as z return P with (x,y) => v end -> v[x:=t][y:=u], have both projection reduction rules (t,u).(fst) -> t and (t,u).(snd) -> u, have both an eta-conversion for destructing let match t as z return P with (x,y) => v end ≣v[x:=fst t][y:=snd t], have both an eta-conversion for projections t ≣ (fst t, snd t). The only difference in theory is that match t as z return P with (x,y) => v end is a macro that evaluates to v[x:=fst t][y:=snd t] in the negative case even when t is not reducible to constructor form, while fst and snd are macros that delta-evaluates in theory to a match in the positive case even when their argument is not reducible to constructor form. These extra reductions which make a difference between the negative and positive views are not needed for the conversion. They matter only when evaluating or reducing non closed expressions and it would probably be worth to reconsider which of these reductions are really useful in practice.

[SkySkimmer]

Probably issue 5 should be a separate CEP

[SkySkimmer]

I think there is a sub choice of whether the projection names exist in the same namespace as constants, or if they're in different namespaces in which case the name can be reused.

[ppedrot]

This choice is linked to the dedicated projection syntax choice. If you have a syntax t.(p) that allows non-primitive projections, whatever the details, then there is an ambiguity.

[SkySkimmer]

A possible system: suppose we allow a.(b) for any application b a, with some table of refs which use that syntax for printing. Meanwhile we have some other syntax PRIMPROJ(p,x) for primitive projections.

Then it is possible to do Notation p' x := (PRIMPROJ(p,x)). and register p', then completely ignore the primitive syntax. Maybe we could even allow calling the notation p.

[Blaisorblade]

BTW Definition f' params x := (x : R params).(f) is a closer translation (in general we don't project variables so this is the only place to put the type annotation). I guess that looks reasonably convenient?

I think you meant to write a pure in-term type ascription that does not leave AST residues, but Coq's term ::= (term : type) constructor is no such thing, and type arguments are what we use instead.
While it's not common to be bitten by this, I hope we can generalize from experience and agree that Coq users need control of every bit of the AST, probably through syntax that is isomorphic to the AST.

[herbelin]

For the record, I added a 2nd design choice in issue 3 about forbidding any form of match on primitive records. I also expanded the unfold issue. About concrete syntax, I don't know what to conclude from the comments. Are there precise alternative proposals to add?

[herbelin]

@mattam82, would you like to say something?

[herbelin]

I wonder how to proceed next.

• We could try to remove match on primitive records and see how much incompatibilities it induces?
• We could try to remove the "unfolded" boolean flag of Proj nodes and see how much incompatibilities it induces? E.g.:

  Set Primitive Projections.
  Record R A := {f:A}.
  Lemma L x : x.(f nat) = 0.
  destruct x.
  (* Showing "d _ {| d := d0 |} = 0" vs directly iota-reducing into "d0 = 0" *)

• We could try removing any Const proj applied to enough arguments, so that it uses instead a Proj (via mkApp). What kind of incompatibilities would there be? E.g. would differences like the following be problematic:

  Set Primitive Projections.
  Record R A := {f:A}.
  Lemma L x : (fun x : Type => f x) nat x = 0.
  simpl.
  (* "f nat x = 0" vs directly going to a compact form "f _ x = 0" *)

Any suggestions on what to do concretely?

[ppedrot]

FTR, I am strongly opposed to adding more quotients as smart constructors in the kernel. We currently have two of those, namely:

• Automatic concatenation of application nodes.
• Collapse of cast nodes.

The first one is reasonable because it's an isomorphism. The second one less so, because it implicitly erases information from the term.

As a general principle, I believe that quotienting ASTs is a very bad practice. It makes reasoning about them harder, and interferes with higher-level abstractions. We already have to rebuild the abstraction in EConstr in order to transparently respect the same invariants in presence of evars, but even that is broken by evar instantiation (i.e. casts might disappear). There are probably other similar issues in the code but we're not aware of them because casts already have a strong tendency to disappear silently.

Doing the same thing with projections would make the situation even worse. Just like casts, the quotient you propose is lossy, so by applying a term you can make information disappear. This can silently hide ill-typed data (e.g. you have broken parameters but since the projection is fully applied they magically disappear) and it would also interfere with evars.

ASTs ought to be what they claim to be, i.e. trees, not semantical objects that have some built-in non-trivial equations. Otherwise, we wouldn't we also include full strong normalization in the smart constructors?

[herbelin]

About how much the concrete syntax can differ from internal representation, I think that I agree that there should be a mode (i.e. at least with Set Printing All extended with universes and existential instances printing) where we can display the internal representation explicitly.

About primitive projections, are you proposing a "design choice" 2.3 which at the time a record with projection name f is declared, do the following:

• provides the ability to use compact Proj(f,c) nodes with concrete syntax c.(f _) (that is c.(f) when parameters are declared implicit)
• defines a constant Const(f) bound to fun params c => c.(f _) with concrete notation f and with non-compact representation App(Const(f),[|params;c|]) whose concrete notation is itself f params c

About compatibility, does this mean that all usages of f params c which currently go to Proj(f,c) would then go instead to App(Const(f),[|params;c|]) hoping that it works almost observationally the same, telling users to use instead c.(f params) if they really want the compact representation?

Regarding the compatibility for records not tagged as primitive, is the syntax c.(f params) disallowed? Is it kept as an alias for f params c? Or is the plan to have a new notation say c.[f] for the compact representation of projections in records tagged as primitive so that it does not interfere with the current usages?

Would it mean also keeping all current code which equates App(Const(f),[|params;c|]) and Proj(f,c) in unification, pattern-matching, notations, etc. or the plan would instead to invite users to make a clear and explicit difference between f params c and c.(f _)?

[ppedrot]

I've already stated it several times around before, but assuming we want to preserve f.(p) for arbitrary applications (which is reasonable given that otherwise it'd be a serious backwards incompatible change) we desperately need a faithful way to display primitive projections to the user. The issues people have experienced so far is not so much a change of semantics rather than an utter confusion at things displayed the same (notably, the folded flag and the proj vs app distinction). Therefore, we must introduce a new syntax that will unambiguously represent Proj.

[SkySkimmer]

Someone needs to unilaterally decide the new syntax or it will stay in bikeshedding mode.

[herbelin]

we desperately need a faithful way to display primitive projections to the user.

This is what #14640 is doing: Proj nodes are bound to c.(f) and App(Const(f),...) nodes to f ..., so when f is a primitive projection, the concrete display faithfully reflects the internal representation.

Or is it that you would like more, e.g. that the notation c.(f) is used exclusively for f the name of a projection in a primitive record, and not only to discriminate between a compact and non-compact use of projections in primitive records?

[ppedrot]

#14640 is incomparable to what I am saying, since part of it is a prerequisite and part of it is unrelated. My proposal is just that we print Proj nodes with a unique syntax different from anything we've been using so far. Obviously it requires preserving those nodes as far as possible inside constr_expr when detyping, but it has no other effects on the runtime.

[herbelin]

My proposal is just that we print Proj nodes with a unique syntax different from anything we've been using so far.

Do you already have in mind a new syntax that could be added to the document? Also what are your plans about existing uses of the x.(f) notation in primitive records at parsing time?

[silene]

We could try to remove match on primitive records and see how much incompatibilities it induces?

I think it is a bad idea. Not only would it break existing code that use primitive projections (as you mentioned), but it would also make it much harder for users to test whether they can switch their code to primitive projections.

We could try to remove the "unfolded" boolean flag of Proj nodes and see how much incompatibilities it induces?

This seems like a better way forward.

[herbelin]

We could try to remove the "unfolded" boolean flag of Proj nodes and see how much incompatibilities it induces?

This seems like a better way forward.

This is somehow what I started in coq/coq#14640 (in addition to print Proj as .( ) and Const as an application). If we continue to equate App(Const(f),[|params;c|]) and Proj(f,c) in unification, pattern-matching, notations, etc. it seems feasible.

[silene]

By the way, it seems there is a design decision you did not consider (or I missed it):

• forbid partially applied primitive projections.

The syntax f params c would still be allowed as syntactic sugar for c.(f params) for forward compatibility. But Const(f) would no longer exist (and neither App(Const(f), ...) as a consequence).

So, it is a variant of your design choice 1 for issue 1.

It would not hinder forward compatibility much, as partially applied projections are rather uncommon, in my experience.

[herbelin]

@silene

So, it is a variant of your design choice 1 for issue 1.

I added 4 new subchoices of choice 1 to make the different possibilities more explicit. @ppedrot's one is 1.2 (as far as I understood). Yours is 1.4. As for the current state of coq/coq#14640, it is halfway between 1.4 and 2.1 (since the current implementation is more on the side of choice 2).

as partially applied projections are rather uncommon, in my experience.

A typical use of partially applied projections is e.g. in List.map f r for a field f having its implicit parameters inserted maximally. But I agree that this can easily be overcome with an expansion.

[Blaisorblade]

Not only would it break existing code that use primitive projections (as you mentioned), but it would also make it much harder for users to test whether they can switch their code to primitive projections.

That’s only true if users are writing those matches by hand (personally never seen that), but more generally, many existing clients have to use 100% of the existing semantics even if they don’t want to. For instance, to work around the existence of wrappers and their semantics, one must often unfold them.

So I was expecting a fresh flag, Set New Primitive Projections. for the new behavior — a fresh design for records with eta without the current compatibility layer. I suspect one might want an option to disable iota-reduction for those via Arguments, as long as that’s not done via folded projections.

[silene]

That’s only true if users are writing those matches by hand (personally never seen that)

As a point of data, there are 93 such match constructs in CoqInterval and 102 in Flocq. But maybe I am an exception and users do not match over records?

[herbelin]

@Blaisorblade

So I was expecting a fresh flag, Set New Primitive Projections. for the new behavior — a fresh design for records with eta without the current compatibility layer. I suspect one might want an option to disable iota-reduction for those via Arguments, as long as that’s not done via folded projections.

Could you give an example of what would be useful for you in case of change of semantics of primitive projections, e.g. a typical situation where you'd like to control iota or have a "new" flag?

[Blaisorblade]

As a point of data, there are 93 such match constructs in CoqInterval and 102 in Flocq. But maybe I am an exception and users do not match over records?

My anecdata is no stronger.

Could you give an example of what would be useful for you in case of change of semantics of primitive projections, e.g. a typical situation where you'd like to control iota or have a "new" flag?

For instance if I have a lemma about the projection. That makes sense for both CS and TCs — if g : Group we might want @add g a b = @add g b a to keep working after simpl. E.g. iris uses this for bi (cc @robbertkrebbers):

https://gitlab.mpi-sws.org/iris/iris/-/blob/95df9887ecd331923ac57345e30d5a35b708c1bc/iris/bi/interface.v#L4
https://gitlab.mpi-sws.org/iris/iris/-/blob/95df9887ecd331923ac57345e30d5a35b708c1bc/iris/bi/interface.v#L162-184
https://gitlab.mpi-sws.org/iris/iris/-/blob/95df9887ecd331923ac57345e30d5a35b708c1bc/iris/bi/interface.v#L205-219

IIUC, the "folded" flag on projections exist to support (1) this scenario (2) "perfect" compatibility with cbv beta delta [projection]. I hope that (1) can be supported somehow, but I conjecture a fresh flag could make sense if you want low-level control.

[gmalecha]

It would be nice if the terms were syntactically equal so that hash-consing and the like would identify these terms.

[herbelin]

@Blaisorblade

For instance if I have a lemma about the projection. That makes sense for both CS and TCs — if g : Group we might want @add g a b = @add g b a to keep working after simpl. E.g. iris uses this for bi (cc @robbertkrebbers):

https://gitlab.mpi-sws.org/iris/iris/-/blob/95df9887ecd331923ac57345e30d5a35b708c1bc/iris/bi/interface.v#L4
https://gitlab.mpi-sws.org/iris/iris/-/blob/95df9887ecd331923ac57345e30d5a35b708c1bc/iris/bi/interface.v#L162-184
https://gitlab.mpi-sws.org/iris/iris/-/blob/95df9887ecd331923ac57345e30d5a35b708c1bc/iris/bi/interface.v#L205-219

IIUC, the "folded" flag on projections exist to support (1) this scenario (2) "perfect" compatibility with cbv beta delta [projection]. I hope that (1) can be supported somehow, but I conjecture a fresh flag could make sense if you want low-level control.

I added in the document a table comparing a behavior of the diverse reduction commands on the diverse representations of projections. If I understand correctly your need (essentially support for simpl never??), dropping the "folded" flag would not have an impact on your use case.

[silene]

For 1:2.3 (controlling delta depending on the number of arguments), I wonder whether it would work to declare the projection as a fixpoint in its last argument. The delta rule would then be provided by the current system for free, and tactics such as simpl are already clever enough not to unfold an unapplied fixpoint.

[Blaisorblade]

At least to go from folded to unfolded, we need beta delta, not delta; I expect iota would then work.

https://coq.zulipchat.com/#narrow/stream/237977-Coq-users/topic/Unfolding.20prim.20projections.20requires.20.60beta.60.20.E2.80.94.20intended.3F

[herbelin]

There are several errors indeed.

• I failed to see that delta was not working alone on "folded"
• The assumption I made on preparing tests on "unfolded" was wrong (due to using delta instead of beta delta) and thus iota but also simpl never on unfolded work
• The unfold at tests were otherwise mixed up.
• I should have distinguished "match" and "expanded match"

[Blaisorblade]

We might want better inspection options as a first step…

[herbelin]

In the last version, to inspect folded vs unfolded (if this is what you meant), I used a match goal which seems correctly discriminating. If you have time, that'll be good to double-check the output of the tests.

[Blaisorblade]

I added in the document a table comparing a behavior of the diverse reduction commands on the diverse representations of projections. If I understand correctly your need (essentially support for simpl never??), dropping the "folded" flag would not have an impact on your use case.

Is that so? I think I found at least one bug in the table, but regardless, AFAICT, the docs below imply that simpl never just disables delta for the projection, so it only stops clearing the flag, but (today) it doesn’t disable iota for the projection. But the docs could mean something else.

https://coq.inria.fr/refman/language/core/records.html#reduction
coq/coq#5698 (comment)

Also, iota is currently mostly about unnamed constants so one can’t “disable it for a projection”, at least in the surface syntax of https://coq.inria.fr/refman/proofs/writing-proofs/rewriting.html#performing-computations. So if we get the option of enabling/disabling iota for individual constants, we’ll want to extend the syntax of cbv (to avoid holes in the low-level commands) — and probably pick a new greek letter for this reduction?

[herbelin]

Is that so? I think I found at least one bug in the table, but regardless, AFAICT, the docs below imply that simpl never just disables delta for the projection, so it only stops clearing the flag, but (today) it doesn’t disable iota for the projection. But the docs could mean something else.

The current situation is more bizarre than I thought. Anyway, I think the important point is to agree on the expected semantics i.e. the last column of the table.

Also, iota is currently mostly about unnamed constants so one can’t “disable it for a projection”, at least in the surface syntax of https://coq.inria.fr/refman/proofs/writing-proofs/rewriting.html#performing-computations. So if we get the option of enabling/disabling iota for individual constants, we’ll want to extend the syntax of cbv (to avoid holes in the low-level commands) — and probably pick a new greek letter for this reduction?

We have already the names "match", "fix", "cofix". We could use "proj"??