[Agda] Telescope syntax

[Andreas Abel]

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/