Proposal for unifying the syntax for parameters and indices of inductive types

[herbelin]

This is a proposal in passing for more flexibility in the concrete syntax of inductive types.

Rendered here.

[SkySkimmer]

How is A bound here?

[SkySkimmer]

This one and the Inductive list := ... one at the end make sense IMO, but the ones were only some of the constructors get the forall and the ones where A is both on the left of the : and as a forall in a constructor don't.
This is similar to definitions: if I do Definition foo (x:bla) : nat := fun x => 0 I get an error.

[herbelin]

Yes, this is the remark "For clarity of scoping, one may also continue to impose that a variable occurring after the : cannot be used in the type of constructors."

[ppedrot]

So we're replacing a trivial criterion with a very complex one which will need to live in the kernel despite not having any model, while at the same time preventing the user to explicitly classify the arguments because some algorithm said so? Looks like a great idea to me 🐊

[SkySkimmer]

At the high level:

• parameters are ignored by the match primitive (not bound in in and constructor patterns)
• parameters do not contribute to the universe level (so Inductive Box (A:Type@{u}) := box : A -> Box A. has constructor box : forall A:Type@{u}, A -> Box A but lives in Type@{u} not Type@{u+1})
• uniform parameters do not vary in the induction principle (so Acc_ind takes P : A -> P not P : forall A, (A -> A -> Prop) -> A -> Prop)
• uniform parameters are treated specially for nested positivity (may be generalizable to all parameters???)

[Alizter]

@ppedrot I'm not following. Is there a proposal to change something in the kernel here? Surely deciding which parameters are uniform is the job of elaboration, but the kernel representation shouldn't need to change right?

[SkySkimmer]

That's not all the proposal contains

[ppedrot]

Obviously you need to change the kernel. Currently the inductive representation is very strict, such a CEP would make it much more complex, so the typing rules of inductive types need to account for that. And that in turn affects guard condition.

I am not even talking about horrors with -indices-matter and the like, but claims such that not all inductive types of a block of mutual inductive types need to have exactly the same parameters are seriously quite frightening.

[herbelin]

not all inductive types of a block of mutual inductive types need to have exactly the same parameters are seriously quite frightening.

This part is actually an old remark of Christine which is made possible with recursively non-uniform parameters and that I'm just forwarding.

More generally, parameters are not needed per se. They optimize the representation of indices that are uniform.

The remark of Christine is also only one part of the proposal. Its model is the one of inductive families (what proposed Christine can already be interpreted today by moving the parameters of a type that are not common to all types of the block to indices [Added: up to the argument counting for the size of the universe in which the inductive type lives]).

despite not having any model

The model is unchanged. Christine's proposal omitted, it differs at worst from a permutation of the arguments.

Moreover, I would not call the current model simple per se (isn't it more that we are used to it?). A model which does not distinguish between parameters and indices could arguably be called simpler. See e.g. the related stack overflow question.

Also, I would say that a model where you can set independently the name and implicit status of the parameters of constructors and types could arguably be called simpler. It is strange per se that you cannot govern the status of all arguments at definition time.

[Added]

preventing the user to explicitly classify the arguments because some algorithm said so

Already today, users have not full control on the classification as they cannot force a parameter to be considered as recursively non-uniform. Giving full control to the user on the classification is a good idea per se though and one would have to invent a syntax for it.

[aspiwack]

Something like this is very welcome. The current syntax is not ideal (and often confusing). I don't know whether it should all be purely inferred, as here, or if there ought to be purely specified syntactically. Probably you'd want the inference algorithm to be more precise to make sure that you can explain its failures (in error messages). And to make sure that we don't have data types unexpectedly (and inexplicably) jumping universe level.

[ppedrot]

More generally, parameters are not needed per se. They optimize the representation of indices that are uniform.

This is not quite true. AFAIK in the Set model, parameters are handled as real lambda abstractions and mutual blocks only quantify over their indices. In particular, structural typing à la coq/coq#5293 makes sense for parameters, but not for indices.

up to the argument counting for the size of the universe in which the inductive type lives

The very fact you had to add this mention this is not precisely going to relax me. The MetaCoq people have been unearthing forbidden knowledge like breakage of SR with a clever use of inductive types. Adding even more complexity to the mix cannot go well if you don't justify a bit more the validity of the approach, e.g. producing a convincing sketch of model, or even better, a MetaCoq proof. I am afraid that authority arguments from hearsay from the 90's shouldn't be considered valid. Also, mere logical validity is a thing, but you also need to consider at least some handwaving argument for decidability of type-checking, SR and all the syntactic whatnot we care about. Given that's it's probably already wrong with the current situation this does not look good.

(As usual you should also consider consequences for upper layers. First thing that comes to my mind is the question of the type of the auto-generated recursor for such generalized types.)

Moreover, I would not call the current model simple per se

It's not simple, and we should strive to make it simpler. I am not against a fancy user-facing mechanism like you propose, but it should be elaborated to something easy to check.

Already today, users have not full control on the classification as they cannot force a parameter to be considered as recursively non-uniform.

This is not true : https://coq.inria.fr/refman/language/core/inductive.html#coq:flag.Uniform-Inductive-Parameters.

[SkySkimmer]

This is not true

You misread the negation, that can force a parameter to be uniform but cannot force to be non uniform.

[ppedrot]

that can force a parameter to be uniform but cannot force to be non uniform

Are you saying that the kernel will generalize the type in your back to a uniform one even though you explicitly asked not to by putting said parameter after the pipe? This looks like a bug to me...

[SkySkimmer]

Are you saying that the kernel will generalize the type in your back to a uniform one even though you explicitly asked not to by putting said parameter after the pipe? This looks like a bug to me...

That's just an incorrect interpretation of putting the parameters after the pipe.

The flag can then be seen as deciding whether the | is at the beginning (when the flag is unset) or at the end (when it is set) of the parameters when not explicitly given.

and when the flag is unset we get the usual automatic discrimination between uniform and non uniform.

[herbelin]

@ppedrot:

Adding even more complexity to the mix cannot go well if you don't justify a bit more the validity of the approach, e.g. producing a convincing sketch of model, or even better, a MetaCoq proof. I am afraid that authority arguments from hearsay from the 90's shouldn't be considered valid.

To be clear, I'm not claiming that my proposal is authoritative nor that the old proposition of Christine is. As I insisted in the text, it is a proposal. I did not make a formal proof of whatever about it and I'd be precisely glad to have an opinion of MetaCoq people. In particular, I'm not opposed to the idea that MetaCoq proofs are produced, well on the contrary. If I'm proposing this CEP, it is because I think it is an idea which makes sense and that it is worth to ponder different approaches. The complexity of the Metacoq formalization is an important criterion but the practicability is too. At this point of the discussion, it is not clear to me that the changes discussed here would be more difficult to MetaCoqize than the current situation. As you suggest below, it is not to be excluded that it could be elaborated to something easy to check.

More generally, parameters are not needed per se. They optimize the representation of indices that are uniform.

This is not quite true. AFAIK in the Set model, parameters are handled as real lambda abstractions and mutual blocks only quantify over their indices. In particular, structural typing à la coq/coq#5293 makes sense for parameters, but not for indices.

I'm unsure about what you exactly have in mind. You are probably not talking about negative records with eta since negative records don't have indices. But what happens in the Set model is important, yes.

up to the argument counting for the size of the universe in which the inductive type lives

The very fact you had to add this mention this is not precisely going to relax me. The MetaCoq people have been unearthing forbidden knowledge like breakage of SR with a clever use of inductive types. (...) Also, mere logical validity is a thing, but you also need to consider at least some handwaving argument for decidability of type-checking, SR and all the syntactic whatnot we care about. Given that's it's probably already wrong with the current situation this does not look good.

What the MetaCoq formalization uncovers is indeed extremely valuable. MetaCoq is a very important project.

(As usual you should also consider consequences for upper layers. First thing that comes to my mind is the question of the type of the auto-generated recursor for such generalized types.)

Yes, the question of the upper layers is important. Here, the types of elimination predicates would be unchanged. However, as for the order of arguments, this is another situation showing that the order chosen by default is not necessarily optimal (*). We can still keep the existing order by compatibility though.

(*) An example which does not fit well already with the current convention is the scheme for rewriting from right to left: forall A x y, x = y -> forall P, P y -> P x.

Moreover, I would not call the current model simple per se

It's not simple, and we should strive to make it simpler. I am not against a fancy user-facing mechanism like you propose, but it should be elaborated to something easy to check.

Sure.

[ppedrot]

I'm unsure about what you exactly have in mind. You are probably not talking about negative records with eta since negative records don't have indices.

coq/coq#5293 is only tangentially about primitive records. What the author was asking for was (a subset of) local inductive blocks, which is what the Set model provides. In such a model, we have e.g.

Inductive foo (b : bool) := Foo : foo

x : bool, y : bool ⊢ foo x ≡ foo y : Type

because parameters are implemented as standard λ-abstractions. Since the above inductive type doesn't mention its parameter argument, we get this conversion for free by mere application of a β-rule. More generally, in this model conversion of inductive types is essentially given by pointwise conversion of the type of the constructors of the block.

This does not make sense when interpreting parameters as indices.

[gares]

Hum, frankly this seems a lot of complexity (mostly in the kernel) for little gain. Moreover, parameters, nu-parameters and indexes are different. We recently got a syntax to remove the last ambiguity by putting nu-parameters after |, that was very welcome on my side, it made the user code easier to understand and more stable. Moreover the last attempt of tricking the user into thinking that parameters are alike regular arguments did not end well, I'm talking about the Asymmetric Pattern thing, which nobody really was in love with.

Finally, I find the current order of arguments quite natural if you you have a background in functional programming. What does not vary in a rec function, you pass it first, since it ease partial application. What changes you pass it last, eg you use the function keyword (in OCaml). This practice transposes well to Coq's inductives, so it's a bit easier to remember/learn it for a class of users, IMO.

[SkySkimmer]

We recently got a syntax to remove the last ambiguity by putting nu-parameters after |

As mentioned that's a misunderstanding, the parameters after the | may still be uniform.

[herbelin]

I'm unsure about what you exactly have in mind. You are probably not talking about negative records with eta since negative records don't have indices.

coq/coq#5293 is only tangentially about primitive records. What the author was asking for was (a subset of) local inductive blocks, which is what the Set model provides. In such a model, we have e.g.

Inductive foo (b : bool) := Foo : foo

x : bool, y : bool ⊢ foo x ≡ foo y : Type

because parameters are implemented as standard λ-abstractions. Since the above inductive type doesn't mention its parameter argument, we get this conversion for free by mere application of a β-rule. More generally, in this model conversion of inductive types is essentially given by pointwise conversion of the type of the constructors of the block.

This does not make sense when interpreting parameters as indices.

May I rephrase your remark into the fact that for the two definitions

F : ISet -> A -> ISet (* strictly positive with ISet impredicative Set *)
Foo := fun params:A => forall P:ISet, F(P, params) -> P

and

F : (A -> ISet) -> A -> ISet (* strictly positive *)
Foo' := fun params:A => forall P:A -> ISet, F(P) params -> P params

Foo params satisfies less definitional equations than Foo' params when params does not actually appear in F? Indeed. I'll add a remark on this in the text.

[ppedrot]

Foo params satisfies less definitional equations than Foo' params when params does not actually appear in F?

Yes, that's one way to see it. It's not only about params not appearing in F, more generally it might be the case that F can compute for some specific instances of params.

[gares]

We recently got a syntax to remove the last ambiguity by putting nu-parameters after |

As mentioned that's a misunderstanding, the parameters after the | may still be uniform.

Is there a real use case for interleaving params and nu-params?

[herbelin]

Hum, frankly this seems a lot of complexity (mostly in the kernel) for little gain.

The proposal is probably badly written if it gives so much the impression of complexity, but there are actually four independent parts in it:

The first two parts do not change the kernel:

• 1- A pedagogical/practical change:

  • how much do we want the classification between parameters and indices to be in charge of the user or being done automatically?
  • how much do we want the position of the : to be significative and be different from other places using :?

  Basically, this change amounts to allow the : to be anywhere (with only the variables before : having global scope).

  As a comparison, in fix, we are not forced to tell which argument is decreasing. It can be inferred if one wants. And conversely, automatic inference does not imply that there is no way for the user to control it.

• 2- Another practical change: how much do we want to make a difference between a variable quantified globally in the block (but then in practise requantified automatically over each constructor) and a variable quantified locally in the constructor? In particular:

  • this allows to faithfully write the types of constructors as they are internally
  • this allows to indicate implicit arguments constructor per constructor
  • this allows to give full control on the names used in the internal representation

  Basically, this change amounts to allow the parameters to be repeated in the type of constructors (and to drop the global context if it binds nothing explicitly any longer).

The last two parts do change the kernel (but only slightly):

• 3- A convenience: being able to mix parameters, non-uniform parameters and indices in any order

  For this, we need to replace two numbers (the number of params and the number of uniform parameters) by a list of status and to replace all List.chop on these numbers by a special function extracting the parameters using the status list.

• 4- A slight optimization: being able to declare more indices as non-uniform parameters in mutually inductive types (Christine's old proposal)

  For this, we need to move the number of parameters and non-uniform parameters (or the list of status if the previous point is adopted) from the mutual block (the "mib") to each individual packet of the block (the "mip") and to accordingly use the index of the packet under consideration when dealing with parameters.

[herbelin]

Moreover the last attempt of tricking the user into thinking that parameters are alike regular arguments did not end well, I'm talking about the Asymmetric Pattern thing, which nobody really was in love with.

I think the symmetrization of patterns was a good choice, starting with the ability to use the same notations in patterns than in terms.

Moreover, parameters are currently supposed to be replaced by _ but we could have allowed as well to bind the parameters in the right-hand side (replacing them either with the actual global parameters of the term to match, or even with the parameters of the corresponding constructor).

Idem for the return clause, we force the parameters to be _ but we could have as well allowed them to be bound and replaced in the predicate by the actual parameters of the term to match.

I don't think that this would be more complicated to explain than the current situation. But I agree that it is also about pedagogy, and we need to experiment to know what is the most natural way to explain things.

[gares]

If an index comes first, can subsequent parameters or nu-parameters depend on it?

[herbelin]

If an index comes first, can subsequent parameters or nu-parameters depend on it?

Typability implies that a parameter cannot depend on a true index (i.e. an index which could not be classified itself as a parameter). Similarly, typability implies that a uniform parameter cannot depend on a (truly) non-uniform parameter.

[gares]

So I don't see what is the point of allowing an arbitrary order.

1. One thing is to say, well, : is a bit misleading, let's provide a syntax where only : sort is allowed (like for record) and use something, say ||, to mark indexes.
2. Another one is to have the position of || be inferred.
3. Yet another thing is to let one write anything and if no inference of "what is this argument" can be done give an error.

IMO 1 is sound, 2 is reasonable (assuming this inference works in practice), 3 is just not worth it (and seems the point which changes the kernel).

[gares]

On another point, I think that being allowed to repeat parameters in constructors just for the sake of setting their implicit status is an x-y problem. According to my experience the status of parameters should be the same all over, with a few exceptions, eg one may want to make A in nil A both maximal and non-maximal. But these exceptions don't justify a general change, IMO.

[herbelin]

So I don't see what is the point of allowing an arbitrary order.

But if the dependencies between arguments have to respect the indices > nu-parameter > parameter order, these does not mean that two arguments have necessarily to be dependent the one of the other (it can be a graph). For instance, currently, I cannot define ge the same way as le is defined below:

Inductive le (n:nat) : nat -> Prop :=
  | le_n : le n n
  | le_S : forall m:nat, le n m -> le n (S m)

[herbelin]

On another point, I think that being allowed to repeat parameters in constructors just for the sake of setting their implicit status is an x-y problem. According to my experience the status of parameters should be the same all over, with a few exceptions, eg one may want to make A in nil A both maximal and non-maximal. But these exceptions don't justify a general change, IMO.

Yes, the change is not needed per se to set names or implicit arguments of constructors (Arguments is still usable).

Personally, 1 and 3 are the ones I'd like to have.

I'm not particularly advocating for 2, but here is nevertheless an example where 2 might be useful...

The library Relation_Operators defines

Variable A : Type.
Variable R : relation A.
Inductive clos_trans (x: A) : A -> Prop :=
  | t_step y : R x y -> clos_trans x y
  | t_trans y z : clos_trans x y -> clos_trans y z -> clos_trans x z.

Imagine I'd like the type to formally be relation A rather than A -> A -> Prop, as done in other places of this library. How can I do it while still preserving the non-uniform parameter status of the arguments, if not allowed to give a context to constructors individually, as, e.g. in:

Inductive clos_trans : relation A :=
  | t_step x y : R x y -> clos_trans x y
  | t_trans x y z : clos_trans x y -> clos_trans y z -> clos_trans x z.

[herbelin]

And to go further, I don't see why to force users to have headache on how to define ge, about what should go before : or after, and about why to transit via le, while they could simply write:

Inductive ge : relation nat :=
  | ge_n n : ge n n
  | ge_S n m : ge n m -> ge (S n) m

[gares]

Why should any of the two argument be a parameter? To me ge is fine... it's le that is weirdly written. Anyway, I think I expressed my opinion. I'll let others bring their contribution.

[herbelin]

Why should any of the two argument be a parameter? To me ge is fine... it's le that is weirdly written.

Then I believe that we agree, i.e. we could try to defend a user view where there are only "indices".

[herbelin]

Actually, I wonder where parameters really matter in the kernel? Could it be that the status of parameter is used only for the nested positivity condition and the nested guard condition (which seem by the way both more restrictive than in Agda)?

As said by @ppedrot, parameters are important in the upper layers though:

• they are used to tell which indices of a truly recursive induction scheme are quantified globally (though the computation of them can be left outside of the kernel)
• they are used to restrict the arguments of an inductive type which may really matter for unification when trying to infer the return clause
• probably some other applications which don't come to the mind right now

[SkySkimmer]

Parameters matter a lot for matches

[herbelin]

Parameters matter a lot for matches

Right, they matter more than just for the inference of the return clause.

If all parameters started to be treated like indices in match we would lose the definitional equalities between the parameters in the type and the parameters in the constructors that currently come by the factorization of parameters in the syntax (similar to @ppedrot's remark on coq/coq#5293 where extruding arguments from a "commutative cut" gives more definitional equalities).

[Digression: These equalities could be recovered with a "small inversion"-like generalisation though. More generally, there are actually more definitional equalities to expect between arguments of the type and arguments of the constructor than just the parameters. This morally applies to all arguments that are fresh variables in the type of a constructor. So, at some time, typing of match may be rethought so as to provide these kinds of definitional equalities automatically, and not only for parameters.]

Anyway, this goes too far from the initial idea. Maybe MetaCoq may like at some time to consider dropping parameters in the metatheory of inductive types and compensating with hard-wired definitional equalities in the typing of match, but probably not now.

So, my current summary about this CEP is: would we like to simplify the user model about inductive types, as suggested in the examples of ge and le, by taking in charge automatically the distinction between parameters and indices, in the same way as, for instance, we already automatically take in charge the inference of the decreasing argument in fix?

[SkySkimmer]

I feel inference of parameters would be more confusing, because then you have to run the inference in your head to understand how to use match.

I support the part about having parameters on individual inductives instead of shared across a block, but not the rest of the proposal.

[herbelin]

I feel inference of parameters would be more confusing, because then you have to run the inference in your head to understand how to use match.

You can also count on About to show the result of the inference.

[If you are talking about the current constraint of using _ in place of the parameters, it is not an essential one.]