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

Thu May 17 10:29:36 CEST 2018

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

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.

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.

-- Jesper

On Wed, May 16, 2018 at 7:01 PM, Jon Sterling <jon at jonmsterling.com> wrote:

> 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
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20180517/00e97ec9/attachment.html>