[Agda] Telescope syntax

[Guillaume Brunerie]

I don’t really see how generalization would work for the Group example.
If you write {{Gstr : GroupStr _}}, then I guess it would be the same
as {#i : Level} {#G : Set #i} {{Gstr : GroupStr #G}} (where #i and #G
are autogenerated by Agda), but then you only have a name for the
group structure and not for the group itself, which seems a bit silly.
And with a mechanism similar to the one in Coq, I guess you would
write {{_ : GroupStr G}} which is turned into {#i : Level} {G : Set
#i} {{_ : GroupStr G}}, which seems good (except that we may want the
G argument to be explicit), but it seems different from what you mean
by generalization, because here we’re generalizing the out-of-scope
variable G and not an underscore.

2014-11-27 7:50 GMT+01:00 Andreas Abel <abela at chalmers.se>:
> Maybe instead of telsyntax someone could sit down an implement
> generalization, which would probably cover what telsyntax does but be more
> useful in general.
>
> If Agda treated (*)
>
>   (A B C : Set _) -> Bla
>
> as
>
>   (A : Set _) (B : Set _) (C : Set _) -> Bla
>
> then Agda could generalize over the three level metas (provided they remain
> unconstrained) and produce
>
>   {i j k : Level} (A : Set i) (B : Set j) (C : Set k) -> ...
>
> The same would work for the "Group" example, I suppose.
>
> (*) The semantics of (A B C : Set _) -> ... is that A B C live at the same
> level, however,
>
>   forall A B C -> Bla
>
> does not impose such constraints and might be sufficient in practice. If
> not, one could introduce a syntax for an alternative underscore that does
> not insist to be filled with the same value in all of its copies.
>
> Cheers,
> Andreas
>
>
> On 27.11.2014 00:07, Matthieu Sozeau wrote:
>>
>> Hi,
>>
>>    It seems you’re gonna have to invent names for the i’s…
>> Coq has a similar feature using a generalizable variables syntax
>> whereby you can declare some names to be generalized (e.g. A B i j k)
>> and then writing `(X : Type i) will add an implicit {i} binder just before
>> (x : Type i). The backquote can actually be put anywhere and will
>> introduce
>> pi’s or lambdas according to whether we’re in type or (term or unknown)
>> position for the generalizable variable occurrences appearing in it’s
>> scope.
>> It was introduced for type class instance arguments mainly, allowing
>> compact `{Eq A} binders for example. It can also introduce automagically
>> named
>> binders for superclasses but it’s seldom used. I just want to point out
>> that
>> if you allow this then further references to constants using telsyntax
>> should probably not be allowed to refer to the generated names :)
>>
>> Best,
>> — Matthieu
>>
>> On 26 nov. 2014, at 22:11, Andy Morris <andy at adradh.org.uk> wrote:
>>
>>> It's backwards the same way the current syntax declarations are, and
>>> presumably for the same reason.
>>>
>>>> On 26 Nov 2014, at 22:08, Felipe Lessa <felipe.lessa at gmail.com> wrote:
>>>>
>>>> On 26-11-2014 11:33, Guillaume Brunerie wrote:
>>>>>
>>>>> telsyntax {i : Level} (X : Set i) = (X : Type)
>>>>
>>>>
>>>> I hope this isn't an obvious question, but isn't this syntax backwards?
>>>> Shouldn't it be like below?
>>>>
>>>> telsyntax (X : Type) = {i : Level} (X : Set i)
>>>>
>>>> Cheers, :)
>>>>
>>>> --
>>>> Felipe.
>
>
>
>
> --
> Andreas Abel  <><      Du bist der geliebte Mensch.
>
> Department of Computer Science and Engineering
> Chalmers and Gothenburg University, Sweden
>
> andreas.abel at gu.se
> http://www2.tcs.ifi.lmu.de/~abel/
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda