[Agda] Telescope syntax

[Guillaume Brunerie]

Le 26 nov. 2014 16:08, "Jesper Cockx" <Jesper at sikanda.be> a écrit :
>
> 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.

Yes, that seems right. I haven't really followed the discussion on grouping
of arguments in Tallinn, but it does sound close.

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

The advantage of the later is that you can factor the three Level
arguments, so it's shorter when you have to write it by hand, but it would
make much more sense to have it translated to the former.

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

That makes sense for postulates for instance, but not for function
definitions, if you want to define a function of type Group -> Group, then
you have to provide the group structure on the result and it might be
nontrivial.

> 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
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20141127/60ed5077/attachment.html