The Coq mailing list

[Matthieu Sozeau <mattam AT mattam.org>]

Dear Peter,

  Basically non-uniform parameters form a restriction of indices.
Their advantage has to do with elimination/inversion: one can univoquely know
from the type of an object of such a type the type of its allowed 
constructors:
all of the constructors apply, as their conclusion must be uniformly 
parametric.
With indices, one needs some kind of unification to do proper dependent 
elimination,
as, e.g. vector 0 can be built only by a subset of the constructors.
The change was deemed inoccuous theoretically, but I don't know of anything
written about it except for the manual.

Hope this helps,
-- Matthieu

Le 16 nov. 2011 à 00:20, Peter LeFanu Lumsdaine a écrit :

> I’m rather confused about what should happen when parameters occur
> non-uniformly in constructors in inductive definitions.  The manual
> says (version 8.3pl1, section 4.5, p111):
> 
>> Since COQ version 8.1, there is no restriction about parameters in the 
>> types of
>> arguments of constructors. The following definition is valid:
> 
> ----8<---
> Inductive list’ (A:Set) : Set :=
>  | nil’ : list’ A
>  | cons’ : A -> list’ (A->A) -> list’ A.
> ----8<---
> 
> When I run this definition through Coq, it does accept it, but seems
> to deal with it just by treating A as an index rather than a
> parameter.  That is, the resulting recursor has type
> 
> ----8<---
> list'_rect
>      : forall P : forall A : Set, list' A -> Type,
>        (forall A : Set, P A (nil' A)) ->
>        (forall (A : Set) (a : A) (l : list' (A -> A)),
>         P (A -> A) l -> P A (cons' A a l)) ->
>        forall (A : Set) (l : list' A), P A l
> ----8<---
> 
> which is what I’d expect with A an index — it is not itself
> universally quantified over all A:Set, but instead requires that the
> predicate into which we eliminate is so quantified.  (And it’s the
> same as what you get if you rewrite the definition with A as an index,
> [Inductive list' : Set -> Set := …].)
> 
> In the manual’s own words on the difference between parameters and indices:
> 
>> The information which says that for any A, (List A) is an inductively 
>> defined Set
>> has been lost.
> 
> Am I misunderstanding something about the difference between
> parameters and indices, or what is going on here?
> 
> The behaviour of Coq here makes more sense to me than what is
> advertised in the manual: I can’t see how you really could let
> parameters occur unrestrictedly in constructors like that, and can’t
> see what other recursor there could be.  But again, I may be
> misunderstanding how the distinction between parameters and indices
> extends to the non-uniform case.
> 
> I would also be interested in any pointers to the literature on
> non-uniform parameters — I haven’t been able to find any.
> 
> –p.
> 

-- Matthieu