[Agda] Telescope syntax

Wed Nov 26 18:39:27 CET 2014

Jason,

Yes, I have had a similar conversation with Bob, though I cannot say
that I have fully digested either Bob's old paper, or Matthieu's recent
work on Coq more deeply than to just be aware of it.

Kind regards, Jon

On Wed, Nov 26, 2014, at 09:35 AM, Jason Gross wrote:
> I have heard that the universe inference & checking algorithm Matthieu
> has implemented for the upcoming version of Coq was based on a
> (1990s?) paper by Harper et al on universe polymorphism, and from
> discussions with Bob Harper. I assume from this, and from what I've
> heard from Bob, that NuPRL, like the upcoming version of Coq, uses
> inferrered universe levels and the syntax of typical ambiguity, so
> that the universes mostly happen behind the scenes and are invisible
> to users.
>
> On 12:07pm, Wed, Nov 26, 2014 Liam O'Connor
> <liamoc at cse.unsw.edu.au> wrote:
>> For the record, NuPRL’s approach is summarised here:

>> http://www.cs.cornell.edu/home/sfa/Nuprl/NuprlPrimitives/Xuniverse_doc.html

>> http://www.cs.cornell.edu/home/sfa/Nuprl/NuprlPrimitives/Xtype_functionality_sequents_doc.html

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

>> Jon, did you mean “why does Agda not have cumulativity?”

>>

>>
>>
>>
>> --
>> Liam O'Connor Sent with Airmail
>>
>> On 27 November 2014 at 3:43:06 am, Jon Sterling
>> (jon at jonmsterling.com) wrote:

>>>
>>> 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.
>>>
>>> Thanks very much, Jon
>>>
>>>
>>> On Wed, Nov 26, 2014, at 07:07 AM, Jesper Cockx
wrote:
>>>> I think this would be a very nice thing to reduce the
verbosity of using universe polymorphism. A few remarks:
>>>>
>>>> - 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
>>>> *internal* representation of hidden function types. So your
proposal could be seen as a concrete syntax for this new internal
representation.
>>>>
>>>> - 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.
>>>>
>>>> - 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.
>>>>
>>>> Cheers, Jesper
>>>>
>>>> On Wed, Nov 26, 2014 at 2:33 PM, Guillaume Brunerie
>>>> <guillaume.brunerie at gmail.com>
wrote:
>>>>> Hello all,
>>>>>
>>>>>
As is well known, it’s currently a bit annoying to use universe
>>>>>
polymorphism in Agda because instead of writing
>>>>>
>>>>>
f : (A B C : Type) -> …
>>>>>
>>>>>
you have to write
>>>>>
>>>>>
f : {i j k : Level} (A : Set i) (B : Set j) (C : Set k) -> …
>>>>>
>>>>>
Would it be a good idea to make the first one a syntactic sugar for
>>>>>
the second one?
>>>>>
I’m thinking about adding a "telsyntax" keyword, such that you can
>>>>>
write for instance
>>>>>
>>>>>
telsyntax {i : Level} (X : Set i) = (X : Type)
>>>>>
>>>>>
and then (A B C : Type) (in a telescope) would be automatically
translated into
>>>>>
>>>>>
{i : Level} (A : Set i) {j : Level} (B : Set j) {k : Level} (C : Set k)
>>>>>
>>>>>
And this is not just about universe management, but it would also be
>>>>>
very useful when using instance arguments. For instance if a group is
>>>>>
a type (of level 0, say) with a group structure (which will be found
>>>>>
by instance search), and you want to write a function taking three
>>>>>
groups as arguments you have to write
>>>>>
>>>>>
g : (G H K : Set) {{_ : GroupStr G}} {{_ : GroupStr H}} {{_
:
>>>>>
GroupStr K}} -> …
>>>>>
>>>>>
But you could say instead
>>>>>
>>>>>
telsyntax (G : Set) {{_ : GroupStr G}} = (G : Group0)
>>>>>
g : (G H K : Group0) -> …
>>>>>
>>>>>
And of course you can combine the two, if groups can be at any
>>>>>
universe level then the following:
>>>>>
>>>>>
telsyntax {i : Level} (G : Set i) {{_ : GroupStr G}} = (G : Group)
>>>>>
g : (G H K : Group) -> …
>>>>>
>>>>>
would be a shorthand for
>>>>>
>>>>>
g : {i j k : Level} {G : Set i} {H : Set j} {K : Set k} {{_
:
>>>>>
GroupStr G}} {{_ : GroupStr H}} {{_ : GroupStr K}} -> …
>>>>>
>>>>>
which is much less readable and annoying to write.
>>>>>
>>>>>
One drawback (in the case of universe levels) is that you don’t have
>>>>>
access to the level anymore, but I don’t think that would really be a
>>>>>
problem, and you still can make the levels explicit if you need to.
>>>>>
Another drawback is that when writing (A : Type) or (G : Group) in a
>>>>>
telescope, it makes it look like Type and Group are types, but it’s
>>>>>
not the case so it could be confusing (for instance you can’t end a
>>>>>
function with "-> Group"). If that’s indeed too confusing, maybe we
>>>>>
could use a different notation than a colon, to make it clear that
>>>>>
it’s just syntactic sugar (on the other hand, it looks nice with a
>>>>>
colon).
>>>>>
>>>>>
What do you think?
>>>>>
>>>>>
Guillaume
>>>>>
_______________________________________________
>>>>>
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
>> _________________________________________________
>>
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/20141126/ca52d448/attachment-0001.html