coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Jacques-Henri Jourdan <jacques-henri.jourdan AT normalesup.org>
- To: coq-club AT inria.fr
- Subject: Re: [Coq-Club] Mysterious Universes introduced by List.tl and List.repeat
- Date: Wed, 6 Sep 2017 13:58:27 +0200
- Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=jacques-henri.jourdan AT normalesup.org; spf=Neutral smtp.mailfrom=jacques-henri.jourdan AT normalesup.org; spf=None smtp.helo=postmaster AT ulminfo.fr
- Ironport-phdr: 9a23:/7P2Mh3Gg4KgebessmDT+DRfVm0co7zxezQtwd8ZsegWKfad9pjvdHbS+e9qxAeQG96Eu7QZ06L/iOPJZy8p2d65qncMcZhBBVcuqP49uEgeOvODElDxN/XwbiY3T4xoXV5h+GynYwAOQJ6tL3DMr2eN7T8OF1C6HEI1Y72tQs+Bx/iwguu14tjYZxhCrDu7e7J7ahus/ivLscxDo4JpM7s80V7pr31Seqx0wn5yKVuV10L+78yp4ZN4tiRdveggscxHTL/2dqIQS7tCCT0iPnso/IvsrxaVHljH3WcVTmhDykkAOAPC9hyvG86p6iY=
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 = 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
- [Coq-Club] Mysterious Universes introduced by List.tl and List.repeat, Jan-Oliver Kaiser, 09/06/2017
- Re: [Coq-Club] Mysterious Universes introduced by List.tl and List.repeat, Guillaume Melquiond, 09/06/2017
- Re: [Coq-Club] Mysterious Universes introduced by List.tl and List.repeat, Jacques-Henri Jourdan, 09/06/2017
- Re: [Coq-Club] Mysterious Universes introduced by List.tl and List.repeat, Guillaume Melquiond, 09/06/2017
- Re: [Coq-Club] Mysterious Universes introduced by List.tl and List.repeat, Jacques-Henri Jourdan, 09/06/2017
- Re: [Coq-Club] Mysterious Universes introduced by List.tl and List.repeat, Guillaume Melquiond, 09/06/2017
- Re: [Coq-Club] Mysterious Universes introduced by List.tl and List.repeat, Jacques-Henri Jourdan, 09/06/2017
- Re: [Coq-Club] Mysterious Universes introduced by List.tl and List.repeat, Matthieu Sozeau, 09/06/2017
- Re: [Coq-Club] Mysterious Universes introduced by List.tl and List.repeat, Jacques-Henri Jourdan, 09/06/2017
- Re: [Coq-Club] Mysterious Universes introduced by List.tl and List.repeat, Guillaume Melquiond, 09/06/2017
- Re: [Coq-Club] Mysterious Universes introduced by List.tl and List.repeat, Jacques-Henri Jourdan, 09/06/2017
- Re: [Coq-Club] Mysterious Universes introduced by List.tl and List.repeat, Jan-Oliver Kaiser, 09/11/2017
- Re: [Coq-Club] Mysterious Universes introduced by List.tl and List.repeat, Matthieu Sozeau, 09/12/2017
- Re: [Coq-Club] Mysterious Universes introduced by List.tl and List.repeat, Jacques-Henri Jourdan, 09/13/2017
- Re: [Coq-Club] Mysterious Universes introduced by List.tl and List.repeat, Ralf Jung, 09/14/2017
- Re: [Coq-Club] Mysterious Universes introduced by List.tl and List.repeat, Jacques-Henri Jourdan, 09/06/2017
- Re: [Coq-Club] Mysterious Universes introduced by List.tl and List.repeat, Guillaume Melquiond, 09/06/2017
- Re: [Coq-Club] Mysterious Universes introduced by List.tl and List.repeat, Jacques-Henri Jourdan, 09/06/2017
- Re: [Coq-Club] Mysterious Universes introduced by List.tl and List.repeat, Guillaume Melquiond, 09/06/2017
- Re: [Coq-Club] Mysterious Universes introduced by List.tl and List.repeat, Jacques-Henri Jourdan, 09/06/2017
- Re: [Coq-Club] Mysterious Universes introduced by List.tl and List.repeat, Guillaume Melquiond, 09/06/2017
Archive powered by MHonArc 2.6.18.