<div dir="ltr">Level polymorphism bloats almost every definition in the Standard Prelude. I have avoided it as much as possible in the text I am writing, settling for plain old Set instead, even though that is restrictive. It would be fantastic if Agda could evolve to a less noisy alternative. Cheers, -- P</div><div class="gmail_extra"><br clear="all"><div><div class="gmail_signature" data-smartmail="gmail_signature"><div dir="ltr"><div><div dir="ltr">.   \ Philip Wadler, Professor of Theoretical Computer Science,<br>.   /\ School of Informatics, University of Edinburgh<br></div><div>.  /  \ and Senior Research Fellow, IOHK<br></div><div dir="ltr">. <span><a href="http://homepages.inf.ed.ac.uk/wadler/" target="_blank">http://homepages.inf.ed.ac.uk/wadler/</a></span></div></div></div></div></div>
<br><div class="gmail_quote">On 17 May 2018 at 05:29, Jesper Cockx <span dir="ltr"><<a href="mailto:Jesper@sikanda.be" target="_blank">Jesper@sikanda.be</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr"><div>Thanks Jon for explaining the situation better than I could've! We have indeed considered other forms of handling universes during previous Agda meetings, such as the schematic polymorphism in Coq or Conor's stratified universes. But so far the conclusion was that the benefits were not worth the big architectural overhaul (or more realistically, no-one has had the time to actually implement it).<br></div><div><br></div><div>One other idea to 'tame' Agda's current universe polymorphism would be to put the `Level` type in its own sort rather than in `Set0` where it currently lives. This would allow us to restrict the allowed operations on levels a bit more.<br></div><div><br></div><div>As noted in my blog post, we will hopefully do some experiments with enabling cumulativity in Agda during the next meeting in June. Assuming that goes well we could maybe add an experimental option for it in the next release.</div><span class="HOEnZb"><font color="#888888"><div><br></div><div>-- Jesper<br></div></font></span></div><div class="HOEnZb"><div class="h5"><div class="gmail_extra"><br><div class="gmail_quote">On Wed, May 16, 2018 at 7:01 PM, Jon Sterling <span dir="ltr"><<a href="mailto:jon@jonmsterling.com" target="_blank">jon@jonmsterling.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">In another "universe" (pun intended) this would be lovely :) I think part of the problem is that the Harper/Pollack treatment (which Coq adopted a few years ago) relies in a purely schematic notion of universe level. This is, in my opinion, this right way to do universe polymorphism, but Agda's universe levels are far more flexible: in particular, they are kind of internalized, so that you have a type of levels, and can quantify over them internally.<br>
<br>
While it may be questionable (to me) whether this flexibility is needed in real life, it seems like as a practical matter it would be a very big change to Agda that probably couldn't be made smoothly.<br>
<br>
What I would love is for the next major version of Agda to support cumulativity of universes, regardless of whether levels are explicit; then, separately, one can bolt on the Harper/Pollack algorithm to infer universes if needed; maybe it could even be implemented as a tactic!<br>
<br>
Another approach that seems really attractive to me, which is quite a bit lighter weight, would be to try out Conor McBride's "crude but effective stratification" idea (see <a href="https://mazzo.li/epilogue/index.html%3Fp=857&cpage=1.html" rel="noreferrer" target="_blank">https://mazzo.li/epilogue/inde<wbr>x.html%3Fp=857&cpage=1.html</a> and <a href="https://pigworker.wordpress.com/2015/01/09/universe-hierarchies/" rel="noreferrer" target="_blank">https://pigworker.wordpress.co<wbr>m/2015/01/09/universe-hierarch<wbr>ies/</a>), which is where you take serious my rephrasing of Conor's rephrasing of James McKinna's Dictum:<br>
<br>
    Never attribute to polymorphism that which is adequately explained by initiality.<br>
<br>
The idea is that rather than making your code polymorphic in a universe level, instead, just write it at the lowest level you can, and then have some operation to shift it up and down.<br>
<br>
But all this is speculation about a parallel universe in which Agda didn't already commit to these very fancy internalizable universe levels. I hope we find a wormhole into that reality soon ;-)<br>
<br>
Best,<br>
Jon<br>
<div class="m_-4639276752000787123HOEnZb"><div class="m_-4639276752000787123h5"><br>
<br>
On Wed, May 16, 2018, at 12:30 AM, Henning Basold wrote:<br>
> -----BEGIN PGP SIGNED MESSAGE-----<br>
> Hash: SHA512<br>
> <br>
> Hi Jesper,<br>
> <br>
> Do you think it would make sense and be feasible to implement<br>
> anonymous universes à la Harper and Pollack in Agda?<br>
> <br>
> Robert Harper and Robert Pollack. Type checking with universes.<br>
> Theoretical Computer Science, 89:107-136, 1991.<br>
> <br>
> Cheers,<br>
> Henning<br>
> <br>
> On 15/05/18 19:09, Thorsten Altenkirch wrote:<br>
> > Hi jesper,<br>
> > <br>
> > I appreciate your efforts to make universes more flexible and<br>
> > maybe capture other notions of universe than the ones given by<br>
> > size. However, I have another issue with the current mechanism<br>
> > (which I actually proposed many years ago). I don't like that all<br>
> > definitions are cluttered with these pesky level annotations. When<br>
> > teaching an introductory course I don't really want to talk about<br>
> > levels but on the other hand I would like to use the definitions<br>
> > from the standard library and not my own simplified versions.<br>
> > However, whenever I show a library definition I have to instruct<br>
> > them to ignore all those levels for the time being.<br>
> > <br>
> > Is there a way out of this dilemma? Coq only does fully automatic <br>
> > indexing but there are many situation where this is not what you<br>
> > want. Is there a way to infer levels and automatically add level<br>
> > annotations but be still able to do the explicitly if you want (or<br>
> > need) to?<br>
> > <br>
> > Cheers, Thorsten<br>
> > <br>
> > From: Agda <<a href="mailto:agda-bounces@lists.chalmers.se" target="_blank">agda-bounces@lists.chalmers.s<wbr>e</a> <br>
> > <mailto:<a href="mailto:agda-bounces@lists.chalmers.se" target="_blank">agda-bounces@lists.cha<wbr>lmers.se</a>>> on behalf of Jesper Cockx <br>
> > <<a href="mailto:Jesper@sikanda.be" target="_blank">Jesper@sikanda.be</a> <mailto:<a href="mailto:Jesper@sikanda.be" target="_blank">Jesper@sikanda.be</a>>> Date: Friday, 4 May<br>
> > 2018 at 09:45 To: agda list <<a href="mailto:agda@lists.chalmers.se" target="_blank">agda@lists.chalmers.se</a><br>
> > <mailto:<a href="mailto:agda@lists.chalmers.se" target="_blank">agda@lists.chalmers.se</a><wbr>>> Subject: [Agda] Blog post: The<br>
> > Agda's New Sorts<br>
> > <br>
> > Hi all,<br>
> > <br>
> > Yesterday I posted a blog post on the recent work I did on Agda's <br>
> > handling of sorts. You can read it here: <br>
> > <a href="https://jesper.sikanda.be/posts/agdas-new-sorts.html" rel="noreferrer" target="_blank">https://jesper.sikanda.be/post<wbr>s/agdas-new-sorts.html</a><br>
> > <br>
> > Any comments are very welcome here on this list!<br>
> > <br>
> > Cheers, Jesper<br>
> > <br>
> > <br>
> > This message and any attachment are intended solely for the<br>
> > addressee and may contain confidential information. If you have<br>
> > received this message in error, please contact the sender and<br>
> > delete the email and attachment.<br>
> > <br>
> > Any views or opinions expressed by the author of this email do not <br>
> > necessarily reflect the views of the University of Nottingham.<br>
> > Email communications with the University of Nottingham may be<br>
> > monitored where permitted by law.<br>
> > <br>
> > <br>
> > <br>
> > <br>
> > <br>
> > ______________________________<wbr>_________________ Agda mailing list <br>
> > <a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a> <br>
> > <a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mail<wbr>man/listinfo/agda</a><br>
> > <br>
> -----BEGIN PGP SIGNATURE-----<br>
> <br>
> iQIzBAEBCgAdFiEEMnUmuprSDishxV<wbr>MiatBsEc2xMm4FAlr73ggACgkQatBs<wbr>Ec2x<br>
> Mm4hgA//SIhOgEq2b80/yioVsTlglq<wbr>zseaonHmH3OAULT15yrLIyHNJ0uWSk<wbr>FmB8<br>
> nfOoiIdpOYFg4Xrq7Bc3zSl0Fa1yLB<wbr>fx3AOPLE267/BrZvQmdjn/Kzh1MkVJ<wbr>MNRT<br>
> rdfgRD7mCt0UaMGWX2PuoTsh3FqpZ/<wbr>LXe+R6GIGSWen7yr8ByG85Hd509WgL<wbr>Z+sM<br>
> TQlPcHn7aebdfJ2GWRwxjab66dySnG<wbr>RxZ/rRiAFJWsepl7Z5tohsfjdvZ3TC<wbr>VAOw<br>
> URDTGOAO/opD8nlpz0CeSyt0dl+qr+<wbr>uem9Ofphd6s7R67PEI4WuYH59kK/QV<wbr>11Hh<br>
> 3lTC5ZH7obu6tftC6HHPym859ZKxYV<wbr>XRSwEng1R91BiCkUyr2jmCHkvj6hqH<wbr>6YiB<br>
> 7MN5mZcqtM9FRt3ZnVYT6BWtm9vMF6<wbr>IuxBjj3uuPMMnmQEC8ont8NZ8LRN2H<wbr>W54U<br>
> BD3nNm7fDVZw5R45WWztUIZkJO/rPs<wbr>IoRw2m4EsWkDtxXDWI3fHTh+yXYIAQ<wbr>nIns<br>
> s72yiaLOOyi9t7FtXzFm07J3B5Alqh<wbr>FA+nsPUHOOUL/35d4iTl2EZ0mGQ6EW<wbr>hjgz<br>
> /GtjQvH7P57yBeZGPuT+342JvGAG79<wbr>FVBgZVr1lv8LQRa0F8TNwP0TAVo1Pl<wbr>KYVl<br>
> lgqdTzAzdkkzh48kMSy4Hkxcyy/bLP<wbr>uwhkKbIZEUQyyDrM1eQ6k=<br>
> =X8m/<br>
> -----END PGP SIGNATURE-----<br>
> ______________________________<wbr>_________________<br>
> Agda mailing list<br>
> <a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
> <a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mail<wbr>man/listinfo/agda</a><br>
______________________________<wbr>_________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mail<wbr>man/listinfo/agda</a><br>
</div></div></blockquote></div><br></div>
</div></div><br>______________________________<wbr>_________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/<wbr>mailman/listinfo/agda</a><br>
<br></blockquote></div><br></div>