[Agda] Telescope syntax

[Andreas Abel]

It is probably more like the pattern synonym facility, so, it would be

   telescope (G : Group) = (G : Set) {{_ : IsGroup G }}
   telescope (X : Type ) = {i : Level} (X : Set i)

It seems like you want first-class Sigma/record types with exactly one 
visible component (all others hidden/instance) and further some way to 
abbreviate it.  In this case, one could just write e.g.

   telescope Group = (G : Set) {{IG : IsGroup G}}
   telescope Type  = {i : Level} (_ : Set i)

since there is exactly one visible component.

Cheers,
Andreas

On 27.11.2014 11:30, Guillaume Brunerie wrote:
> Oh, I see, I forgot that "syntax" provides the syntax of a specific
> identifier (I don’t use it very often).
> Good, we can have it in the forward direction then :)
>
> 2014-11-27 11:05 GMT+01:00 Ulf Norell <ulf.norell at gmail.com>:
>> The reason syntax declarations are 'backwards' is that they should be read
>> as providing the syntax for a particular identifier. For instance,
>>
>>    syntax foo x y z = [ x / y ]- z
>>
>> defines the syntax of foo to be the thing on the right. Having it the other
>> way around would give you the wrong idea of what's going on. In particular
>> you'd expect to be able do write things like
>>
>>    syntax [ x ] = x :: []
>>
>> or
>>
>>    syntax [ x / y ]- z = foo x y z
>>    syntax [ x /]- z = foo x x z
>>
>> The backwards direction doesn't make sense for the telescope syntax though.
>> In that case you are defining a new name (like 'Type' or 'Group') so that
>> should go on the left (in my opinion).
>>
>> / Ulf
>>
>> On Thu, Nov 27, 2014 at 10:25 AM, Guillaume Brunerie
>> <guillaume.brunerie at gmail.com> wrote:
>>>
>>> (apparently something got wrong with my previous email, trying again...)
>>>
>>> I have no idea why the "syntax" syntax is backwards, but I thought it
>>> would make more sense to have both of them backwards rather than having them
>>> in different directions.
>>>
>>> Le 27 nov. 2014 10:21, "Guillaume Brunerie" <guillaume.brunerie at gmail.com>
>>> a écrit :
>>>
>>>>> 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.
>>>>>>
>>>>>> _______________________________________________
>>>>>> 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
>


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