The Coq mailing list

[Matthieu Sozeau <mattam AT mattam.org>]

Hi,

  The reason is that template polymorphism is limited to inductive types (and abstraction on the universes of their parameters only). So, the list_RF application cannot be set to a level lower than the global Type it is declared at even if applied to parameters in Set/Prop. That's one limitation of template polymorphism that goes away with full universe polymorphism.

Cheers,

-- Matthieu

On Tue, Jan 24, 2017 at 2:28 PM Cedric Auger <sedrikov AT gmail.com> wrote:

Same problem if you use unit instead of True, and Empty_set instead of False?

I do not remember if they are expected to have the same behaviour or not, but as your list_R is in type and not in Prop, I think it is clearer to use unit and Empty_set instead of True and False.

2017-01-24 0:53 GMT+01:00 Abhishek Anand <abhishek.anand.iitg AT gmail.com>:

Consider the following two ways of defining the same relation:

(this relation is the parametricity translation of list)

Fixpoint list_RF (A A₂ : Type) (A_R : A -> A₂ -> Type) 

                                  (l : list A) (l₂ : list A₂) {struct l} :

   Type :=

   match l with

   | nil =>

       match l₂ with

       | nil => True

       | cons _ _ => False

       end

   | cons h tl =>

       match l₂ with

       | nil  => False

       | cons h₂ tl₂ =>

           A_R h h₂ * list_RF A A₂ A_R tl tl₂

       end

   end.

Inductive list_R (A₁ A₂ : Type) (A_R : A₁ -> A₂ -> Type) : list A₁ -> list A₂ -> Type :=

| nil_R : list_R A₁ A₂ A_R nil nil

| cons_R : forall (h : A₁) (h₂ : A₂),

    A_R h h₂ ->

    forall (tl : list A₁) (tl₂ : list A₂),

    list_R A₁ A₂ A_R tl tl₂ -> list_R A₁ A₂ A_R (cons h tl) (cons h₂ tl₂).

Template Polymorphism works better for the latter definition:

Fail Check  ((list_RF nat nat (fun _ _ => True) nil nil):Set).

Check  ((list_R nat nat (fun _ _ => True) nil nil):Set).

Is there a way to make the first Check succeed?

Is there a theoretical problem in making the Check succeed, or just something that hasn't been implemented yet?

Although this is a simple example, in case of indexed inductives, I find the 

first style (using Fixpoint instead of Inductive) much easier to use.

Is there some documentation for template polymorphism?

Thanks,

-- Abhishek

http://www.cs.cornell.edu/~aa755/