<!DOCTYPE html>
<html>
<head>
<title></title>
</head>
<body><div>Yes, I suppose my reasoning for bringing up Nuprl was that it seems to be more applicable to Agda than Coq, since Nuprl is a fully predicative theory and, like Agda, it takes propositions-as-types seriously unlike Coq; i.e. Prop[i] is a synonym for Univ[i], and the various "logical style" connectives are just synonyms for their propositions-as-types analogues.<br></div>
<div> </div>
<div>Kind regards,<br></div>
<div>Jon<br></div>
<div> </div>
<div> </div>
<div> </div>
<div>On Wed, Nov 26, 2014, at 09:07 AM, Liam O'Connor wrote:<br></div>
<blockquote type="cite" style="margin: 15px 0px;"><div style="margin-top: 0px;"><p style="-webkit-margin-before: 0px; margin: 15px 0px;">For the record, NuPRL’s approach is summarised here:<br></p><p style="margin: 15px 0px;">http://www.cs.cornell.edu/home/sfa/Nuprl/NuprlPrimitives/Xuniverse_doc.html<br></p><p style="margin: 15px 0px;">http://www.cs.cornell.edu/home/sfa/Nuprl/NuprlPrimitives/Xtype_functionality_sequents_doc.html<br></p><p style="margin: 15px 0px;">From what I can tell, NuPRLs approach is much the same as Agda, with universe polymorphism and a hierarchy of universes, although it distinguishes between Type and Prop, and from what I can tell it has cumulativity, unlike Agda.<br></p><p style="margin: 15px 0px;">Jon, did you mean “why does Agda not have cumulativity?”<br></p><p style="margin: 15px 0px;"><br></p></div>
<div><div style="font-family:Helvetica,Arial;font-size:13px; color: rgba(0,0,0,1.0); margin: 0px; line-height: auto;"> </div>
<div> </div>
<div><span class="font" style="font-family:helvetica, arial"><span class="size" style="font-size:13px"></span></span>-- <br></div>
<div>Liam O'Connor<br></div>
<div><span>Sent with Airmail</span><br></div>
<div> </div>
<p style="color: rgb(0, 0, 0); margin: 15px 0px;">On 27 November 2014 at 3:43:06 am, Jon Sterling (<a href="mailto:jon@jonmsterling.com" style="text-decoration: none; background-color: inherit; color: rgb(65, 131, 196);">jon@jonmsterling.com</a>) wrote:<br></p><blockquote type="cite" style="margin: 15px 0px;"><span style="margin-bottom: 0px; margin-top: 0px;"><div><div> </div>
<div><div>Perhaps this is the wrong place to ask, but I am wondering if
there is something I can read about why Agda does the universe
hierarchy, which even with syntactic sugar, is a little bit tiring
to use—as opposed to the approach used in Nuprl, and soon (I
think), in Coq? My assumption has always been that nobody had got
around to doing it, which is fine since it is difficult to
implement, but I wanted to be sure I wasn't missing more
foundational.<br></div>
<div> </div>
<div>Thanks very much,<br></div>
<div>Jon<br></div>
<div> </div>
<div> </div>
<div>On Wed, Nov 26, 2014, at 07:07 AM, Jesper Cockx
wrote:<br></div>
<blockquote type="cite" style="margin: 15px 0px;"><div dir="ltr" style="margin-top: 0px;"><div>I think this would be a very nice thing to reduce the
verbosity of using universe polymorphism. A few
remarks:<br></div>
<div> </div>
<div>- If I understand correctly, a telsyntax statement would
always contain exactly one visible argument plus any number of
hidden and instance arguments before and after? This looks very
similar to the idea Andreas proposed in Tallinn for changing the
<i>internal</i> representation of hidden function types. So your
proposal could be seen as a concrete syntax for this new internal
representation.<br></div>
<div> </div>
<div>- Do you want (A B C : Type) to be translated to {i : Level}
(A : Set i) {j : Level} (B : Set j) {k : Level} (C : Set k), or to
{i j k : Level} (A : Set i) (B : Set j) (C : Set k)? I usually
write the latter, though the former is more consistent with the
idea of grouping hidden arguments with a visible
argument.<br></div>
<div> </div>
<div>- There is a way to make sense of having Type and Group as the
return type of a function: "f : ... -> Type" just stands for "f
: ... -> Set _", and "g : ... -> Group0" stands for "g : ...
-> Set", but using g also brings a term of type "GroupStr (g
...)" into scope for instance resolution. Then you could make (A :
Set) a synonym for {i : Level} (A : Set i) instead of (A : Set0),
so that functions that look non-level-polymorphic can actually be
used at any level.<br></div>
<div> </div>
<div>Cheers,<br></div>
<div>Jesper<br></div>
</div>
<div><div> </div>
<div><div>On Wed, Nov 26, 2014 at 2:33 PM, Guillaume Brunerie <span dir="ltr"><<a href="mailto:guillaume.brunerie@gmail.com" target="_blank" style="text-decoration: none; background-color: inherit; color: rgb(65, 131, 196);">guillaume.brunerie@gmail.com</a>></span>
wrote:<br></div>
<blockquote style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Hello all,<br style="margin-top: 0px;"> <br>
As is well known, it’s currently a bit annoying to use
universe<br>
polymorphism in Agda because instead of writing<br> <br>
f : (A B C : Type) -> …<br> <br>
you have to write<br> <br>
f : {i j k : Level} (A : Set i) (B : Set j) (C : Set k)
-> …<br> <br>
Would it be a good idea to make the first one a syntactic sugar
for<br>
the second one?<br>
I’m thinking about adding a "telsyntax" keyword, such that you
can<br>
write for instance<br> <br>
telsyntax {i : Level} (X : Set i) = (X : Type)<br> <br>
and then (A B C : Type) (in a telescope) would be automatically
translated into<br> <br>
{i : Level} (A : Set i) {j : Level} (B : Set j) {k : Level}
(C : Set k)<br> <br>
And this is not just about universe management, but it would also
be<br>
very useful when using instance arguments. For instance if a group
is<br>
a type (of level 0, say) with a group structure (which will be
found<br>
by instance search), and you want to write a function taking
three<br>
groups as arguments you have to write<br> <br>
g : (G H K : Set) {{_ : GroupStr G}} {{_ : GroupStr H}} {{_
:<br>
GroupStr K}} -> …<br> <br>
But you could say instead<br> <br>
telsyntax (G : Set) {{_ : GroupStr G}} = (G : Group0)<br>
g : (G H K : Group0) -> …<br> <br>
And of course you can combine the two, if groups can be at
any<br>
universe level then the following:<br> <br>
telsyntax {i : Level} (G : Set i) {{_ : GroupStr G}} = (G :
Group)<br>
g : (G H K : Group) -> …<br> <br>
would be a shorthand for<br> <br>
g : {i j k : Level} {G : Set i} {H : Set j} {K : Set k} {{_
:<br>
GroupStr G}} {{_ : GroupStr H}} {{_ : GroupStr K}} -> …<br> <br>
which is much less readable and annoying to write.<br> <br>
One drawback (in the case of universe levels) is that you don’t
have<br>
access to the level anymore, but I don’t think that would really be
a<br>
problem, and you still can make the levels explicit if you need
to.<br>
Another drawback is that when writing (A : Type) or (G : Group) in
a<br>
telescope, it makes it look like Type and Group are types, but
it’s<br>
not the case so it could be confusing (for instance you can’t end
a<br>
function with "-> Group"). If that’s indeed too confusing, maybe
we<br>
could use a different notation than a colon, to make it clear
that<br>
it’s just syntactic sugar (on the other hand, it looks nice with
a<br>
colon).<br> <br>
What do you think?<br> <br>
Guillaume<br>
_______________________________________________<br>
Agda mailing list<br> <a href="mailto:Agda@lists.chalmers.se" style="text-decoration: none; background-color: inherit; color: rgb(65, 131, 196);">Agda@lists.chalmers.se</a><br> <a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank" style="margin-bottom: 0px; text-decoration: none; background-color: inherit; color: rgb(65, 131, 196);">https://lists.chalmers.se/mailman/listinfo/agda</a></blockquote></div>
<div> </div>
</div>
<div><u>_______________________________________________</u><br></div>
<div>Agda mailing list<br></div>
<div><a href="mailto:Agda@lists.chalmers.se" style="text-decoration: none; background-color: inherit; color: rgb(65, 131, 196);">Agda@lists.chalmers.se</a><br></div>
<div style="margin-bottom: 0px;"><a href="https://lists.chalmers.se/mailman/listinfo/agda" style="text-decoration: none; background-color: inherit; color: rgb(65, 131, 196);">https://lists.chalmers.se/mailman/listinfo/agda</a><br></div>
</blockquote><div> </div>
<div>_______________________________________________
<br></div>
<div>Agda mailing list
<br></div>
<div>Agda@lists.chalmers.se
<br></div>
<div>https://lists.chalmers.se/mailman/listinfo/agda
<br></div>
</div>
</div>
</span></blockquote></div>
<div style="margin-bottom: 0px;"><p style="-webkit-margin-before: 0px; margin: 15px 0px;"><br></p></div>
</blockquote><div> </div>
</body>
</html>