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

Discussion:

Jesper Cockx

2018-05-04 08:45:57 UTC

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

Thorsten Altenkirch

2018-05-15 17:09:44 UTC

Permalink

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-***@lists.chalmers.se<mailto:agda-***@lists.chalmers.se>> on behalf of Jesper Cockx <***@sikanda.be<mailto:***@sikanda.be>>
Date: Friday, 4 May 2018 at 09:45
To: agda list <***@lists.chalmers.se<mailto:***@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.

Martin Escardo

2018-05-15 17:28:52 UTC

Permalink

Thorsten,

I do the following (in a base module):

\begin{code}

open import Agda.Primitive using (_⊔_) renaming (lzero to U₀ ; lsuc to
_′ ; Level to Universe) public

_̇ : (U : Universe) → _
U ̇ = Set U -- This should be the only use of the Agda keyword 'Set'.

U₁ = U₀ ′
U₂ = U₁ ′

infix 0 _̇

\end{code}

Notice the almost invisible dot superscript. It is invisible on purpose
(and it almost completely disappears from view when it is followed by
")" or "}").

For example, we write the following instead of

Π : ∀ {i j} {X : Set i} (Y : X → Set j) → Set (i ⊔ j)
Π Y = ∀ x → Y x

\begin{code}

Π : ∀ {U V} {X : U ̇} (Y : X → V ̇) → U ⊔ V ̇
Π Y = ∀ x → Y x

_∘_ : ∀ {U V W} {X : U ̇} {Y : V ̇} {Z : Y → W ̇}
→ Π Z → (f : X → Y) → Π (λ x → Z (f x))
g ∘ f = λ x → g(f x)

\end{code}

The first definition says that X is the universe U and Y is an X-indexed
family of types in the universe V, and then Π Y lives in the first
universe after U and V. Then I consistently use U,V,W for universes. (I
tried the curly versions, but the fonts are not available in all
installations I use, and I don't know how to get them.)

(Also I avoid "Set" because in univalent mathematics not all elements of
"Set j" are sets, and curly "U" is (aptly) used in the HoTT book for
universes.)

Martin

Post by Thorsten Altenkirch
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
Date: Friday, 4 May 2018 at 09:45
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
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
https://lists.chalmers.se/mailman/listinfo/agda

--
Martin Escardo
http://www.cs.bham.ac.uk/~mhe

Henning Basold

2018-05-16 07:30:25 UTC

Permalink

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

Post by Thorsten Altenkirch
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
Agda's New Sorts
Hi all,
Yesterday I posted a blog post on the recent work I did on Agda's
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
https://lists.chalmers.se/mailman/listinfo/agda

Jon Sterling

2018-05-16 17:01:33 UTC

Permalink

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

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

Post by Thorsten Altenkirch
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
Agda's New Sorts
Hi all,
Yesterday I posted a blog post on the recent work I did on Agda's
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
https://lists.chalmers.se/mailman/listinfo/agda

Jon Sterling

2018-05-17 13:49:16 UTC

Permalink

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

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/

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

Post by 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/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
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

Post by Thorsten Altenkirch
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
Agda's New Sorts
Hi all,
Yesterday I posted a blog post on the recent work I did on Agda's
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
https://lists.chalmers.se/mailman/listinfo/agda

_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda

The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.