The Coq mailing list

[Bruno Barras <bruno.barras AT inria.fr>]

On 11/16/2011 11:50 AM, Peter LeFanu Lumsdaine wrote:
> 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 := …].)

Putting what Matthieu already said with my own words:
non-uniform parameters behave
(1) like normal indices w.r.t. recursive schemes
(2) like parameters w.r.t. dependent pattern-matching (check out list'_case)

With regular parameters, each instance can be defined independently from 
the other instances. This does not hold with non-uniform parameters 
(list' nat refers to list' (nat->nat)). The recursive scheme cannot be 
expressed for one particular instance.

For pattern-matching, the knowledge of the non-uniform parameters can be 
propagated to the pattern variables, in the same way as we do for 
regular parameters.


> I would also be interested in any pointers to the literature on
> non-uniform parameters — I haven’t been able to find any.

This has been proposed and implemented by Christine Paulin, but I don't 
think she published anything about that. The initial guess was that 
non-uniform parameters could be interpreted in terms of usual inductive 
definitions. The formal study of inductive definitions I've been working 
on uncovered (solvable) difficulties to prove their soundness, but my 
conclusion is that they don't drastically strengthen the theory (if they 
ever do).

The problem is that the translation of list' with indices gives:
Inductive list’ : Set->Set :=
  | nil’ : forall A:Set, list’ A
  | cons’ : forall A:Set, A ->  list’ (A->A) ->  list’ A.
which is impredicative and impredicative inductive definitions 
(replacing Set with Type) leads to paradoxes. Here, there's no paradox 
because the A argument of constructors is not free. Rather, it is 
uniquely determined by the type.

But there's still an issue when studying this feature in general.
Consider
Inductive I (X:Set) : Set :=
  C : X -> I X.
(You could add a constructor D : I (X->X) -> I X to prevent X from being 
a real parameter but it has not much to do with my point.)

With standard inductive types, you can deal with indices by first 
defining a non-dependent datatype and then you can define a predicate 
that rules out the raw values that do not respect the index constraints. 
For instance, the non-dep datatype associated to vector is list, and 
it's fairly easy to write a predicate that enforces the size constraint.

With I, the problem is that the set of raw values is too big (and 
doesn't fit in Set): basically I X is a copy of X, so the union of all 
values of I X is the whole Set universe. The extra work is to show that 
each subset I X for a particular X:Set form a small set. This is so 
because the set of subterms (the argument of the D constructor) form a 
small set, and this is hereditary (the union of X with X->X, 
(X->X)->X->X,... is a small set). This very last argument hasn't been 
fully formalized yet.

Bruno.

--
Bruno Barras                    Typical team - INRIA Saclay
LIX - Ecole Polytechnique       91128 Palaiseau Cedex - France
Tel: +33 1 69 33 40 57          Fax: +33 1 69 33 30 14