The Coq mailing list

[Chris Casinghino <ccasin AT cis.upenn.edu>]

(Apologies if you receive this message twice - it doesn't seem to have
gone through the first time)


Hello all,

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?

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?

Thanks!

--Chris Casinghino