[Agda] new generalize feature, first version

[Nils Anders Danielsson]

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}

-- 
/NAD