[Agda] Telescope syntax

[Andreas Abel]

If the generalization includes the "free variable feature" (see Twelf, 
Coq, http://www.cs.mcgill.ca/~bpientka/papers/recon-jfp.pdf), then you 
could write

   {{ _ : GroupStr G }} -> ...

and it would quantify over G and the meta variables it had to create 
during checking this type, so

   {#i : Level} {G : Set #i} {{ _ : GroupStr G }} -> ...

The eligible free variables (like G) should be declared in some form 
(see Coq's Generalize declaration).

Cheers,
Andreas

On 27.11.2014 15:25, Guillaume Brunerie wrote:
> 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
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>


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