The Coq mailing list

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

Hi Russell,

Let me comment your question about non constant parameters of
inductive types.


* The Calculus of Inductive Constructions do not support inductive
families defined over non constant parameters.

As pointed out in previous mails, non constant parameters must be
"re-generalized" over each constructor, but then, the parameters
become effective arguments of the constructors and there is no
syntactic way to express that they should not.

Especially, for the (informal) definition

  Inductive term (A:Set) : Set :=
  | Var : A -> term A
  | App : term A -> term A -> term A
  | Fun : term (option A) -> term A.

the elimination scheme cannot just be

  term_rec : forall
    (P:forall A:Set, term A -> Set)
    (A:Set)
    (var_case:forall a:A, P A (Var A a))
    (app_case:forall a b:term A, P A a -> P A b -> P A (App A a b))
    (fun_case:forall a:term (option A), P (option A) a -> P A (Fun A a))
    (a:term A),
    (P A a)

but must rather be

  term_rec' : forall
    (P:forall A:Set, term A -> Set)
    (var_case:forall A (a:A), P A (Var A a))
    (app_case:forall A (a b:term A), P A a -> P A b -> P A (App A a b))
    (fun_case:forall A (a:term (option A)), P (option A) a -> P A (Fun A a))
    (A:Set)
    (a:term A),
    (P A a)

since otherwise, no other subcase can be applied after a fun_case has
been applied.

But term_rec' is too general since the intended semantics is that the
computational part of the instance for P is not allowed to refer to A
which has to remain a parameter and only a parameter of the
inductive type (i.e. it must not inhabit the type).


* Interestingly, a typical concept that would allow to express the
expected constraint is the one of "implicit product" described in the
context of the Calculus of Constructions by Alexandre Miquel (The
Implicit Calculus of Constructions, TLCA '01).

Roughly, an untyped lambda-term of the form "\x.t" is typable of type
"!x:A,B(x)", where "!" denotes implicit product, if x does not occur
in t (i.e. if it is not computationally used).

As for parameters, implicit products in constructors type would not
enforce universes constraint wrt the inductive itself.

Thanks to implicit products, the expected term and term_rec could then
be _predicatively_ rewritten into

  Inductive term : Set -> Set :=
  | Var : !A:Set, A -> term A
  | App : !A:Set, term A -> term A -> term A
  | Fun : !A:Set, term (option A) -> term A.

  term_rec : forall
    (P:forall A:Set, term A -> Set)
    (var_case:!A, forall (a:A), P A (Var A a))
    (app_case:!A, forall (a b:term A), P A a -> P A b -> P A (App A a b))
    (fun_case:!A, forall (a:term (option A)), P (option A) a -> P A (Fun A a))
    (A:Set)
    (a:term A),
    (P A a)

Implicit products have not been studied in the context of the Calculus
of Inductive Constructions though.


* An alternative approach for formalizing in Coq the implementation of
untyped lambda-calculus that you considered could be to reformulate
the datatype of terms as follow

  Fixpoint Lift (A:Set) (n:nat) {struct n} : Set :=
    match n with
    | O => A
    | S n => option (Lift A n)
    end.

  Inductive term (A:Set) : nat -> Set :=
  | var : forall n, Lift A n -> term A n
  | app : forall n, term A n -> term A n -> term A n
  | lambda : forall n, term A (S n) -> term A n.

in such a way that the non constant part of the parameter is moved to
a lower universe level (from Set to nat).

However, I don't know how far this alternative representation is
tractable and whether it is still acceptable wrt your initial
objectives.

Best regards,

Hugo Herbelin