Gaëtan Gilbert (Mar 02 2023 at 13:52): Gaëtan Gilbert (Mar 02 2023 at 13:52):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)
Gaëtan Gilbert (Mar 02 2023 at 13:53):(and of course this is only for inductives not coinductives)
Pierre-Marie Pédrot (Mar 02 2023 at 13:58):We want dependent induction on these types, but the fact we must implement it with case analysis reeks of a foundational issue somewhere.
Pierre-Marie Pédrot (Mar 02 2023 at 13:58):So I'm leaning towards considering that these types should just be forbidden.
Jason Gross (Mar 02 2023 at 15:27):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.)
Pierre-Marie Pédrot (Mar 02 2023 at 15:31):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.
Pierre-Marie Pédrot (Mar 02 2023 at 15:32):so the claim that primitive projections matter for efficiency is somewhat moot
Pierre-Marie Pédrot (Mar 02 2023 at 15:32):(that's not the case today but there is nothing foundational)
Pierre-Marie Pédrot (Mar 02 2023 at 15:33):meanwhile primitive projections are critical to control the elimination rules of records to provide η-laws definitionally
Jason Gross (Mar 02 2023 at 15:33):(You'd also need to get parameter-free definitions when the body is just a case node, right?)
Pierre-Marie Pédrot (Mar 02 2023 at 15:34):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.
Pierre-Marie Pédrot (Mar 02 2023 at 15:34):so really, parameter-free cases and primitive projections are really equivalent in terms of efficiency
Pierre-Marie Pédrot (Mar 02 2023 at 15:35):(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)
Pierre-Marie Pédrot (Mar 02 2023 at 15:36):(but the point is that parameters can be dropped and must be added in both cases exactly in the same situations)
Jason Gross (Mar 02 2023 at 15:36):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?)
Pierre-Marie Pédrot (Mar 02 2023 at 15:39):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.
Pierre-Marie Pédrot (Mar 02 2023 at 15:39):(for corecursive primitive records it's a different matter)
Jason Gross (Mar 02 2023 at 15:42):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?
Hugo Herbelin (Mar 04 2023 at 10:49):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:
{|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. Hugo Herbelin (Mar 04 2023 at 10:50):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?
Paolo Giarrusso (Mar 04 2023 at 11:45):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.
Paolo Giarrusso (Mar 04 2023 at 11:46):Desugaring during elaboration might avoid some of those problems; polymorphic syntactic matches might still need both cases, but that's unavoidable.
Hugo Herbelin (Mar 04 2023 at 17:44):@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: Oct 13 2024 at 01:02 UTC