[Agda] Blog post: The Agda's New Sorts

[Jon Sterling]

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.

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.

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!

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 https://mazzo.li/epilogue/index.html%3Fp=857&cpage=1.html and https://pigworker.wordpress.com/2015/01/09/universe-hierarchies/), which is where you take serious my rephrasing of Conor's rephrasing of James McKinna's Dictum:

    Never attribute to polymorphism that which is adequately explained by initiality.

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.

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 ;-)

Best,
Jon


On Wed, May 16, 2018, at 12:30 AM, Henning Basold wrote:
> -----BEGIN PGP SIGNED MESSAGE-----
> Hash: SHA512
> 
> Hi Jesper,
> 
> Do you think it would make sense and be feasible to implement
> anonymous universes à la Harper and Pollack in Agda?
> 
> Robert Harper and Robert Pollack. Type checking with universes.
> Theoretical Computer Science, 89:107-136, 1991.
> 
> Cheers,
> Henning
> 
> On 15/05/18 19:09, Thorsten Altenkirch wrote:
> > Hi jesper,
> > 
> > I appreciate your efforts to make universes more flexible and
> > maybe capture other notions of universe than the ones given by
> > size. However, I have another issue with the current mechanism
> > (which I actually proposed many years ago). I don't like that all
> > definitions are cluttered with these pesky level annotations. When
> > teaching an introductory course I don't really want to talk about
> > levels but on the other hand I would like to use the definitions
> > from the standard library and not my own simplified versions.
> > However, whenever I show a library definition I have to instruct
> > them to ignore all those levels for the time being.
> > 
> > Is there a way out of this dilemma? Coq only does fully automatic 
> > indexing but there are many situation where this is not what you
> > want. Is there a way to infer levels and automatically add level
> > annotations but be still able to do the explicitly if you want (or
> > need) to?
> > 
> > Cheers, Thorsten
> > 
> > From: Agda <agda-bounces at lists.chalmers.se 
> > <mailto:agda-bounces at lists.chalmers.se>> on behalf of Jesper Cockx 
> > <Jesper at sikanda.be <mailto:Jesper at sikanda.be>> Date: Friday, 4 May
> > 2018 at 09:45 To: agda list <agda at lists.chalmers.se
> > <mailto:agda at lists.chalmers.se>> Subject: [Agda] Blog post: The
> > Agda's New Sorts
> > 
> > Hi all,
> > 
> > Yesterday I posted a blog post on the recent work I did on Agda's 
> > handling of sorts. You can read it here: 
> > https://jesper.sikanda.be/posts/agdas-new-sorts.html
> > 
> > Any comments are very welcome here on this list!
> > 
> > Cheers, Jesper
> > 
> > 
> > This message and any attachment are intended solely for the
> > addressee and may contain confidential information. If you have
> > received this message in error, please contact the sender and
> > delete the email and attachment.
> > 
> > Any views or opinions expressed by the author of this email do not 
> > necessarily reflect the views of the University of Nottingham.
> > Email communications with the University of Nottingham may be
> > monitored where permitted by law.
> > 
> > 
> > 
> > 
> > 
> > _______________________________________________ Agda mailing list 
> > Agda at lists.chalmers.se 
> > https://lists.chalmers.se/mailman/listinfo/agda
> > 
> -----BEGIN PGP SIGNATURE-----
> 
> iQIzBAEBCgAdFiEEMnUmuprSDishxVMiatBsEc2xMm4FAlr73ggACgkQatBsEc2x
> Mm4hgA//SIhOgEq2b80/yioVsTlglqzseaonHmH3OAULT15yrLIyHNJ0uWSkFmB8
> nfOoiIdpOYFg4Xrq7Bc3zSl0Fa1yLBfx3AOPLE267/BrZvQmdjn/Kzh1MkVJMNRT
> rdfgRD7mCt0UaMGWX2PuoTsh3FqpZ/LXe+R6GIGSWen7yr8ByG85Hd509WgLZ+sM
> TQlPcHn7aebdfJ2GWRwxjab66dySnGRxZ/rRiAFJWsepl7Z5tohsfjdvZ3TCVAOw
> URDTGOAO/opD8nlpz0CeSyt0dl+qr+uem9Ofphd6s7R67PEI4WuYH59kK/QV11Hh
> 3lTC5ZH7obu6tftC6HHPym859ZKxYVXRSwEng1R91BiCkUyr2jmCHkvj6hqH6YiB
> 7MN5mZcqtM9FRt3ZnVYT6BWtm9vMF6IuxBjj3uuPMMnmQEC8ont8NZ8LRN2HW54U
> BD3nNm7fDVZw5R45WWztUIZkJO/rPsIoRw2m4EsWkDtxXDWI3fHTh+yXYIAQnIns
> s72yiaLOOyi9t7FtXzFm07J3B5AlqhFA+nsPUHOOUL/35d4iTl2EZ0mGQ6EWhjgz
> /GtjQvH7P57yBeZGPuT+342JvGAG79FVBgZVr1lv8LQRa0F8TNwP0TAVo1PlKYVl
> lgqdTzAzdkkzh48kMSy4Hkxcyy/bLPuwhkKbIZEUQyyDrM1eQ6k=
> =X8m/
> -----END PGP SIGNATURE-----
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda