[Agda] new generalize feature, first version

[Peter Divianszky]

 > Do you also allow Γ : Con and ⦃ Γ ⦄ : Con?

Yes, it is also allowed.
For example,

   generalize A {B .C} : Set

will generalize A as non-implicit, B as implicit and C as implicit an 
hidden.
'generalize' allows anything which is allowed after a 'field' keyword.

 > I wonder what happens if some name like Γ is both declared to be
 > generalizable and declared as a regular name (perhaps in another
 > module). Is this treated as an error?

Yes, this is treated as an error.
'generalize' introduce new definitions into the scope like 'postulate'.

 > I think that I might prefer more easily predictable types. If we skip
 > the magic underscores, then we get that, at the cost of more verbosity:
 >
 >    generalize
 >      {Γ Δ Θ} : Con
 >      {A B}   : Ty Γ
 >      {C}     : Ty Δ
 >
 > Now it is obvious what the names of the arguments are and how they are
 > ordered: just drop the parts of the telescope that are unused.
 >
 > This also allows you to have regular underscores in the types:
 >
 >    generalize
 >      {p} : tt ≡ _

The implementation does exactly this.
Your examples are already valid. Both recursive generalize (like in your 
first example) and generalize with meta (like in your second example) is 
valid.


About sections:

I am not familiar with sections, can you point to a documentation?
Are the following statements true for sections? (they are true for 
'generalize')

1) if you generalize over A, B and C but you use only A then only A is 
added to the signature

2) metavariables are solved on-demand
    for example, A and B is generalized, both of type (Ty _) then '_' 
may or may not coincide or refer to each-other, depending on the usage 
of A and B in the type signature

3) unsolved metavariables can be generalized (in a controlled way)




On 2018-03-29 18:23, Nils Anders Danielsson wrote:
> On 2018-03-29 14:13, Peter Divianszky wrote:
>> I implemented a first version of forall-generalization, and I would
>> like to get feedback on it.
> 
> I've wanted something like this for quite some time now. I sometimes
> omit implicit argument declarations when presenting Agda code in papers,
> and I'd prefer to be able to present actual Agda code snippets.
> 
>> There is a new keyword 'generalize', which accept declarations like
>> 'field' for records:
>>
>> generalize
>>    {Γ Δ Θ} : Con
>>    {A B C} : Ty _
>>    {σ δ ν} : Sub _ _
>>    {t u v} : Tm _ _
> 
> Do you also allow Γ : Con and ⦃ Γ ⦄ : Con?
> 
>> - avoid accidental generalization
>>    - only the given names are generalized
>>    - the type of generalizable variables are checked
>>      against the given schema, which adds extra safety
> 
> I wonder what happens if some name like Γ is both declared to be
> generalizable and declared as a regular name (perhaps in another
> module). Is this treated as an error?
> 
>> - Name the generalized metavariables also according by the given
>>   generalizable variables. For example, if _1 : Con, then take the
>>   first freely available <Name> : Con, where <Name> was defined by
>>   'generalize'. If no more names are available, stop with an error
>>   message.
> 
> I think that I might prefer more easily predictable types. If we skip
> the magic underscores, then we get that, at the cost of more verbosity:
> 
>    generalize
>      {Γ Δ Θ} : Con
>      {A B}   : Ty Γ
>      {C}     : Ty Δ
> 
> Now it is obvious what the names of the arguments are and how they are
> ordered: just drop the parts of the telescope that are unused.
> 
> This also allows you to have regular underscores in the types:
> 
>    generalize
>      {p} : tt ≡ _
> 
>> - What should be the keyword?
> 
> The variant that I have described is similar to sections in Coq. Perhaps
> the following notation (which introduces a block) could be used:
> 
>    section {Γ : Ctxt} … where
> 
> This is similar to "module _ <telescope> where", but with the "drop
> unused bindings" semantics.
> 
>> For Agda implementors
> 
> Would the changes I suggested above make the implementation easier for
> you?
> 
>> Plans (not implemented yet)
>>
>> - automatic generalization of record fields and constructor types
> 
> Jesper Cockx and I discussed sections recently, and came to the
> conclusion that it might be nice to allow sections inside data and
> record type declarations:
> 
>    data D (A : Set) : Set where
>      ⋮
> 
>    data P {A : Set} : D A → D A → Set where
>      section {x y : D A} where
>        c₁ : P x x
>        c₂ : P x y → P y x
>        ⋮
> 
> Note that this isn't quite code that I would like to present in a paper:
> I would probably often hide the section line. However, hiding the
> section line is easy when using agda --latex (and could presumably be
> automated), whereas hacks like the following one are complicated and
> error prone:
> 
>    \begin{code}[hide]
>      module Hack {x y : D A} where
>    \end{code}
>    \begin{code}
>        data P {A : Set} : D A → D A → Set where
>          c₁ : P x x
>          c₂ : P x y → P y x
>    \end{code}
>    \begin{code}[hide]
>      data P {A : Set} : D A → D A → Set where
>        c₁ : ∀ {x} → P x x
>        c₂ : ∀ {x y} → P x y → P y x
>    \end{code}
>