[Agda] new generalize feature, first version

[Peter Divianszky]

 >> I am not familiar with sections, can you point to a documentation?
 >
 > https://coq.inria.fr/refman/gallina-ext.html#Section

I translated the given Coq example to Agda with 'generalize'.

First try:

     {-# OPTIONS --generalize #-}
     data nat : Set where
       Z : nat
       S : nat → nat

     _+_ : nat → nat → nat
     Z   + m = m
     S n + m = S (n + m)

     -- actual example
     generalize x y : nat
     y' = y
     x' = S x
     x'' = x' + y'

Agda complains that 'Generalizable variable y is not supported here'
and points to the rhs of y' = y.
This is because forall-generalize is supported only in type signatures.
(It would be a separate feature to do something meaningful in the rhs of 
a definition.)

Next try, trying to get as close as possible:

     {-# OPTIONS --generalize #-}
     data nat : Set where
       Z : nat
       S : nat → nat

     _+_ : nat → nat → nat
     Z   + m = m
     S n + m = S (n + m)

     record Sing {A : Set}(a : A) : Set where
       field sing : A

     open Sing

     -- actual example
     generalize x y : nat

     postulate
       y'  : Sing y          -- ^ like in Coq
       x'  : Sing (S x)      -- ^ like in Coq
       x'' : Sing (sing (x' x) + sing (y' y))
       -- ^ unlike in Coq
       -- x'' : Sing (sing x' + sing y')

     {- derived types
     y'  : (y₁ : nat) → Sing y₁
     -- ^ like in Coq
     x'  : (x₁ : nat) → Sing (S x₁)
     -- ^ like in Coq
     x'' : (x₁ y₁ : nat) → Sing (sing (x' x₁) + sing (y' y₁))
     -- ^ unlike in Coq
     -- x'' : (x y : nat) → Sing (sing (x' x) + y)
     -}

The main difference is, that
x' should be applied to x, unlike in Coq.

As Joachim pointed out in another mail, 'this generalizes the variables 
_in each type signature_' unlike section which generalize at the end, once.

So I also conclude that section is a different construct.


On 2018-03-30 19:19, Nils Anders Danielsson wrote:
> On 2018-03-30 10:25, Peter Divianszky wrote:
>> For example,
>>
>>    generalize A {B .C} : Set
>>
>> will generalize A as non-implicit, B as implicit and C as implicit an 
>> hidden.
> 
> Hidden? Do you mean irrelevant?
> 
>>  > 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.
> 
> What does the following code expand to?
> 
>    generalize
>      {x} : ⊤
>      p   : tt ≡ _
> 
>    postulate
>      foo : p ≡ p
> 
> Is it something like
> 
>    postulate
>      foo : {x : ⊤} (p : tt ≡ x) → p ≡ p
> 
> or
> 
>    postulate
>      foo : (p : tt ≡ tt) → p ≡ p?
> 
> Anyway, my main point was that I want it to be easy to understand what
> the type of a definition is. The names of implicit arguments matter, as
> does the order of arguments. When we have discussed this kind of feature
> in the past some issues have come up:
> 
> * Is the order of the arguments unknown (or hard to predict)? In that
>    case it should (IMO) only be possible to give them by name, not by
>    position.
> 
> * Are the names automatically generated? In that case it should (IMO)
>    not be possible to give the arguments by name.
> 
> If you have arguments that can neither be given by position nor by name,
> then this can potentially lead to usability issues.
> 
>> I am not familiar with sections, can you point to a documentation?
> 
> https://coq.inria.fr/refman/gallina-ext.html#Section
>