The Coq mailing list

[Jacques-Henri Jourdan <jacques-henri.jourdan AT normalesup.org>]

Thank to both of you, this improves a lot our understanding of template universe polymorphism.

Our current understanding is that the template-polymorphic version of list should be equivalent to the fully-polymorphic one, because the universe of list has no reason to be upper bounded by anything (it is not upper bounded in its definition of list, and its uses should only constraint its instances). But somehow, this is not the case, for at least two reasons, that may be related:

Reason 1)

Partially applying a template polymorphic type does not trigger instantiation with fresh universe variables, and we do not understand why. This issue has already been raised on this mailing list on Sat, 22 Oct 2016 by Gregory Malecha in a post entitled "list :: nil?", but I do not quite understand the answer. At that time, Matthieu answered :

    >   Indeed, in the template case partial applications do not give you a fresh instance (because there's no way to know what the fresh levels are in that case, when retyping) , but an eta-expanded version will work I think, e.g fun X => list X, as then we can look at the type of X to determine the type of list X.

What does "because there's no way to know what the fresh levels are in that case, when retyping"?
Can't you just use fresh level and unify them with whatever they need to be unified with, depending on the context?
Why is this a problem for template polymorphism and not for full polymorphism?
Also, more fundamentally, why doesn't that break subject reduction, given that eta-reduction is part of Coq's conversion rules?

Reason 2)

In Janno's original e-mail, he noticed that the definition of List.tl introduces a spurious universe:

tl =
fun (A : Type@{Coq.Lists.List.1}) (l : list A) =>
match l return (list A) with
| nil => @nil A
| cons _ m => m
end
     : forall (A : Type@{Coq.Lists.List.1}) (_ : list A), list A
(* Coq.Lists.List.10 |= Coq.Init.Datatypes.44 < Coq.Lists.List.10
                        Coq.Lists.List.1 <= Coq.Init.Datatypes.44
                         *)

Coq.Init.Datatypes.44 is the universe of the list type. Apparently, it is set to be strictly lower than Coq.Lists.List.10, which AFAIK does not appear anywhere else.

What is this Coq.Lists.List.10 universe?
Where is it used?
Why is it constrained to be strictly larger than Coq.Init.Datatypes.44, the list universe ? Note that only instances of list should be used, and hence only constraints of the kind XXX <= Coq.Init.Datatypes.44 should appear?
Note that this does not happen if you are redefining List.tl  by either specifying explicitly the parameter of nil or the return clause of the match.

Thank you for your answers!
--
JH

Le 06/09/2017 à 11:36, Matthieu Sozeau a écrit :

Indeed, that's how it works: the "template" part is about instantiating the type of the template polymorphic inductive so that its conclusion depends on the levels of the actual parameters, and can hence get lower than the original declared universe. However the constraints are not touched at all and we hence must add constraints between the actual parameters and the declared ones in case the constructors introduce constraints on them. What you describe is what the "full" universe polymorphism mechanism does, instantiating the constraints. Example why it is necessary:

Set Printing Universes.

Polymorphic Definition lt@{i j} := let X := Type@{i} : Type@{j} in unit.

Universe k.

Inductive foo@{l} (A : Type@{l}) : Type :=

| bar (B : lt@{l k}) : A -> foo A.

Print foo.

(* Inductive foo (A : Type@{l}) : Type@{max(Set, l)} :=  bar : lt@{l k} -> A -> foo A

  (* l |= l < k *)  *)

Variables B : Type@{k}.

Fail Definition baz' := foo B.

The term "B" has type "Type@{k}" while it is expected to have type "Type@{Top.75}"

(universe inconsistency: Cannot enforce k <= Top.75 because Top.75 < k).

(* Top.75 is l *)

Hope this helps,

-- Matthieu

On Wed, Sep 6, 2017 at 11:20 AM Jacques-Henri Jourdan <jacques-henri.jourdan AT normalesup.org> wrote:

Ok, I see that.

But then my question is : why is this even called "polymorphism"?

Perhaps, what I am asking for is some sort of explanation of what is
template universe polymorphism, actually.

--
JH

Le 06/09/2017 à 10:51, Guillaume Melquiond a écrit :
> On 06/09/2017 10:42, Jacques-Henri Jourdan wrote:
>> My naive understanding is that it would create a fresh (set of) universe
>> variable, and copy all the edges of the existing universe variable of
>> the list inductive type. But there should not be any direct constraint
>> between the fresh universe to the one of the original list definition.
> I don't think it has ever worked that way. (That said, I never
> understood why it was called "template", so maybe it was meant to work
> that way). For instance, if you type
>
>   Check (fun T : Type => list T).
>
> you get a constraint between the Type type here and the one from the
> definition of list:
>
>   Top.1 |= Top.1 <= Coq.Init.Datatypes.44
>
> Best regards,
>
> Guillaume

Attachment: signature.asc
Description: OpenPGP digital signature