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]

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]

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?

[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.

[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]

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 https://github.com/coq/coq/issues/5698#issuecomment-337556472

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"??