The Coq mailing list

[Hugo Herbelin <Hugo.Herbelin AT inria.fr>]

Hi,

> In coq 8.1, recursively non-uniform parameters in inductive types were
> added.  I think this means that, for example, the following definition
> is now accepted:
> 
> Inductive hlist (A : Type) : Type :=
>  | HNil  : hlist A
>  | HCons : forall B, A -> hlist B -> hlist A.
> 
> An (hlist A) is a list where the first element (if there is one) is an
> A.  I think this would have been rejected previously because I've
> identified A as a parameter, but in the recursive part of the HCons
> case I don't use the same A.  Is this right?

Yes.

> My question is: what is the purpose of this feature?  It's my
> (possibly incorrect) understanding that the chief reason to use a
> parameter rather than an index (or "real argument") is to get a nicer
> elimination principle.  When A is a uniform parameter, the family to
> which we eliminate and the cases for each contructor do not need to
> quantify over A individually.
> 
> But this isn't the case for "non-uniform" parameters.  This intuition
> is confirmed by examining the generated elimination rules for hlist
> and a similarly defined normal list type.  In the case of hlist, I
> could make A an index rather than a parameter without changing the
> elimination schemes.
> 
> I suppose there must be (a) some other reason to prefer parameters or
> (b) an example where making a suitable index into a non-uniform
> parameter does change the elimination rules.  Can someone explain?

As far as I know, the main reason for having introduced recursively
non-uniform parameters was to avoid artificially raising the universe
level of an inductive type.

Beside the reference given by Yves, I believe the feature is also used
in the "lc" Coq contribution (http://coq.inria.fr/contribs/lc.html) where
the set of lambda-terms with free variables in type X is defined by:

Inductive term (X : Type) : Type :=
  | var : X -> term X
  | app : term X -> term X -> term X
  | abs : term (option X) -> term X.

Here both X and term X are the same type level.

If it had be defined by

Inductive term : Type -> Type :=
  | var X : X -> term X
  | app X : term X -> term X -> term X
  | abs X : term (option X) -> term X.

then, "term X" would have been at an upper level than X (simply
because X is an argument of the constructors and then an effective
element of "term X", e.g., a projection from "term X" to Type
extracting X is possible). 

Then, considering a term over terms would have not been possible.

Besides this motivation, recursively non-uniform parameters also
simplify case analysis (the rec. non-uniform param. come for free
without any need for some kind of "inversion").

This is for what I know...

Hugo Herbelin