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

Thu May 17 14:30:40 CEST 2018

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
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20180517/3cc9c1e9/attachment.html>
-------------- next part --------------
An embedded and charset-unspecified text was scrubbed...
Name: not available
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20180517/3cc9c1e9/attachment.ksh>