Suppose I have a primitive record without eta, typically a recursive record like

```
Set Primitive Projections.
Inductive foo := mk { f1 : list foo }.
```

is there a reason to forbid case nodes (which would then allow propositional eta)?

then having primitive projections for it would really only be about the optimization of omitting parameters

(when we have definitional eta we need `match x with mk bla => f end`

to be convertible with `let bla := x.(f1) in f`

but without eta this is not a problem)

(and of course this is only for inductives not coinductives)

We want dependent induction on these types, but the fact we must implement it with case analysis reeks of a foundational issue somewhere.

So I'm leaning towards considering that these types should just be forbidden.

Are you thinking that they should be forbidden only with primitive projections, or also forbidden as records even without primitive projections? (If the former, I disagree: primitive projections can be seen as just a performance optimization about dropping the parameters of the inductive type.)

We discussed about that with @Gaëtan Gilbert, and nowadays it's obvious that we could *also* have an efficient representation (i.e. parameter-free) for case nodes.

so the claim that primitive projections matter for efficiency is somewhat moot

(that's not the case today but there is nothing foundational)

meanwhile primitive projections are critical to control the elimination rules of records to provide η-laws definitionally

(You'd also need to get parameter-free definitions when the body is just a case node, right?)

No, because primitive projections are not functions. You also have to expand them (and thus explicit the parameters) to turn them into functions, just like case nodes.

so really, parameter-free cases and primitive projections are really equivalent in terms of efficiency

(ok, there is a constant overhead with case nodes because you need to encode the context but if you had to use real unbounded integers instead of machine words in primitive records you'd see this as well)

(but the point is that parameters can be dropped and must be added in both cases exactly in the same situations)

Ah, so we'd replace the definitions of the projections with Notation? And I guess you might need to fix the other parts of the system that are horribly inefficient on case nodes? (Or maybe dropping parameters and return clauses in the right way would do this already?)

I'm not advocating to change the system. Just saying that the efficiency mumbo-jumbo around primitive projections is largely accidental complexity and could be fixed in theory. This would make *recursive* primitive records useless. Thus it's an argument to forbid these things on foundational grounds.

(for corecursive primitive records it's a different matter)

I've been looking at formulations of type formers based on adjoints and Kan lifts recently, and one interesting issue is that for left adjoints / positive types (like sum), we get explicit large eliminators automatically from the formulation, but for right adjoints / negative types (like prod), we don't (and instead the same power is provided by the eta laws). And I think projections are only a natural part of the formulation for negative types. I'm not up to date on the stuff my colleagues have been working on with recursive types here, but I'll take a look and see if there's the same issue around not getting projections from recursive types. Is this something like the foundational issue you're looking for?

but the point is that parameters can be dropped and must be added in both cases exactly in the same situations

That would be good indeed to optimize `match`

as well!

More generally, my position is probably known. Distinguishing negative (projection-based) and positive (match-based) non-recursive index-free conjunctive types makes sense in linear logic but makes less sense in intuitionistic logic where, in the presence of (definitional) eta, they are (definitionally) isomorphic.

In practice, I think we have to gain to merge negative and positive index-free non-recursive conjunctive types in Type, that is to provide both a `match`

and primitive projections in those types. That may look surprising at first because it looks like we don't have anymore a clear notion of normal form for open terms, but after all, I don't think that it really matters:

- at the level of the conversion, it is not a problem because it is up to eta and we don't need a notion of normal form
- at the level of tactics, I don't see a problem at reducing the two kinds of redexes
`{|f:=t|}.(f)`

and`match Build t with Build x => u end`

(they reduce the same whatever the positive or negative "semantics" we may have in mind), and at leaving the`t.(f)`

and`match t with Build x => u end`

on neutral term`t`

unreduced (similarly, they would be blocked whatever positive or negative semantics we may have in mind); additionally, we may want to add special reduction strategies for expanding a projection into a`match`

or a`match`

into projections (knowing that we already conflate`{|f:=t|}`

and`Build t`

), if ever it happens to be useful in practice.

I'm unsure about the inductive/coinductive cases. What would be problematic in the inductive case to interpret a `Proj`

node as a primitive notation for a `match`

node, providing the reduction rules above in tactics and expanding `Proj`

into a `match`

in the conversion (in place of reasoning modulo eta)? And, in parallel, to interpret a `match`

node over a "bridled" (eta-free, Baclofen-style) dependent type in the coinductive type as a primitive notation for its expansion into projections?

if you want the two constructs to be syntactically distinct but to hide the difference: tactic-wise, wouldn't users writing syntactic matches have to account for both elimination forms? If you're proposing to quotient them inside syntactic matches, is this quotienting more robust than what Coq tries to do for primitive projections, doesn't quite manage, and maybe can't (https://github.com/coq/coq/issues/15295#issuecomment-1185699994 )? Among other requirements, let me extrapolate from that bug and say the two elimination forms two things should probably unify even when the projection is marked as opaque for unification: otherwise, Coq would have to expose which form unification is going to produce.

Desugaring during elaboration might avoid some of those problems; polymorphic syntactic matches might still need both cases, but that's unavoidable.

@Paolo Giarrusso : To be honest, I'm not at the level of the issue you are mentioning. That is, I don't clearly see how to move from the current situation to a clearer model. In any case, in the model I'm mentioning, there is only one notion of primitive projection, no such folded/unfolded form of them (the folded/unfolded thing should eventually be removed I would say).

Additionally, under the assumption of being able to optimize the representation of `match`

, another conclusion of the definitional isomorphism between non-recursive index-free positive and negative types is that we could entirely get rid of a primitive form of projections for these types (keeping a notion of primitive projections only for coinductive types).

Last updated: Sep 28 2023 at 11:01 UTC