[Agda] new generalize feature, first version

[Peter Divianszky]

>> 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 mean irrelevant, not hidden, you guessed it right.


> 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?

The first one.
I typed in

     {-# OPTIONS --generalize #-}
     data _≡_ {A : Set}(x : A) : (x : A) → Set where
       refl : x ≡ x
     data ⊤ : Set where
       tt : ⊤

     generalize
       {x} : ⊤
       p   : tt ≡ _

     postulate
       foo : p ≡ p

and Agda derived the following type for (foo):

     {x = x₁ : ⊤} (p₁ : tt ≡ x₁) → p₁ ≡ p₁

I guess the indices were added to make names less ambiguous because both 
x and p is in scope. I'll try to improve the result to be instead

     {x : ⊤} (p : tt ≡ x) → p ≡ p

Note that I had to add the name 'x' in (x : A) → Set  in the type of _≡_ 
to achieve this naming.


> 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.

The order of arguments are easy to predict.
If you have

     generalize A B : Set

then

     postulate f :: A → B → B

means

     postulate f :: (A B : Set) → A → B → B

and

     postulate f :: B → A → A

means

     postulate f :: (A B : Set) → B → A → A

The same holds for hidden arguments:
If you have

     generalize A B : T _

then it means

     generalize A : T _
                B : T _

so you have an ordering on metas too.

The given order is respected as far as possible.
The exact algorithm which decides the ordering given the prior ordering 
and the dependencies is easy to understand.
See "smallest-numbered available vertex first" topological sorting at 
https://en.wikipedia.org/wiki/Topological_sorting#Examples

I also have an idea how to give predictable, non-automatically-generated 
names to hidden arguments, but that is not implemented yet.
So both of your wishes can be fulfilled, I hope.


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
 >