[Agda] Telescope syntax

[Andreas Abel]

On 27.11.2014 11:28, Guillaume Brunerie wrote:
> I'm not sure what you mean. When using (X : Type) in my proposed syntax,
> you don't give a name to the i, hence it will be autogenerated by Agda
> so there will be no way to refer back to it by name.

Same for generalization.

> What you can do instead if you need the level somewhere, is to define
> the following function:
>
> get-level : (X : Type) -> Level
> get-level {i} _ = i
>
> And then [get-level X] returns the universe level of X.
>
> Also, in Coq why do you have to give specific names to be generalized?
> Why not generalize every variable which is not in scope?

Well, this would throw us back to the age of BASIC where a missspelled 
identifier does not lead to a syntax error but changes the semantics 
silently...

> Le 27 nov. 2014 00:07, "Matthieu Sozeau" <matthieu.sozeau at gmail.com
> <mailto:matthieu.sozeau at gmail.com>> a écrit :
>  >
>  > 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
> <mailto: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
> <mailto: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 <mailto:Agda at lists.chalmers.se>
>  > >> https://lists.chalmers.se/mailman/listinfo/agda
>  > >
>  > > _______________________________________________
>  > > Agda mailing list
>  > > Agda at lists.chalmers.se <mailto:Agda at lists.chalmers.se>
>  > > https://lists.chalmers.se/mailman/listinfo/agda
>  >
>  > _______________________________________________
>  > Agda mailing list
>  > Agda at lists.chalmers.se <mailto: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/