[Agda] Why aren't free vars in types automatically generalized

[Robert J. Simmons]

In Twelf, you can effectively specify implicit arguments by giving a
type annotation. If I have this Twelf signature

 nat : type.
 z : nat.
 s : nat -> nat.

 plus : nat -> nat -> nat -> type.
 pz : plus z N N.
 ps : plus N M P -> plus (s N) M (s P).

 q = ps.
 p = (ps : plus N N N -> plus (s N) N (s N))

Then q has three implicit natural number arguments and p has one
implicit natural number argument (N). Am I right that Agda doesn't
have a similar annotation syntax? I've always been able to add
implicit vars when I've wanted to insert a type annotation, so perhaps
annotations aren't necessary when you can give implicit vars.

 - Rob

On 3/30/09, Stefan Monnier <monnier at iro.umontreal.ca> wrote:
>>> Whichever option you choose, Twelf requires you to stick with your
>>> choice.
>> Assuming that we have the definitions
>
>>  Ctxt : Set
>>  Ty   : Ctxt → Set
>>  Tm   : Ty Γ → Set  (meaning ∀ {Γ} → Ty Γ → Set)
>>  ⋆    : Ty Γ        (meaning ∀ {Γ} → Ty Γ),
>
>> does this mean that there is no direct way to write
>>  El : ∀ {Γ} → Tm (⋆ {Γ}) → Ty Γ  ?
>
> Indeed: Twelf does not provide the user any way to explicitly specify an
> implicit argument.  So you wouldn't define
>
>     ⋆    : Ty Γ
> but
>     ⋆    : ∀ (Γ) → Ty Γ
>
> I haven't used Twelf enough to know if it occurs often that parameters
> can usually be inferred, but not always.
>
> The choice of how to pass implicit args explicitly (in the case of
> Twelf: never) and the use of free-vars-are-implicit-args are mostly
> independent, AFAIK.  Except obviously that if you can't pass implict
> args explicitly, you don't need to worry about ordering of
> implicit args.
>
>
>         Stefan
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>