coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Mysterious Universes introduced by List.tl and List.repeat

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 11:19:47 +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:zMgrrx9HjIGWzP9uRHKM819IXTAuvvDOBiVQ1KB90+kcTK2v8tzYMVDF4r011RmSAtWdtqoMotGVmp6jcFRI2YyGvnEGfc4EfD4+ouJSoTYdBtWYA1bwNv/gYn9yNs1DUFh44yPzahANS47TeVDInX2z8TNXXzy3dU8sfry0ScbuiJG80Pn38JnOaS1JgiC8aPV8NkaYtwLU4+sfipJ/J7106hbPuHoAWeNL329hIxrHnR/3/9q959tj/iJKurQj8NNaXaz8V6I/V7lRCDk9Lnhz49fk40qQBTCT72cRBz1F2iFDBBLIuVSjBs/8

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, Jan-Oliver Kaiser, 09/06/2017