Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Universe Polymorphism

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Universe Polymorphism


Chronological Thread 
  • From: Helmut Brandl <helmut.brandl AT gmx.net>
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] Universe Polymorphism
  • Date: Thu, 17 Nov 2022 10:45:39 +0100
  • Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=helmut.brandl AT gmx.net; spf=Pass smtp.mailfrom=helmut.brandl AT gmx.net; spf=None smtp.helo=postmaster AT mout.gmx.net
  • Ironport-data: A9a23:88Lc2q/iKHnq1Qv0H1dtDrUDk3qTJUtcMsCJ2f8bNWPcYEJGY0x3z jFLUDqDP/3cZmHwKtkgPtm19hgH7ZLSndI1G1Rv+HhEQiMRo6IpJ/zJdxaqZ3v6wu7rFR88s Z1GMrEsCOhuExcwcz/0auCJQUFUjP3OHPylYAL9EngZbRd+Tys8gg5Ulec8g4p56fC0GArlV ena+qUzA3f4nW8qWo4ow/jb8kk25a2t4GlwUmEWPJingneOzxH5M7pEfcldH1OgKqFIE+izQ fr0zb3R1gs1KD9wYj8Nuu+TnnwiGtY+DyDW4pZlc/TKbix5m8AH+v1T2Mzwxqtgo27hc9hZk L2hvHErIOsjFvWkdO81C3G0H8ziVEHvFXCuzXWX6KSuI0P6n3TEhK8xEW9mLNUixMl5XmFMq KNIMjAwYUXW7w626OrTpuhEg8M+MI/kOZNZvHx8pd3bJax/G9aZGfqMvIAehm1YasNmRZ4yY +IZZD5qcQiGaQdGPFsTIJ07jKGui2WXnzhw9wLL+/NqvDi7IApZ9rnQafPKJ/O2W+ZSx3SFn HLlzUmpHURPXDCY4WPYriz137GncTnAcIkVDfiz8uNgqEaCw3QaThwQT1qy5/ej4nNSQPpaL FEIvCUrve40+VDDosTBswOQ5yTbozBMSoJqLcI0twGPl/WE+QakCT1RJtJeU+AOuMgzTD0s8 1aGmdL1GDBi2IF5r1rCr994ShvtYEAowX8+iTwsEVtUsoW+yG0npkKUEYszeEKgpoCtQVnNL ya2QD8Wq5h7YSQj9Kyh+UvdnjKhznQiZlFrv16KNo5JxilwaIOjIrO180TH4PNKIZyWJmRtU VABnNWCqu8LHdeLmTDlrAQx8FOBtq7t3N702A8H83wdG9KFpSfLkWd4vmsWGauRGpxYEQIFm WeK0e+r2LddPWGxcYh8aJ+rBsIhwMDITIq7Bq6ONYYUPcIpL2drGR2Cg2bPjggBd2BzwckC1 WuzKpfE4YsyVPg2kmHvLwvj+eVznXBhrY8seXwL5036jeTHPSD9pUYtaRXXJuE/8K6epgjJu 99QX/ZmOD0PONASlhL/qNZJRXhTdSZTLcmv96R/K7DfSiI7RjBJI6GLndsJJdc/94wLzbigw 51IchQFoLYJrSabclrih7EKQO+HYKuTWlpiY318ZA72hid7CWtthY9GH6YKkXAc3LQL5ZZJo zMtIa1s29wfF2SVyCdXdpTnso1peTKigA/EbWLvYyEyc9QkD0bF88PtNFmnviQfLDuFhe1nq Z2Z1yTfXcUiQSZmB53oc/6B9Q66kkUcv+NQZHH2BOdvVn/iy6VUDhDgr+QWJpgMICrTxzHB2 AexBwwZlNb3oIQ00YfogPmao7eQDtkkRxZ+GjTf4Z2XLgjfxHKomqVbYdaLfBfcdWL6w7qjb uNr1MPBMOULsVJJkohkGZN55Pgay/q2gJEC1SViPnHAT2rzO4NaOnPcgPV+7Pxc9IFWqS6de xyp+OADHZ6rJcm8MloaBDR9X9S5zftOxwXjt6UkEn7buh1y0qGMC3hJHh+2jydYErt5HaUlz colu+8U8waPsQUrAPnXkhFr83mwEVJYX5UFrp06BKrZujgvwHxGYr3eDXb424HQStNuNkJxH CSYqpCfjJthx23DUUEJK17z4cRni64z5S96lG05GwzRm/7upOMG4xlKwDFmEiVX1kpm1sxwC EhKNmp0B6OEzzh1js19B0GtBABzKxmL8WPhy1YytTP4Tmv5ckfvPWECKeK200RByF1lfx9f5 6C+9GbpdR3IbfPB9HI+dmA9osOyUOEr0BPJnf6WOvisHr44UGLDubCvb29ZkCnXK5o9q2Ofr NY74dsqT7PwMBMRhKgJC4O687A0YzLcLUxgRcBRxo84LVv+ShqThwfXc1uQf/lTLcPk6UW7U sxiBvxeXiSEiRqhkGopOr4uEZRVwtgZvMEPa5H6F14g6rG/lAdkgLjU1yr5hVIofelQrNYAG tvRWg+GQ0Othipyum7SrcN7FHKyTvsaaSbdgu2k0uU7OKgSkeNrcHNoi+eQuiiRPCBG5DORh hvIPIXN/txhyKNtvoriKbpCDAOKMuHOVPyE3QSwktZWZ/bNDJv+jBwUoVzZIAhmB7sddNBpn 7CrstSs/kf6kJspcmLewb+tKrJo4JisYe9pLc7HFnlWsi+cUsvK4RFY2WSZK4RMoexN9PucW Aq0R8uhR+E7A+4H6iVuVBFfNBIBB4DcTKTq/3q9psvRLCkt61XMKdf/+EL5aW1eSDQzBKT/L Q3K6saevoUS6MwGARIfHPhpDqNpOFKpC+Nsa9T1siLeFWWyxE+Lvrz5jxc79DXXET++Hd3n5 Y7eDA3LHPhoVHokEPkC22CzgvEWMJq5qew3Y15b9NtmzTa3EAbq6Ajb3YouUvlpfu7ajfkUp w0hqEMtDDW7WzlYGfk5yMq2RR+RX4TiJf+gTgHEPCqoh+OeC4aQRr1s6k+MJpuwliTLlImaF D3VxpE80tVdDH2kqSb/K8FXWdta+84=
  • Ironport-hdrordr: A9a23:Ytj/5aijH6zEI+BI/XCC/byxVHBQXvgji2hC6mlwRA09TyX4ra 6TdZEgviMc5wxwZJhNo7y90ey7MBHhHOBOjrX5TI3CYOCOggLBQb2Kr7GSpwEIcBeOldK1u5 0QFpRWNP21K0RmhsDn5wSCH88n28TvytHRuQ6n9QYLcelwAZsQiTuR5zzra3Gfz2R9b6YEKA ==
  • Ironport-phdr: A9a23:0LI9yBCcWDp7ONXiDu6BUyQUfEkY04WdBeb1wqQuh78GSKm/5ZOqZ BWZua8xygOZFt2Ho7Ic0qyK6fumATRBqb+681k6OKRWUBEEjchE1ycBO+WiTXPBEfjxciYhF 95DXlI2t1uyMExSBdqsLwaK+i764jEdAAjwOhRoLerpBIHSk9631+ev8JHPfglEnjWwba19I RmsogjctcYajZdtJ60szhfFvmZEd/5ZyG92K1+fhQrw6tu18JV+7ylepvUt+tJaX67nZao4V 7tYDDonM2Ax+sLmsATIQBWM6HUBTGgYiwJEDAfZ4h70WJfxqTb6ufFm2CaGJ832TKs7Viqk4 qx2VRLnkiYHNzo+8GHKlsx9ib9QrRy9qxBjxYPffYaaOudjfqPGZdMVW3ZOXtpfWSxGB4Ozd YoPD+wcNupcoITwo14CoB2jDgeuGezv0CdFiH/106Im3OsvHxzI0w4+EdIAt3rZt8/6OLsXU e2vzKnE0TfOYvVL0jn98ojIdRUhrOmOU71udcrRzFQvFx/YhViNs4zqJTWV2fkJs2OG6OdgV fygi2oiqwFsvjij3NwjipPTiYIT11/E8T50wIkwJdy3UkJ7Z8CrEIdJuiycKoB5Td8sTXtyt yYm1r0Jp4S7fC4SxZk52xLSZfyKf5SV7h/hVeucJTl1iXZ4db6jiRi//kitx+PiWse6zVpHr iRLn9fCuHwT2RLd5cmKRuV/80qv2juC0R3Y5O9DIUAxj6XbKpghz6Y/lpoSrUTDHjL2l17sg K+XcUUp/PWj5ef/Yrj+uJOQKpF4hhvgPqgwmMGzG/k0PwoUU2SF5+iwzLnu8E3jTLhJivA6i LTVvZ7VKMgBuKK0DAlY2Zs55RmlFTepytEYkGEHLF1bfBKHiJDkO1TJIPDlEfezmVuskDJkx vzcOL3uHInNImDCkLfnY7l991ZRxBQuwdxB/Z5YFK8NLfDpVkPsttHUFAE1PxKsz+biEtp91 4ceWWyVAq+eNaPfqV+I6fwrI+mJeY8VpCzxJOM/5/H0i382hFsdcLKm3ZsSZ3G0BPJmLFuFY Xb0hNcOCn8FvhAiQ+zylF2CTTlTam6vU64k/DE0FJqmDZvfRoCqmLGOwCC7HoRPam9aDlCMD Gznep6fW/YMbSKSOtVuniYFVbinUY8h1AuhuBX0y7p9faLo/XgTsoum39xo7cXSkwsz/Hp6F ZezyWaIGkF5mmYVW3ccxql5rUg1nleO1a1ln7pSD9VV6/dhXQIqc5jR07opWJjJRgvdc4LRG x6dSdK8DGRtH7rZovcLakd5QZC5iwzbmjCtCPkTnqCKA5o99uTd2WLwLoBz0SWOz7Ev2n8hR MYHLmi6nuhn7QGGB4PNlliF0aywfKIQ2AbC8XfFy2eS7wlDSAAlaazeRjgEY1fO69Hw50fMV birXLQqNg5c1YiIMKJMZtnBglBWAvHuJIeWeHq/zkG3AxvA3baQdMzqdmEaiT3aE1QBmhsP8 GyuMA8jGmGupnKYCjFyfb72S2Xr9+Q26HayT0tuihqPc1Ukzb2+vBgcmf2bTfoXmLMCoiYo7 TtuTh672JrNBtyMqhAEHu0UaM4h4FpByWPSthBsdp2mIad4g1cCcgNx90rw3hRzA49EnIAkt nQvhAZ1LKuZ1htGeVb6ldjwN7nSN3W09gqmbaLS8l7bwJCQ97tOoPU0plP/vR24Q1I4+iYv2 N1U3n2Ao5TSWVBLC9SrCBlxrkc8/euJB0t1r5nZ3nBtL6Su5zrL2tZzQfAg1g7lZdBUdqWNC A71FcQeQcmoMu0j3VazPXdmdKhf8rA5O8S+er6IwqmuaaxgkTajkHgB6pp01E6I3yV5WqjO0 opPkJT6lkOXEizxilusqJW9mY1AYCwOWGClwC7oAKZeY700e4sXQzTLQYX/1pB1gJjjXGRd/ VioCgYd2cOnThGVakT0wQxa0Ul/TWWPoSKj1HQ0ljgoqvDaxynS26H4cxFBPGdXRW5khFOqI I6ujtlcUlL6JwQukRKk4w79yc057Ox/Im3WXFsOdTL/KW1meqS1pvyEbtIH5J4zsCpRWfixe hjAE+S7+UFFlXq8WTEEjDkgPymnoJD4gwB3hAf/ZD5ooXzVdNsxjRbT6drAROJAiz8PRS12k z7SVRC3O9ik+8nRlo+W6LnkETj7CdsKLm+xl9Dl1mPz/2BhDByhkurmn9TmFVJ/yirnz5xwU i6Oqh/gY47t3qD8MOR9f0AuCkWvjqgyUox4jIY0g4kdnHYAgZDAt3oKlWLuLZNRw6v4YH4lS jsbhdjY/EK2vS8rZmLM3I//WniHl4Fhat2/f39Q0Dg06cxOIKiR/PpCkDc/8T/a5UrBJPN6m Dka0/4n7nUX1voItAQaxSKYGrkOHENcMH+kh1GS4tu5tqkSeHe3fO36yh9lhd74RuLnwEkUS DPjd5wlByM18shvLAeGzijo8o+9MNjIMYBJ70bSykmdybYJbsp2zKFChDI7az2h+yd9m6hmy 0Iymsvk2erPY2R1oPDjW0QebGeqIZpJpHe01/YZxJve3pjzTM84QHNRBsSuFK/uSHVI6JGFf 06PCGFu8C7BX+CFQknGtwE+6CiQW5GzayPIeD9DlYUkGF/EdRYY2l5cXS1mzM5jUFn0mYq4L RY/vndLujua4lNN0r46bUCgFDiF4l3wNXFsD8LAZBtOslMSvQGMb5HYtLgiWXoBtpy58F7dc CrCOVkOVzpRHBbdTxXqOr3kjTXZ286fAOf2b/7HYLHU7PdbS+/N35WklI1v4zeLMMyLeHhkF fwynERZDzh/HIzCljMDRjZy9WqFZtOHpBq65ix8r9yuuPXtVgX14IKTCrxUedxx8hGyiK2HO qaeniF8YTpf05oNwzfPxt19lBYKjDpycjC2DbkanSvKUb6WlapHSRgWd2I7NcdF6b49whgYO cPfjYCQtPYwhfo0BlFZEF35z5vwP4pQeT77bQyBXhzYUdbObSfGyMz2f66mHLhZjeEO8ga1p S7eCUjoeDKKizjuURmrd+BKliCSehJE6+TfOl5gD3buSNX+Z1i1Kthy2Hc2zLkxm2+MP3QVN zR4W0xIvvuW4D8S0ZAdUyRRq2FoK+WJgXPT9+7DNpMfqudmGAxxkP9Gpns/2/1T4T0OF5kX0 GPC69VppV+hiOyGzDFqBQFPpjh8j4WOpUx+OK/d+/GouF7B+w8Rq2qVG1IMqsc3UrUHXohfz 8iJkq/vem8qGz388s4MQc7ZNJDeWEc=
  • Ironport-sdr: 637602c5_0U9oBujy5OAvtyXZmqbfG2zHamk6x90DyxCJ6rKdS0A9911 2dYKho46DpPGDwPRkXtei+LRAMa+QLzhCIwHokQ==
  • Ui-outboundreport: notjunk:1;M01:P0:CnBOv917jOc=;6ap6KYsPoMahsqqCZOXqctxYwaq qSAY6k6oIOUDT05VvppnlB9ggoJ7vHAcHiIOMc/lxPQwG/oYHAeK8itlQXdsCqBhgWr3WRKdE q1FJsXeV+ULBF9p+neFw7TYnlUPcXr3e6HqwiDE059m4m+GDBCGaL9UUiNCFVAmf7DxScNEiL 1d8Eady7QEyiiTKM/mvlPcLQdC7cAMWDOsN5FaUZQEFHoXQr/vGxAASWf8AjjK2Q8EZ9PCB8W oS0MCHDWcGfRP4drTEHc4XK6jom0ZLUeLktAe/SvPtVNJ6ye+cAwBuf3axeRCaJcX6h9Z34wc kt2HoJss36J2PJ6Wm4ii6SVNtq0foLq2t9fI3QIcohYqgA2cf/BWaVpH4jiWCCMdYLFNyaKUL Zt4sQuspqDwMVexndPjFtI86iBxt1sgMfF2W264tKJmrikw3clYon/357FfZCt1UOUryJdJPz ay6pGOiv3u6NZW6JvKlQtPpcbldOwyaFXb5GammLODLx+ZbCfR2XBvh94fQrlZEmLK0ZfvC4z FcjvHfFUgd7ek+Jb435dZQAsSWJk8DbCUYfhCIuOpGp3oYXlNJxmYc6rjOLZLbYyGpraS+iA+ LyQmf5YM70YRq+yvn3QChsUmSrTVqGmo/lr4+gQwzH3Jse6rWCvoEke3WUDTLq4BjGK0Mye9T Ni713W9mYlChimNG0VpULSg3xKHMzwAzOwue6AdTepkKfNG6eznNB257Vz1pjiHzByAQowPh4 yD00T1/alKVc1uOAntZiELnhwUD0tR0u6Qw2Ia50LmKmvz1HUne84WJrugiXrvjcuG3kaDNqc 4Nc0E/bg7HsxVG6gK1WWgAMXRtWVmHejd124hIcvwmXkQ+zym7DiGQaYOFzNGkoln+H8C1z6B +AeBNld+xWh1YiyM1fltqr23VnMnBA6X+/kdRJwobMO+kg4EpDo2CHE0HeGjKfUmZaNgznMqu ZY6Swwoni124+Me05KPVfK15Inw=



On 16 Nov 2022, at 23:35, Gaëtan Gilbert <gaetan.gilbert AT skyskimmer.net> wrote:

The rules for inductives https://coq.github.io/doc/master/refman/language/core/inductive.html#theory-of-inductive-definitions
basically every argument of a constructor must be at a smaller or equal universe to the output universe of the inductive. The first argument of cons fails this.

Thanks for the explanation. I have tried to read the description in the link. Unfortunately I have not found the rule that every argument of a constructor must be at a smaller or equal universe to the output universe. Could you point to the specific paragraph which states that rule. Since the rules are very technical I might have overlooked it.

My intention is to understand not only the “what” of the rules, but also the “why” of the rules. What is the justification of such a rule? E.g. first I didn’t understand the necessity of the positivity rule of the constructor types. Then I have found an example which makes the necessity of the positivity rule clear. If the following inductive type were allowed

Inductive T: Type :=
| co: (T -> T) -> T.

I could define a fixpoint with infinite recursion

Fixpoint run (t: T): T :=
  match t with
  | co f => run (f (co f))
  end.

Is there a similar justification for the rule you have mentioned? Does the rule inhibit an inconsistency like infinite recursion?

— Helmut



Gaëtan Gilbert

On 16/11/2022 22:32, Helmut Brandl wrote:
On 16 Nov 2022, at 22:06, Helmut Brandl <helmut.brandl AT gmx.net <mailto:helmut.brandl AT gmx.net>> wrote:



On 16 Nov 2022, at 21:23, Gaëtan Gilbert <gaetan.gilbert AT skyskimmer.net <mailto:gaetan.gilbert AT skyskimmer.net>> wrote:


I.e. the argument type of a function type can live in a higher universe than the result type.

Yes, but "lst" is an _inhabitant_ of the function type, it's not the function type itself.

Similarly "(fun A:Type@{u+1} => A) : Type@{u+1} -> Type@{u}" is rejected

In that case the rejection is clear to me. The term ‘A’ has type ’Type@{u+1}’. Therefore the function returns a result of type ’Type@{u+1}’ and not ’Type@{u}’ as required by the type annotation. I.e. the function on the left hand side of the colon is not an inhabitant of the type on the right hand side of the colon. The compiler must reject it.

Are you saying that the type ’Type@{u+1} -> Type@{u}’ is not allowed to be inhabited? Is there such a typing rule? If there is such a typing rule, I would like to understand why it is there. Does the violation of such a typing rule create any inconsistencies like an inhabitant of the type ‘forall A: Type, A’?
According to coq the type ’Type@{u+1} -> Type@{u}’ can have inhabitants. E.g. the following is accepted by coq:
   Check (fun A: Type@{u+1} => nat): Type@{u+1} -> Type@{u}.
However my construction of the inductive type ‘lst’ which is an inhabitant of exactly that type is rejected. Why is it possible to construct a function of that type but not an inductive definition?


— Helmut




On 16/11/2022 21:02, Helmut Brandl wrote:
I’d like to understand universes and universe polymorphism better. Therefore I have some questions:
The following term is well typed in coq:
  Universe u.
  Check forall A:Type@{u+1}, Type@{u}.
I.e. the argument type of a function type can live in a higher universe than the result type. If I try the same with an inductive type, I get an error.
  Inductive lst (A: Type@{u+1}): Type@{u} :=
  | nil: lst A
  | cons: A -> lst A -> lst A.
  *Error:*Universe inconsistency. Cannot enforce u = max(Set, u+1).
What is the theoretical background of this consistency error. The type of ‘lst’ is exactly the type I have checked above as well typed. I suspect that if it were well typed, then I could ‘hide’ an object from the universe ‘u+1’ in the list which resides in the universe ‘u’. Can anybody help to give a more precise explanation.
Regards
Helmut





Archive powered by MHonArc 2.6.19+.

Top of Page