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

Thu May 17 15:49:16 CEST 2018

Indeed; to give another little data point, my personal experience is that I use --type-in-type with Agda almost always, and check predicativity by hand (usually not that hard, if you aren't doing something which will obviously be bad). I suspect a lot of people work this way, so as far as the social force is concerned, the solution which is eventually adopted in Agda X might need to be not much more bureaucratic than this.

(Personally, I don't mind a little syntactic noise: for instance, I'm fine with explicit levels---in order to get off the ground, I just need at least cumulativity and the ability to shift definitions, whether that is accomplished through polymorphism or through Conor's idea; to me, the really impracticable thing is having to take the join of like 10 universe levels if I am trying to do some algebra or category theory, and then getting utterly owned because even now, I need to use some explicit Lift type to shift something around).

On Thu, May 17, 2018, at 5:30 AM, Philip Wadler wrote:
> 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
> 
> .   \ Philip Wadler, Professor of Theoretical Computer Science,
> .   /\ School of Informatics, University of Edinburgh
> .  /  \ and Senior Research Fellow, IOHK
> . http://homepages.inf.ed.ac.uk/wadler/
> 
> On 17 May 2018 at 05:29, Jesper Cockx <Jesper at sikanda.be> wrote:
> 
> > 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/inde
> >> x.html%3Fp=857&cpage=1.html and https://pigworker.wordpress.co
> >> m/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
> >>
> >
> >
> > _______________________________________________
> > Agda mailing list
> > Agda at lists.chalmers.se
> > https://lists.chalmers.se/mailman/listinfo/agda
> >
> >
> The University of Edinburgh is a charitable body, registered in
> Scotland, with registration number SC005336.