[Agda] new generalize feature, first version

This post might be inappropriate. Click to display it.

Peter Divianszky

2018-03-30 08:25:42 UTC

Post by Nils Anders Danielsson
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.

Post by Nils Anders Danielsson
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'.

Post by Nils Anders Danielsson
I think that I might prefer more easily predictable types. If we skip
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.
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)

Post by Peter Divianszky
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.

Post by Peter Divianszky
There is a new keyword 'generalize', which accept declarations like
generalize
   {Γ Δ Θ} : Con
   {A B C} : Ty _
   {σ δ ν} : Sub _ _
   {t u v} : Tm _ _

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

Post by Peter Divianszky
- 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?

Post by Peter Divianszky
- 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
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.
generalize
    {p} : tt ≡ _

Post by Peter Divianszky
- What should be the keyword?

The variant that I have described is similar to sections in Coq. Perhaps
section {Γ : Ctxt} … where
This is similar to "module _ <telescope> where", but with the "drop
unused bindings" semantics.

Post by Peter Divianszky
For Agda implementors

Would the changes I suggested above make the implementation easier for
you?

Post by Peter Divianszky
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
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
      ⋮
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
\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}

Nils Anders Danielsson

2018-03-30 17:19:46 UTC

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

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.

Post by Peter Divianszky
I am not familiar with sections, can you point to a documentation?

https://coq.inria.fr/refman/gallina-ext.html#Section

--
/NAD

Peter Divianszky

2018-03-30 20:27:36 UTC

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

Post by Nils Anders Danielsson
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.

Post by Nils Anders Danielsson
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
* 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.

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

Post by Nils Anders Danielsson
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
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.
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
* 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.

Post by Peter Divianszky
I am not familiar with sections, can you point to a documentation?

https://coq.inria.fr/refman/gallina-ext.html#Section

Nils Anders Danielsson

2018-03-30 20:55:36 UTC

Post by Nils Anders Danielsson
What does the following code expand to?
[...]

The first one.

This means that meta-variables do not have their usual meaning under
generalize. Perhaps it would be better to use a different notation for
the magic meta-variables.

Post by Peter Divianszky
{x = x₁ : ⊤} (p₁ : tt ≡ x₁) → p₁ ≡ p₁
[...]
{x : ⊤} (p : tt ≡ x) → p ≡ p

These two types are definitionally equal.

Post by Peter Divianszky
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.

One property I did not bring up was that of stability. I hope that we
will not end up in a situation in which one can break lots of code by,
say, adding one variable name to a generalize block.

--
/NAD

Peter Divianszky

2018-03-30 22:00:35 UTC

Post by Nils Anders Danielsson
[...]

The first one.

This means that meta-variables do not have their usual meaning under
generalize. Perhaps it would be better to use a different notation for
the magic meta-variables.

All right, the syntax can be changed to be less confusing.

Post by Peter Divianszky
{x = x₁ : ⊤} (p₁ : tt ≡ x₁) → p₁ ≡ p₁
[...]
{x : ⊤} (p : tt ≡ x) → p ≡ p

These two types are definitionally equal.

Right, I just wanted to be precise with naming.
The former is the current type signature and the latter is the desired one.

Post by Nils Anders Danielsson
One property I did not bring up was that of stability. I hope that we
will not end up in a situation in which one can break lots of code by,
say, adding one variable name to a generalize block.

My idea would be stable in this sense.
Adding a new variable to a generalize block would be conservative, so
more programs would be accepted and previous code would not change.

The idea is that type checking would halt with an error if not enough
name suggestions were available.

If you don't like the current syntax then it could be changed in a way
which also make my idea easier to implement, like

generalize
p : tt ≡ _{x y z}

Here we give name suggestions to generalized metas and at the same time
one can notice that it is not like an ordinary meta. A bit less clean
though.

Post by Nils Anders Danielsson
What does the following code expand to?
[...]

The first one.

This means that meta-variables do not have their usual meaning under
generalize. Perhaps it would be better to use a different notation for
the magic meta-variables.

Post by Peter Divianszky
{x = x₁ : ⊤} (p₁ : tt ≡ x₁) → p₁ ≡ p₁
[...]
{x : ⊤} (p : tt ≡ x) → p ≡ p

These two types are definitionally equal.

One property I did not bring up was that of stability. I hope that we
will not end up in a situation in which one can break lots of code by,
say, adding one variable name to a generalize block.

Nils Anders Danielsson

2018-03-31 09:58:01 UTC

Post by Peter Divianszky
{x = x₁ : ⊤} (p₁ : tt ≡ x₁) → p₁ ≡ p₁
[...]
{x : ⊤} (p : tt ≡ x) → p ≡ p

These two types are definitionally equal.

Right, I just wanted to be precise with naming.
The former is the current type signature and the latter is the desired one.

There is no difference between these type signatures, even if you take
the names of implicit arguments into account. Agda sometimes prints type
signatures using the {x = y : A} notation in order to avoid issues
related to shadowing. Here is one example:

F : (Set → Set) → Set₁
F G = {A : Set} → G A

T : Set₁
T = {A : Set} → F (λ X → A → X)

How should the normal form of T be printed? Agda prints

{A : Set} {A = A₁ : Set} → A → A₁.

Note that this notation is not parsed by Agda.

My idea would be stable in this sense.
For example,
postulate
ass : (σ ∘ δ) ∘ ν ≡ σ ∘ (δ ∘ ν)
means
postulate
ass : ∀{Γ Δ Σ Ω}{σ : Sub Σ Ω}{δ : Sub Δ Σ}{ν : Sub Γ Δ}
→ ((σ ∘ δ) ∘ ν) ≡ (σ ∘ (δ ∘ ν))

This suggested to me that if I replaced

{Γ Δ Θ} : Con

with

{Γ whatever Δ Θ} : Con,

then the type signature would change. However, I see now that your
example uses the names Σ and Ω which are not listed in any generalize
block. I tried your example myself, and this is what you actually end up
with:

{Γ = Γ₁ : Con} {Δ = Δ₁ : Con} {Γ = Γ₂ : Con} {Γ = Γ₃ : Con}
{σ = σ₁ : Sub Γ₁ Δ₁} {δ = δ₁ : Sub Γ₂ Γ₁} {ν = ν₁ : Sub Γ₃ Γ₂} →
((σ₁ ∘ δ₁) ∘ ν₁) ≡ (σ₁ ∘ (δ₁ ∘ ν₁))

The telescope contains /three/ implicit arguments all named Γ.

(I'm not sure why the {x = y : A} notation is used for all the other
implicit arguments. My guess would be that it has something to do with
the implementation of generalize.)

If you perform the change that I mentioned above, then you still end up
with the type signature above. Thus the type signature is stable under
this particular kind of change.

After some experimentation I managed to figure out where the names in
the type signature come from. If I replace

Sub : (Γ Δ : Con) → Set

with

Sub : (Γ Σ : Con) → Set,

then I get a different type signature:

{Γ = Γ₁ : Con} {Σ : Con} {Γ = Γ₂ : Con} {Γ = Γ₃ : Con}
{σ = σ₁ : Sub Γ₁ Σ} {δ = δ₁ : Sub Γ₂ Γ₁} {ν = ν₁ : Sub Γ₃ Γ₂} →
((σ₁ ∘ δ₁) ∘ ν₁) ≡ (σ₁ ∘ (δ₁ ∘ ν₁))

I still don't quite understand why you get one occurrence of Σ but three
occurrences of Γ. Does it depend on arbitrary choices made by the
unifier?

Furthermore I'm not sure that it's a good idea to use names subject to
α-conversion (like Π-bound names) in a setting in which α-conversion is
not applicable (like in implicit Π binders).

I tried to figure out what would happen if one of the bound names in the
type signature of Sub shadowed another name by parametrising the
module:

module _ {Σ : Set} where

However, this triggered some kind of error:

meta var MetaId 48 was generalized
CallStack (from HasCallStack):
error, called at src/full/Agda/TypeChecking/Rules/Term.hs:1580:86 in [...]

--
/NAD

Arseniy Alekseyev

2018-03-31 12:19:59 UTC

It's possible that I'm missing a key distinction, but this `generalize`
keyword sounds like it's exactly the same as `variable` keyword in lean.

These two pages give some (very simple) description:
https://leanprover.github.io/reference/other_commands.html
https://leanprover.github.io/theorem_proving_in_lean/dependent_type_theory.html#variables-and-sections

I don't know where to find a more in-depth explanation of how this works.

{x = xâ : â€} (pâ : tt â¡ xâ) â pâ â¡ pâ
[...]
{x : â€} (p : tt â¡ x) â p â¡ p

These two types are definitionally equal.

Right, I just wanted to be precise with naming.
The former is the current type signature and the latter is the desired one.

There is no difference between these type signatures, even if you take
the names of implicit arguments into account. Agda sometimes prints type
signatures using the {x = y : A} notation in order to avoid issues
F : (Set â Set) â Setâ
F G = {A : Set} â G A
T : Setâ
T = {A : Set} â F (Î» X â A â X)
How should the normal form of T be printed? Agda prints
{A : Set} {A = Aâ : Set} â A â Aâ.
Note that this notation is not parsed by Agda.

Post by Peter Divianszky
One property I did not bring up was that of stability. I hope that we

Post by Nils Anders Danielsson
will not end up in a situation in which one can break lots of code by,
say, adding one variable name to a generalize block.

My idea would be stable in this sense.

For example,

Post by Peter Divianszky
postulate
ass : (Ï â ÎŽ) â Îœ â¡ Ï â (ÎŽ â Îœ)
means
postulate
ass : â{Î Î Î£ Î©}{Ï : Sub Î£ Î©}{ÎŽ : Sub Î Î£}{Îœ : Sub Î Î}
â ((Ï â ÎŽ) â Îœ) â¡ (Ï â (ÎŽ â Îœ))

This suggested to me that if I replaced
{Î Î Î} : Con
with
{Î whatever Î Î} : Con,
then the type signature would change. However, I see now that your
example uses the names Î£ and Î© which are not listed in any generalize
block. I tried your example myself, and this is what you actually end up
{Î = Îâ : Con} {Î = Îâ : Con} {Î = Îâ : Con} {Î = Îâ : Con}
{Ï = Ïâ : Sub Îâ Îâ} {ÎŽ = ÎŽâ : Sub Îâ Îâ} {Îœ = Îœâ : Sub Îâ Îâ} â
((Ïâ â ÎŽâ) â Îœâ) â¡ (Ïâ â (ÎŽâ â Îœâ))
The telescope contains /three/ implicit arguments all named Î.
(I'm not sure why the {x = y : A} notation is used for all the other
implicit arguments. My guess would be that it has something to do with
the implementation of generalize.)
If you perform the change that I mentioned above, then you still end up
with the type signature above. Thus the type signature is stable under
this particular kind of change.
After some experimentation I managed to figure out where the names in
the type signature come from. If I replace
Sub : (Î Î : Con) â Set
with
Sub : (Î Î£ : Con) â Set,
{Î = Îâ : Con} {Î£ : Con} {Î = Îâ : Con} {Î = Îâ : Con}
{Ï = Ïâ : Sub Îâ Î£} {ÎŽ = ÎŽâ : Sub Îâ Îâ} {Îœ = Îœâ : Sub Îâ Îâ} â
((Ïâ â ÎŽâ) â Îœâ) â¡ (Ïâ â (ÎŽâ â Îœâ))
I still don't quite understand why you get one occurrence of Î£ but three
occurrences of Î. Does it depend on arbitrary choices made by the
unifier?
Furthermore I'm not sure that it's a good idea to use names subject to
Î±-conversion (like Î -bound names) in a setting in which Î±-conversion is
not applicable (like in implicit Î binders).
I tried to figure out what would happen if one of the bound names in the
type signature of Sub shadowed another name by parametrising the
module _ {Î£ : Set} where
meta var MetaId 48 was generalized
error, called at src/full/Agda/TypeChecking/Rules/Term.hs:1580:86 in [...]
--
/NAD
_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda

Peter Divianszky

2018-03-31 19:11:34 UTC

Arseniy, thanks for the pointers.

I checked them and indeed, 'generalize' and 'variable' in lean is quite
similar.
They both allow to specify the type of the generalizable variables.

I think 'generalize' is strictly more powerful, because you can use
holes inside the specified types like

generalize any : _ -- possible in Lean
-- this is idris-style generalization?

generalize A : Ty _ -- not possible/not documented in Lean

Post by Arseniy Alekseyev
It's possible that I'm missing a key distinction, but this `generalize`
keyword sounds like it's exactly the same as `variable` keyword in lean.
https://leanprover.github.io/reference/other_commands.html
https://leanprover.github.io/theorem_proving_in_lean/dependent_type_theory.html#variables-and-sections
I don't know where to find a more in-depth explanation of how this works.
>> {x = x₁ : ⊤} (p₁ : tt ≡ x₁) → p₁ ≡ p₁
>>
>> [...]
>>
>> {x : ⊤} (p : tt ≡ x) → p ≡ p
>
> These two types are definitionally equal.
Right, I just wanted to be precise with naming.
The former is the current type signature and the latter is the desired one.
There is no difference between these type signatures, even if you take
the names of implicit arguments into account. Agda sometimes prints type
signatures using the {x = y : A} notation in order to avoid issues
F : (Set → Set) → Set₁
F G = {A : Set} → G A
T : Set₁
T = {A : Set} → F (λ X → A → X)
How should the normal form of T be printed? Agda prints
{A : Set} {A = A₁ : Set} → A → A₁.
Note that this notation is not parsed by Agda.
> One property I did not bring up was that of stability. I
hope that we
> will not end up in a situation in which one can break lots
of code by,
> say, adding one variable name to a generalize block.
My idea would be stable in this sense.
For example,
postulate
ass : (σ ∘ δ) ∘ ν ≡ σ ∘ (δ ∘ ν)
means
postulate
ass : ∀{Γ Δ Σ Ω}{σ : Sub Σ Ω}{δ : Sub Δ Σ}{ν : Sub Γ Δ}
→ ((σ ∘ δ) ∘ ν) ≡ (σ ∘ (δ ∘ ν))
This suggested to me that if I replaced
{Γ Δ Θ} : Con
with
{Γ whatever Δ Θ} : Con,
then the type signature would change. However, I see now that your
example uses the names Σ and Ω which are not listed in any generalize
block. I tried your example myself, and this is what you actually end up
{Γ = Γ₁ : Con} {Δ = Δ₁ : Con} {Γ = Γ₂ : Con} {Γ = Γ₃ : Con}
{σ = σ₁ : Sub Γ₁ Δ₁} {δ = δ₁ : Sub Γ₂ Γ₁} {ν = ν₁ : Sub Γ₃ Γ₂} →
((σ₁ ∘ δ₁) ∘ ν₁) ≡ (σ₁ ∘ (δ₁ ∘ ν₁))
The telescope contains /three/ implicit arguments all named Γ.
(I'm not sure why the {x = y : A} notation is used for all the other
implicit arguments. My guess would be that it has something to do with
the implementation of generalize.)
If you perform the change that I mentioned above, then you still end up
with the type signature above. Thus the type signature is stable under
this particular kind of change.
After some experimentation I managed to figure out where the names in
the type signature come from. If I replace
Sub : (Γ Δ : Con) → Set
with
Sub : (Γ Σ : Con) → Set,
{Γ = Γ₁ : Con} {Σ : Con} {Γ = Γ₂ : Con} {Γ = Γ₃ : Con}
{σ = σ₁ : Sub Γ₁ Σ} {δ = δ₁ : Sub Γ₂ Γ₁} {ν = ν₁ : Sub Γ₃ Γ₂} →
((σ₁ ∘ δ₁) ∘ ν₁) ≡ (σ₁ ∘ (δ₁ ∘ ν₁))
I still don't quite understand why you get one occurrence of Σ but three
occurrences of Γ. Does it depend on arbitrary choices made by the
unifier?
Furthermore I'm not sure that it's a good idea to use names subject to
α-conversion (like Π-bound names) in a setting in which α-conversion is
not applicable (like in implicit Π binders).
I tried to figure out what would happen if one of the bound names in the
type signature of Sub shadowed another name by parametrising the
module _ {Σ : Set} where
meta var MetaId 48 was generalized
error, called at
src/full/Agda/TypeChecking/Rules/Term.hs:1580:86 in [...]
--
/NAD
_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda
<https://lists.chalmers.se/mailman/listinfo/agda>

Peter Divianszky

2018-03-31 23:20:30 UTC

Post by Peter Divianszky
{x = x₁ : ⊤} (p₁ : tt ≡ x₁) → p₁ ≡ p₁
[...]
{x : ⊤} (p : tt ≡ x) → p ≡ p

These two types are definitionally equal.

Right, I just wanted to be precise with naming.
The former is the current type signature and the latter is the desired one.

There is no difference between these type signatures, even if you take
the names of implicit arguments into account. [...]

Ok, I saw how

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

is equal to

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

but I missed that this is further equal to

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

because the second argument is not hidden.

Post by Peter Divianszky
postulate
ass : (σ ∘ δ) ∘ ν ≡ σ ∘ (δ ∘ ν)
[...]

[...] and this is what you actually end up
{Γ = Γ₁ : Con} {Δ = Δ₁ : Con} {Γ = Γ₂ : Con} {Γ = Γ₃ : Con}
{σ = σ₁ : Sub Γ₁ Δ₁} {δ = δ₁ : Sub Γ₂ Γ₁} {ν = ν₁ : Sub Γ₃ Γ₂} →
((σ₁ ∘ δ₁) ∘ ν₁) ≡ (σ₁ ∘ (δ₁ ∘ ν₁))
The telescope contains /three/ implicit arguments all named Γ.

The naming of arguments is not yet fully implemented, only the ordering.

I just implemented another simplified naming which is stable too.
The result is:

{σ.Γ σ.Δ δ.Γ ν.Γ : Con}
{σ = σ₁ : Sub σ.Γ σ.Δ}
{δ = δ₁ : Sub δ.Γ σ.Γ}
{ν = ν₁ : Sub ν.Γ δ.Γ} →
(σ₁ ∘ δ₁) ∘ ν₁ ≡ σ₁ ∘ (δ₁ ∘ ν₁)

if

Sub : (Γ Δ : Con) → Set

otherwise, if

Sub : Con → Con → Set

then it becomes

{σ.1 σ.2 δ.1 ν.1 : Con}
{σ = σ₁ : Sub σ.1 σ.2}
{δ = δ₁ : Sub δ.1 σ.1}
{ν = ν₁ : Sub ν.1 δ.1} →
(σ₁ ∘ δ₁) ∘ ν₁ ≡ σ₁ ∘ (δ₁ ∘ ν₁)

Post by Nils Anders Danielsson
I still don't quite understand why you get one occurrence of Σ but three
occurrences of Γ. Does it depend on arbitrary choices made by the
unifier?

It depends on the unifier, but not arbitrarily. Metavariables of
generalized variables defined earlier wins.

Post by Nils Anders Danielsson
Furthermore I'm not sure that it's a good idea to use names subject to
α-conversion (like Π-bound names) in a setting in which α-conversion is
not applicable (like in implicit Π binders).

I'm also not sure.
It is nice though that the naming of automatic implicit parameters can
be influenced be existing syntactic constructs.

Post by Nils Anders Danielsson
I tried to figure out what would happen if one of the bound names in the
type signature of Sub shadowed another name by parametrising the
module _ {Σ : Set} where
meta var MetaId 48 was generalized
error, called at src/full/Agda/TypeChecking/Rules/Term.hs:1580:86 in [...]

This bug is fixed now.

Post by Peter Divianszky
>> {x = x₁ : ⊤} (p₁ : tt ≡ x₁) → p₁ ≡ p₁
>>
>> [...]
>>
>> {x : ⊤} (p : tt ≡ x) → p ≡ p
>
> These two types are definitionally equal.
Right, I just wanted to be precise with naming.
The former is the current type signature and the latter is the desired one.

There is no difference between these type signatures, even if you take
the names of implicit arguments into account. Agda sometimes prints type
signatures using the {x = y : A} notation in order to avoid issues
F : (Set → Set) → Set₁
F G = {A : Set} → G A
T : Set₁
T = {A : Set} → F (λ X → A → X)
How should the normal form of T be printed? Agda prints
{A : Set} {A = A₁ : Set} → A → A₁.
Note that this notation is not parsed by Agda.

Post by Peter Divianszky
> One property I did not bring up was that of stability. I hope that we
> will not end up in a situation in which one can break lots of code by,
> say, adding one variable name to a generalize block.
My idea would be stable in this sense.
For example,
postulate
   ass : (σ ∘ δ) ∘ ν ≡ σ ∘ (δ ∘ ν)
means
postulate
   ass   : ∀{Γ Δ Σ Ω}{σ : Sub Σ Ω}{δ : Sub Δ Σ}{ν : Sub Γ Δ}
         → ((σ ∘ δ) ∘ ν) ≡ (σ ∘ (δ ∘ ν))

This suggested to me that if I replaced
{Γ Δ Θ} : Con
with
{Γ whatever Δ Θ} : Con,
then the type signature would change. However, I see now that your
example uses the names Σ and Ω which are not listed in any generalize
block. I tried your example myself, and this is what you actually end up
{Γ = Γ₁ : Con} {Δ = Δ₁ : Con} {Γ = Γ₂ : Con} {Γ = Γ₃ : Con}
{σ = σ₁ : Sub Γ₁ Δ₁} {δ = δ₁ : Sub Γ₂ Γ₁} {ν = ν₁ : Sub Γ₃ Γ₂} →
((σ₁ ∘ δ₁) ∘ ν₁) ≡ (σ₁ ∘ (δ₁ ∘ ν₁))
The telescope contains /three/ implicit arguments all named Γ.
(I'm not sure why the {x = y : A} notation is used for all the other
implicit arguments. My guess would be that it has something to do with
the implementation of generalize.)
If you perform the change that I mentioned above, then you still end up
with the type signature above. Thus the type signature is stable under
this particular kind of change.
After some experimentation I managed to figure out where the names in
the type signature come from. If I replace
Sub : (Γ Δ : Con) → Set
with
Sub : (Γ Σ : Con) → Set,
{Γ = Γ₁ : Con} {Σ : Con} {Γ = Γ₂ : Con} {Γ = Γ₃ : Con}
{σ = σ₁ : Sub Γ₁ Σ} {δ = δ₁ : Sub Γ₂ Γ₁} {ν = ν₁ : Sub Γ₃ Γ₂} →
((σ₁ ∘ δ₁) ∘ ν₁) ≡ (σ₁ ∘ (δ₁ ∘ ν₁))
I still don't quite understand why you get one occurrence of Σ but three
occurrences of Γ. Does it depend on arbitrary choices made by the
unifier?
Furthermore I'm not sure that it's a good idea to use names subject to
α-conversion (like Π-bound names) in a setting in which α-conversion is
not applicable (like in implicit Π binders).
I tried to figure out what would happen if one of the bound names in the
type signature of Sub shadowed another name by parametrising the
module _ {Σ : Set} where
meta var MetaId 48 was generalized
error, called at src/full/Agda/TypeChecking/Rules/Term.hs:1580:86
in [...]

Nils Anders Danielsson

2018-04-01 08:35:33 UTC

Post by Peter Divianszky
I just implemented another simplified naming which is stable too.
{σ.Γ σ.Δ δ.Γ ν.Γ : Con}
{σ.1 σ.2 δ.1 ν.1 : Con}

These naming schemes have the advantage that one cannot give the
arguments by name, so the names do not matter, but the type signatures
are still readable.

If one of these arguments needs to be given explicitly, then one can
give it by position. However, this is rather clunky (f {_} {_} {_} {x}),
and could lead to brittle code.

--
/NAD

Peter Divianszky

2018-03-30 21:46:01 UTC

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

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

Post by Peter Divianszky
> 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
>
>    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.
>
>
>    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
* 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.

Post by Peter Divianszky
I am not familiar with sections, can you point to a documentation?

https://coq.inria.fr/refman/gallina-ext.html#Section

Joachim Breitner

2018-03-30 14:24:04 UTC

Hi,

Post by Peter Divianszky
- What should be the keyword?

The variant that I have described is similar to sections in Coq. Perhaps
section {Î : Ctxt} âŠ where
This is similar to "module _ <telescope> where", but with the "drop
unused bindings" semantics.

a question from the sidelines: There seems to be a crucial difference
to Coqâs section feature, if I am not mistaken: In Coq, you write

Section Foo.
Context {x : nat}.
Definition bar := x + 1.
Definition baz := bar + 2.
End Foo.
Definition foo := bar 1 + 2.

So within the section, x is not generalized, and bar has type nat, but
outside the section, bar has type (nat -> nat).

This forbids calling bar within the Section with a different parameter:

Section Foo.
Context {x : nat}.
Definition bar := x + 1.
Definition baz := bar 2. (* type error *)
End Foo.

If I read Peterâs description of his `generalize` feature correctly,
then this generalizes the variables _in each type signature_, and you
can call bar from baz with different arguments for the generalized
parameter.

If I read this correctly, then it would maybe more confusing than
helpful to call it section.

Cheers,
Joachim

--
Joachim Breitner
***@joachim-breitner.de
http://www.joachim-breitner.de/

Jannis Limperg

2018-03-30 15:17:39 UTC

Agda's unnamed modules are closer to Coq's sections than this new
feature, working pretty much exactly like Joachim describes. Hence, I
would also find 'sections' confusing.

For the same reason, I don't like 'notation' too much, since it invokes
Coq's notation feature, which is Agda's 'syntax' on steroids. Of course,
it is not exactly an absolute imperative that Agda stay consistent with
Coq's usage of these terms, but it's something to consider.

Peter's new feature, if I understand it correctly, is closest to Coq's
implicit generalization [1, Section 2.7.19] (which is frequently handy,
so add my voice to the choir of fans of this feature.) To summarise
Coq's design:

- You can declare variable names as generalizable using `Generalizable
Variables x y z` or `Generalizable All Variables`. This roughly
corresponds to Peter's `generalize` declaration.
- Contrary to Peter's design, generalization only takes effect if the
generalizable variables are mentioned in a special binder that enables
generalization, of the form `(P : n = n) or `{P : n = n} (the backtick
is part of the binder). Given the above binders, n would be generalized
if it was previously declared generalizable. I have no strong opinion on
requiring this additional step; perhaps one could ask on Coq-Club why
the Coq implementors chose to do so.

An example:

Generalizable Variables A.

Definition id `(x : A) : A := x.

About id.

(* id : forall A : Type, A -> A

Argument A is implicit and maximally inserted [...] *)

[1] https://coq.inria.fr/refman/gallina-ext.html#Implicit%20Arguments

Nils Anders Danielsson

2018-03-30 16:36:59 UTC

If I read Peter’s description of his `generalize` feature correctly,
then this generalizes the variables _in each type signature_, and you
can call bar from baz with different arguments for the generalized
parameter.
If I read this correctly, then it would maybe more confusing than
helpful to call it section.

That's a good point.

--
/NAD

Martin Escardo

2018-03-29 16:47:20 UTC

I like this, Peter! It should simplify a lot of my code. M.

Post by Peter Divianszky
Dear Agda users and implementors,
I implemented a first version of forall-generalization, and I would like
to get feedback on it.
For users
---------
An example Agda file can be found at
https://github.com/divipp/agda/blob/master/test/Succeed/Generalize.agda
postulate
Con :                       Set
Ty : (Γ : Con) →           Set
Sub : (Γ Δ : Con) →         Set
Tm : (Γ : Con)(A : Ty Γ) → Set
There is a new keyword 'generalize', which accept declarations like
generalize
{Γ Δ Θ} : Con
{A B C} : Ty _
{σ δ ν} : Sub _ _
{t u v} : Tm _ _
After these 12 declarations
(1) Γ, Δ and Θ behave as Con-typed terms, but they are automatically
forall-generalized, so, for example
postulate
id : Sub Γ Γ
_∘_ : Sub Θ Δ → Sub Γ Θ → Sub Γ Δ
means
postulate
id : ∀ {Γ} → Sub Γ Γ
_∘_ : ∀ {Γ Δ Θ} → Sub Θ Δ → Sub Γ Θ → Sub Γ Δ
(2) A, B and C behaves as (Ty _)-typed terms (their types contain a
dedicated metavariable for each of them),
and they are also automatically forall-generalized.
For example,
postulate
_▹_ : ∀ Γ → Ty Γ → Con
π₁ : Sub Γ (Δ ▹ A) → Sub Γ Δ
means
_▹_ : ∀ Γ → Ty Γ → Con
π₁ : ∀{Γ Δ}{A : Ty Δ} → Sub Γ (Δ ▹ A) → Sub Γ Δ
(3) The metavariables of generalizable variables are also automatically
generalized.
For example,
postulate
ass : (σ ∘ δ) ∘ ν ≡ σ ∘ (δ ∘ ν)
means
postulate
ass   : ∀{Γ Δ Σ Ω}{σ : Sub Σ Ω}{δ : Sub Δ Σ}{ν : Sub Γ Δ}
        → ((σ ∘ δ) ∘ ν) ≡ (σ ∘ (δ ∘ ν))
(4) The place and order of generalized variables are fixed by the
A) generalized bindings are placed at the front of the type signature
B) the dependencies between the generalized variables are always respected
C) whenever possible, introduce A before B if A < B
- for non-metas, A < B if A was declared before B with a 'generalize'
keyword
- a meta is smaller than a non-meta
- for metas, A < B if A was declared before B with a 'generalize'
keyword. For example, σ : Sub _1 _2 was declared before δ : Sub _3 _4 so
instances of _1, _2, _3, _4 are ordered according to the indices.
----
- make type signatures shorter
- the type schema of generalizable variables helps
    to make even more guesses by the type system
- avoid accidental generalization
- only the given names are generalized
- the type of generalizable variables are checked
    against the given schema, which adds extra safety
- make generalized type signatures reliable
(the ordering, and also the naming, see later)
- What should be the keyword?
'notation' seems also good for me.
The idea behind 'notation' is that this language construct
makes informal sentences like "Let Γ Δ Θ denote contexts." formal.
Plans (not implemented yet)
- automatic generalization of record fields and constructor types
- allow 'generalize' keyword in submodules and between record fields
- make generalizable variables importable?
- 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.
https://github.com/divipp/agda
For Agda implementors
---------------------
The main patch is
https://github.com/divipp/agda/commit/d172d1ade15abe26be19311300f7d640563a6a57
- metavariables of generalizable variables are solved locally during
typechecking of terms and reverted later
- generalizable variables are stored in the signature as if they were
introduced by 'postulate'
The Generalize.agda file succeeds when I load it into emacs, but fails
if I call Agda directly. Somehow I could not filter out metavariables
introduced by 'generalize', so Agda tries to serialize them.
It would great if you could help me to let this feature in.
Best Regards,
Peter
_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda

--
Martin Escardo
http://www.cs.bham.ac.uk/~mhe

Thorsten Altenkirch

2018-03-29 17:24:16 UTC

I like it too. Also one wouldn't need to doctor agda code anymore to make it publishable (destroying the literate idea in the process).

Thorsten

On 29/03/2018, 17:47, "Agda on behalf of Martin Escardo" <agda-***@lists.chalmers.se on behalf of ***@cs.bham.ac.uk> wrote:

I like this, Peter! It should simplify a lot of my code. M.

Post by Peter Divianszky
Dear Agda users and implementors,
I implemented a first version of forall-generalization, and I would like
to get feedback on it.
For users
---------
An example Agda file can be found at
https://github.com/divipp/agda/blob/master/test/Succeed/Generalize.agda
postulate
Con : Set
Ty : (Γ : Con) → Set
Sub : (Γ Δ : Con) → Set
Tm : (Γ : Con)(A : Ty Γ) → Set
There is a new keyword 'generalize', which accept declarations like
generalize
{Γ Δ Θ} : Con
{A B C} : Ty _
{σ δ ν} : Sub _ _
{t u v} : Tm _ _
After these 12 declarations
(1) Γ, Δ and Θ behave as Con-typed terms, but they are automatically
forall-generalized, so, for example
postulate
id : Sub Γ Γ
_∘_ : Sub Θ Δ → Sub Γ Θ → Sub Γ Δ
means
postulate
id : ∀ {Γ} → Sub Γ Γ
_∘_ : ∀ {Γ Δ Θ} → Sub Θ Δ → Sub Γ Θ → Sub Γ Δ
(2) A, B and C behaves as (Ty _)-typed terms (their types contain a
dedicated metavariable for each of them),
and they are also automatically forall-generalized.
For example,
postulate
_▹_ : ∀ Γ → Ty Γ → Con
π₁ : Sub Γ (Δ ▹ A) → Sub Γ Δ
means
_▹_ : ∀ Γ → Ty Γ → Con
π₁ : ∀{Γ Δ}{A : Ty Δ} → Sub Γ (Δ ▹ A) → Sub Γ Δ
(3) The metavariables of generalizable variables are also automatically
generalized.
For example,
postulate
ass : (σ ∘ δ) ∘ ν ≡ σ ∘ (δ ∘ ν)
means
postulate
ass : ∀{Γ Δ Σ Ω}{σ : Sub Σ Ω}{δ : Sub Δ Σ}{ν : Sub Γ Δ}
→ ((σ ∘ δ) ∘ ν) ≡ (σ ∘ (δ ∘ ν))
(4) The place and order of generalized variables are fixed by the
A) generalized bindings are placed at the front of the type signature
B) the dependencies between the generalized variables are always respected
C) whenever possible, introduce A before B if A < B
- for non-metas, A < B if A was declared before B with a 'generalize'
keyword
- a meta is smaller than a non-meta
- for metas, A < B if A was declared before B with a 'generalize'
keyword. For example, σ : Sub _1 _2 was declared before δ : Sub _3 _4 so
instances of _1, _2, _3, _4 are ordered according to the indices.
----
- make type signatures shorter
- the type schema of generalizable variables helps
to make even more guesses by the type system
- avoid accidental generalization
- only the given names are generalized
- the type of generalizable variables are checked
against the given schema, which adds extra safety
- make generalized type signatures reliable
(the ordering, and also the naming, see later)
- What should be the keyword?
'notation' seems also good for me.
The idea behind 'notation' is that this language construct
makes informal sentences like "Let Γ Δ Θ denote contexts." formal.
Plans (not implemented yet)
- automatic generalization of record fields and constructor types
- allow 'generalize' keyword in submodules and between record fields
- make generalizable variables importable?
- 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.
https://github.com/divipp/agda
For Agda implementors
---------------------
The main patch is
https://github.com/divipp/agda/commit/d172d1ade15abe26be19311300f7d640563a6a57
- metavariables of generalizable variables are solved locally during
typechecking of terms and reverted later
- generalizable variables are stored in the signature as if they were
introduced by 'postulate'
The Generalize.agda file succeeds when I load it into emacs, but fails
if I call Agda directly. Somehow I could not filter out metavariables
introduced by 'generalize', so Agda tries to serialize them.
It would great if you could help me to let this feature in.
Best Regards,
Peter
_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda

--
Martin Escardo
http://www.cs.bham.ac.uk/~mhe
_______________________________________________
Agda mailing list
***@lists.chalmers.se
https://lists.chalmers.se/mailman/listinfo/agda

This message and any attachment are intended solely for the addressee
and may contain confidential information. If you have received this
message in error, please contact the sender and delete the email and
attachment.

Any views or opinions expressed by the author of this email do not
necessarily reflect the views of the University of Nottingham. Email
communications with the University of Nottingham may be monitored
where permitted by law.

Robby Findler

2018-03-29 17:39:14 UTC

On Thu, Mar 29, 2018 at 12:24 PM, Thorsten Altenkirch

Post by Thorsten Altenkirch
I like it too. Also one wouldn't need to doctor agda code anymore to make it publishable (destroying the literate idea in the process).

Yay! "Run your research" support in Agda! I love it.

More generally, while I'm a total newbie compared to most people here,
I really do love the design of Agda. It is so ... I don't have a good
word for it ... *human*. I love the idea that it gets features that
make it easier to show sensible and yet accurate code snippets in
papers.

Robby

Apostolis Xekoukoulotakis

2018-03-29 22:07:53 UTC

I agree with Nils points,

i think that it is better to return an error if you try to generalize a
name that already exists.

In idris, where every implicit argument is generalized, you get into
problems because of that.
You want your function to get a specific value, but instead it assumes that
it is an implicit argument.

http://docs.idris-lang.org/en/latest/tutorial/typesfuns.html#using-notation
(Check the "important section" there)

So, if it returns an error in such a case and since generalization are
local, this might work.

Post by Robby Findler
On Thu, Mar 29, 2018 at 12:24 PM, Thorsten Altenkirch

Post by Thorsten Altenkirch
I like it too. Also one wouldn't need to doctor agda code anymore to

make it publishable (destroying the literate idea in the process).
Yay! "Run your research" support in Agda! I love it.
More generally, while I'm a total newbie compared to most people here,
I really do love the design of Agda. It is so ... I don't have a good
word for it ... *human*. I love the idea that it gets features that
make it easier to show sensible and yet accurate code snippets in
papers.
Robby
_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda

Peter Divianszky

2018-03-30 08:34:04 UTC

It's great that you like this feature.

My motivation was that now I am working with Ambrus Kaposi on
type-theory-in-type-theory, and I have to formalize his work in Agda.

A little part of the basics, without and with forall-generalization (the
second covers more type formers):

https://bitbucket.org/akaposi/tt-in-tt/src/6f71db610e9d27147abcf743cbe1731ed5c9ca0a/TTR.agda?at=master&fileviewer=file-view-default

https://github.com/divipp/agda/blob/master/test/Succeed/Generalize.agda

If you look at the type of ,∘ for example, you will notice the difference.

By the way, I fixed an error in the implementation and now all Agda
tests are OK including the new one.

These tasks are also ready now:

- automatic generalization of record fields and constructor types
- allow 'generalize' keyword in submodules

Best,
Peter

Post by Robby Findler
On Thu, Mar 29, 2018 at 12:24 PM, Thorsten Altenkirch

Post by Thorsten Altenkirch
I like it too. Also one wouldn't need to doctor agda code anymore to make it publishable (destroying the literate idea in the process).

Yay! "Run your research" support in Agda! I love it.
More generally, while I'm a total newbie compared to most people here,
I really do love the design of Agda. It is so ... I don't have a good
word for it ... *human*. I love the idea that it gets features that
make it easier to show sensible and yet accurate code snippets in
papers.
Robby

Martin Stone Davis

2018-04-01 13:01:54 UTC

Peter, many accolades to you for developing and sharing. Now for the
complaints!

My trouble is shown in the code below, which is failing on the last
line. Is this a bug in the new feature?

```
{-# OPTIONS --generalize #-}

postulate
Class : Set -> Set
method : {X : Set} {{_ : Class X}} -> X -> Set
Nat : Set
Fin : Nat -> Set

generalize
{n} : Nat
{x} : Fin _

postulate
instance ClassFin : Class (Fin n)
works1 : {x : Fin n} -> method x
works2 : method {{ClassFin}} x
works3 : method {X = Fin n} x
fails : method x
{-
Unsolved meta not generalized
when checking that the expression method x has type Set _22
-}
```

Post by Peter Divianszky
Dear Agda users and implementors,
I implemented a first version of forall-generalization, and I would
like to get feedback on it.
For users
---------
An example Agda file can be found at
https://github.com/divipp/agda/blob/master/test/Succeed/Generalize.agda
postulate
Con :                       Set
Ty : (Γ : Con) →           Set
Sub : (Γ Δ : Con) →         Set
Tm : (Γ : Con)(A : Ty Γ) → Set
There is a new keyword 'generalize', which accept declarations like
generalize
{Γ Δ Θ} : Con
{A B C} : Ty _
{σ δ ν} : Sub _ _
{t u v} : Tm _ _
After these 12 declarations
(1) Γ, Δ and Θ behave as Con-typed terms, but they are automatically
forall-generalized, so, for example
postulate
id : Sub Γ Γ
_∘_ : Sub Θ Δ → Sub Γ Θ → Sub Γ Δ
means
postulate
id : ∀ {Γ} → Sub Γ Γ
_∘_ : ∀ {Γ Δ Θ} → Sub Θ Δ → Sub Γ Θ → Sub Γ Δ
(2) A, B and C behaves as (Ty _)-typed terms (their types contain a
dedicated metavariable for each of them),
and they are also automatically forall-generalized.
For example,
postulate
_▹_ : ∀ Γ → Ty Γ → Con
π₁ : Sub Γ (Δ ▹ A) → Sub Γ Δ
means
_▹_ : ∀ Γ → Ty Γ → Con
π₁ : ∀{Γ Δ}{A : Ty Δ} → Sub Γ (Δ ▹ A) → Sub Γ Δ
(3) The metavariables of generalizable variables are also
automatically generalized.
For example,
postulate
ass : (σ ∘ δ) ∘ ν ≡ σ ∘ (δ ∘ ν)
means
postulate
ass   : ∀{Γ Δ Σ Ω}{σ : Sub Σ Ω}{δ : Sub Δ Σ}{ν : Sub Γ Δ}
        → ((σ ∘ δ) ∘ ν) ≡ (σ ∘ (δ ∘ ν))
(4) The place and order of generalized variables are fixed by the
A) generalized bindings are placed at the front of the type signature
B) the dependencies between the generalized variables are always respected
C) whenever possible, introduce A before B if A < B
- for non-metas, A < B if A was declared before B with a 'generalize'
keyword
- a meta is smaller than a non-meta
- for metas, A < B if A was declared before B with a 'generalize'
keyword. For example, σ : Sub _1 _2 was declared before δ : Sub _3 _4 so
instances of _1, _2, _3, _4 are ordered according to the indices.
----
- make type signatures shorter
- the type schema of generalizable variables helps
    to make even more guesses by the type system
- avoid accidental generalization
- only the given names are generalized
- the type of generalizable variables are checked
    against the given schema, which adds extra safety
- make generalized type signatures reliable
(the ordering, and also the naming, see later)
- What should be the keyword?
'notation' seems also good for me.
The idea behind 'notation' is that this language construct
makes informal sentences like "Let Γ Δ Θ denote contexts." formal.
Plans (not implemented yet)
- automatic generalization of record fields and constructor types
- allow 'generalize' keyword in submodules and between record fields
- make generalizable variables importable?
- 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.
https://github.com/divipp/agda
For Agda implementors
---------------------
The main patch is
https://github.com/divipp/agda/commit/d172d1ade15abe26be19311300f7d640563a6a57
- metavariables of generalizable variables are solved locally during
typechecking of terms and reverted later
- generalizable variables are stored in the signature as if they were
introduced by 'postulate'
The Generalize.agda file succeeds when I load it into emacs, but fails
if I call Agda directly. Somehow I could not filter out metavariables
introduced by 'generalize', so Agda tries to serialize them.
It would great if you could help me to let this feature in.
Best Regards,
Peter
_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda

Peter Divianszky

2018-04-01 18:02:14 UTC

Martin, thanks for testing and for the test case.

This is a bug. I'll try to fix this.
(The fix should be that the generalized type should be build up from
outside to inside, adding outer bindings first. Currently it is done in
the other way around, so metavariables are solved before the
generalization begins, but not solved during the generalization.)

Post by Martin Stone Davis
Peter, many accolades to you for developing and sharing. Now for the
complaints!
My trouble is shown in the code below, which is failing on the last
line. Is this a bug in the new feature?
```
{-# OPTIONS --generalize #-}
postulate
Class : Set -> Set
method : {X : Set} {{_ : Class X}} -> X -> Set
Nat : Set
Fin : Nat -> Set
generalize
{n} : Nat
{x} : Fin _
postulate
instance ClassFin : Class (Fin n)
works1 : {x : Fin n} -> method x
works2 : method {{ClassFin}} x
works3 : method {X = Fin n} x
fails : method x
{-
Unsolved meta not generalized
when checking that the expression method x has type Set _22
-}
```

Post by Peter Divianszky
Dear Agda users and implementors,
I implemented a first version of forall-generalization, and I would
like to get feedback on it.
For users
---------
An example Agda file can be found at
https://github.com/divipp/agda/blob/master/test/Succeed/Generalize.agda
postulate
Con :                       Set
Ty : (Γ : Con) →           Set
Sub : (Γ Δ : Con) →         Set
Tm : (Γ : Con)(A : Ty Γ) → Set
There is a new keyword 'generalize', which accept declarations like
generalize
{Γ Δ Θ} : Con
{A B C} : Ty _
{σ δ ν} : Sub _ _
{t u v} : Tm _ _
After these 12 declarations
(1) Γ, Δ and Θ behave as Con-typed terms, but they are automatically
forall-generalized, so, for example
postulate
id : Sub Γ Γ
_∘_ : Sub Θ Δ → Sub Γ Θ → Sub Γ Δ
means
postulate
id : ∀ {Γ} → Sub Γ Γ
_∘_ : ∀ {Γ Δ Θ} → Sub Θ Δ → Sub Γ Θ → Sub Γ Δ
(2) A, B and C behaves as (Ty _)-typed terms (their types contain a
dedicated metavariable for each of them),
and they are also automatically forall-generalized.
For example,
postulate
_▹_ : ∀ Γ → Ty Γ → Con
π₁ : Sub Γ (Δ ▹ A) → Sub Γ Δ
means
_▹_ : ∀ Γ → Ty Γ → Con
π₁ : ∀{Γ Δ}{A : Ty Δ} → Sub Γ (Δ ▹ A) → Sub Γ Δ
(3) The metavariables of generalizable variables are also
automatically generalized.
For example,
postulate
ass : (σ ∘ δ) ∘ ν ≡ σ ∘ (δ ∘ ν)
means
postulate
ass   : ∀{Γ Δ Σ Ω}{σ : Sub Σ Ω}{δ : Sub Δ Σ}{ν : Sub Γ Δ}
        → ((σ ∘ δ) ∘ ν) ≡ (σ ∘ (δ ∘ ν))
(4) The place and order of generalized variables are fixed by the
A) generalized bindings are placed at the front of the type signature
B) the dependencies between the generalized variables are always respected
C) whenever possible, introduce A before B if A < B
- for non-metas, A < B if A was declared before B with a 'generalize'
keyword
- a meta is smaller than a non-meta
- for metas, A < B if A was declared before B with a 'generalize'
keyword. For example, σ : Sub _1 _2 was declared before δ : Sub _3 _4 so
instances of _1, _2, _3, _4 are ordered according to the indices.
----
- make type signatures shorter
- the type schema of generalizable variables helps
    to make even more guesses by the type system
- avoid accidental generalization
- only the given names are generalized
- the type of generalizable variables are checked
    against the given schema, which adds extra safety
- make generalized type signatures reliable
(the ordering, and also the naming, see later)
- What should be the keyword?
'notation' seems also good for me.
The idea behind 'notation' is that this language construct
makes informal sentences like "Let Γ Δ Θ denote contexts." formal.
Plans (not implemented yet)
- automatic generalization of record fields and constructor types
- allow 'generalize' keyword in submodules and between record fields
- make generalizable variables importable?
- 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.
https://github.com/divipp/agda
For Agda implementors
---------------------
The main patch is
https://github.com/divipp/agda/commit/d172d1ade15abe26be19311300f7d640563a6a57
- metavariables of generalizable variables are solved locally during
typechecking of terms and reverted later
- generalizable variables are stored in the signature as if they were
introduced by 'postulate'
The Generalize.agda file succeeds when I load it into emacs, but fails
if I call Agda directly. Somehow I could not filter out metavariables
introduced by 'generalize', so Agda tries to serialize them.
It would great if you could help me to let this feature in.
Best Regards,
Peter
_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda

_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda

Andrés Sicard-Ramírez

2018-04-01 15:18:38 UTC

It seems that Coq also has a forall-generalisation mechanism (which
I'm not familiarised).

(* Tested with Coq 8.7.1. *)

Require Import Unicode.Utf8.

Axiom Con : Set.
Axiom Sub : Con → Con → Set.

Generalizable All Variables.
Axiom id : `{Sub Γ Γ}.
Axiom comp : `{Sub Θ Δ → Sub Γ Θ → Sub Γ Δ}.

See Section 2.7.19 of
https://github.com/coq/coq/releases/download/V8.7.2/coq-8.7.2-reference-manual.pdf
(because Coq website ( https://coq.inria.fr/ ) seems down).

--
Andrés

Peter Divianszky

2018-04-01 18:04:24 UTC

Andrés, thanks for the pointers.

Yes, it seems that Coq also has a forall-generalisation.
The main difference is that it is not possible to specify the types of
the variables to be generalized.

It seems that Coq also has a forall-generalisation mechanism (which
I'm not familiarised).
(* Tested with Coq 8.7.1. *)
Require Import Unicode.Utf8.
Axiom Con : Set.
Axiom Sub : Con → Con → Set.
Generalizable All Variables.
Axiom id : `{Sub Γ Γ}.
Axiom comp : `{Sub Θ Δ → Sub Γ Θ → Sub Γ Δ}.
See Section 2.7.19 of
https://github.com/coq/coq/releases/download/V8.7.2/coq-8.7.2-reference-manual.pdf
(because Coq website ( https://coq.inria.fr/ ) seems down).

Nils Anders Danielsson

2018-04-01 19:38:28 UTC

Yes, it seems that Coq also has a forall-generalisation. The main
difference is that it is not possible to specify the types of the
variables to be generalized.

Correct me if I'm wrong, but I don't think Coq has a first-class
implicit function space like Agda does. (This function space has led to
a number of problems.)

--
/NAD

Martin Stone Davis

2018-04-02 01:01:36 UTC

Respect the privacy of --generalize'd identifiers!

```
{-# OPTIONS --generalize #-}

postulate
Nat : Set
Fin : Nat → Set

module _ where

private
    generalize
      n : Nat
{-
    Using private here has no effect. Private applies only to
    declarations that introduce new identifiers into the module, like
    type signatures and data, record, and module declarations.
    when scope checking the declaration
      module _ where
-}

postulate foo : Fin n

postulate n : Nat
{-
Multiple definitions of n. Previous definition at
[snip]
when scope checking the declaration
n : Nat
-}
```

Post by Peter Divianszky
Dear Agda users and implementors,
I implemented a first version of forall-generalization, and I would
like to get feedback on it.
For users
---------
An example Agda file can be found at
https://github.com/divipp/agda/blob/master/test/Succeed/Generalize.agda
postulate
Con :                       Set
Ty : (Γ : Con) →           Set
Sub : (Γ Δ : Con) →         Set
Tm : (Γ : Con)(A : Ty Γ) → Set
There is a new keyword 'generalize', which accept declarations like
generalize
{Γ Δ Θ} : Con
{A B C} : Ty _
{σ δ ν} : Sub _ _
{t u v} : Tm _ _
After these 12 declarations
(1) Γ, Δ and Θ behave as Con-typed terms, but they are automatically
forall-generalized, so, for example
postulate
id : Sub Γ Γ
_∘_ : Sub Θ Δ → Sub Γ Θ → Sub Γ Δ
means
postulate
id : ∀ {Γ} → Sub Γ Γ
_∘_ : ∀ {Γ Δ Θ} → Sub Θ Δ → Sub Γ Θ → Sub Γ Δ
(2) A, B and C behaves as (Ty _)-typed terms (their types contain a
dedicated metavariable for each of them),
and they are also automatically forall-generalized.
For example,
postulate
_▹_ : ∀ Γ → Ty Γ → Con
π₁ : Sub Γ (Δ ▹ A) → Sub Γ Δ
means
_▹_ : ∀ Γ → Ty Γ → Con
π₁ : ∀{Γ Δ}{A : Ty Δ} → Sub Γ (Δ ▹ A) → Sub Γ Δ
(3) The metavariables of generalizable variables are also
automatically generalized.
For example,
postulate
ass : (σ ∘ δ) ∘ ν ≡ σ ∘ (δ ∘ ν)
means
postulate
ass   : ∀{Γ Δ Σ Ω}{σ : Sub Σ Ω}{δ : Sub Δ Σ}{ν : Sub Γ Δ}
        → ((σ ∘ δ) ∘ ν) ≡ (σ ∘ (δ ∘ ν))
(4) The place and order of generalized variables are fixed by the
A) generalized bindings are placed at the front of the type signature
B) the dependencies between the generalized variables are always respected
C) whenever possible, introduce A before B if A < B
- for non-metas, A < B if A was declared before B with a 'generalize'
keyword
- a meta is smaller than a non-meta
- for metas, A < B if A was declared before B with a 'generalize'
keyword. For example, σ : Sub _1 _2 was declared before δ : Sub _3 _4 so
instances of _1, _2, _3, _4 are ordered according to the indices.
----
- make type signatures shorter
- the type schema of generalizable variables helps
    to make even more guesses by the type system
- avoid accidental generalization
- only the given names are generalized
- the type of generalizable variables are checked
    against the given schema, which adds extra safety
- make generalized type signatures reliable
(the ordering, and also the naming, see later)
- What should be the keyword?
'notation' seems also good for me.
The idea behind 'notation' is that this language construct
makes informal sentences like "Let Γ Δ Θ denote contexts." formal.
Plans (not implemented yet)
- automatic generalization of record fields and constructor types
- allow 'generalize' keyword in submodules and between record fields
- make generalizable variables importable?
- 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.
https://github.com/divipp/agda
For Agda implementors
---------------------
The main patch is
https://github.com/divipp/agda/commit/d172d1ade15abe26be19311300f7d640563a6a57
- metavariables of generalizable variables are solved locally during
typechecking of terms and reverted later
- generalizable variables are stored in the signature as if they were
introduced by 'postulate'
The Generalize.agda file succeeds when I load it into emacs, but fails
if I call Agda directly. Somehow I could not filter out metavariables
introduced by 'generalize', so Agda tries to serialize them.
It would great if you could help me to let this feature in.
Best Regards,
Peter
_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda

Peter Divianszky

2018-04-02 12:03:35 UTC

Thanks for this test case too!
I'll add this also to the test suit.
I think it will be easy to fix this one.

Btw, I allowed issue tracking now on my fork:
https://github.com/divipp/agda/issues

My plan is to try to use gradually 'generalize' in a fork of std-lib.
I guess that would be a good overall test case.

Post by Martin Stone Davis
Respect the privacy of --generalize'd identifiers!
```
{-# OPTIONS --generalize #-}
postulate
Nat : Set
Fin : Nat → Set
module _ where
private
    generalize
      n : Nat
{-
    Using private here has no effect. Private applies only to
    declarations that introduce new identifiers into the module, like
    type signatures and data, record, and module declarations.
    when scope checking the declaration
      module _ where
-}
postulate foo : Fin n
postulate n : Nat
{-
Multiple definitions of n. Previous definition at
[snip]
when scope checking the declaration
n : Nat
-}
```

Post by Peter Divianszky
Dear Agda users and implementors,
I implemented a first version of forall-generalization, and I would
like to get feedback on it.
For users
---------
An example Agda file can be found at
https://github.com/divipp/agda/blob/master/test/Succeed/Generalize.agda
postulate
Con :                       Set
Ty : (Γ : Con) →           Set
Sub : (Γ Δ : Con) →         Set
Tm : (Γ : Con)(A : Ty Γ) → Set
There is a new keyword 'generalize', which accept declarations like
generalize
{Γ Δ Θ} : Con
{A B C} : Ty _
{σ δ ν} : Sub _ _
{t u v} : Tm _ _
After these 12 declarations
(1) Γ, Δ and Θ behave as Con-typed terms, but they are automatically
forall-generalized, so, for example
postulate
id : Sub Γ Γ
_∘_ : Sub Θ Δ → Sub Γ Θ → Sub Γ Δ
means
postulate
id : ∀ {Γ} → Sub Γ Γ
_∘_ : ∀ {Γ Δ Θ} → Sub Θ Δ → Sub Γ Θ → Sub Γ Δ
(2) A, B and C behaves as (Ty _)-typed terms (their types contain a
dedicated metavariable for each of them),
and they are also automatically forall-generalized.
For example,
postulate
_▹_ : ∀ Γ → Ty Γ → Con
π₁ : Sub Γ (Δ ▹ A) → Sub Γ Δ
means
_▹_ : ∀ Γ → Ty Γ → Con
π₁ : ∀{Γ Δ}{A : Ty Δ} → Sub Γ (Δ ▹ A) → Sub Γ Δ
(3) The metavariables of generalizable variables are also
automatically generalized.
For example,
postulate
ass : (σ ∘ δ) ∘ ν ≡ σ ∘ (δ ∘ ν)
means
postulate
ass   : ∀{Γ Δ Σ Ω}{σ : Sub Σ Ω}{δ : Sub Δ Σ}{ν : Sub Γ Δ}
        → ((σ ∘ δ) ∘ ν) ≡ (σ ∘ (δ ∘ ν))
(4) The place and order of generalized variables are fixed by the
A) generalized bindings are placed at the front of the type signature
B) the dependencies between the generalized variables are always respected
C) whenever possible, introduce A before B if A < B
- for non-metas, A < B if A was declared before B with a 'generalize'
keyword
- a meta is smaller than a non-meta
- for metas, A < B if A was declared before B with a 'generalize'
keyword. For example, σ : Sub _1 _2 was declared before δ : Sub _3 _4 so
instances of _1, _2, _3, _4 are ordered according to the indices.
----
- make type signatures shorter
- the type schema of generalizable variables helps
    to make even more guesses by the type system
- avoid accidental generalization
- only the given names are generalized
- the type of generalizable variables are checked
    against the given schema, which adds extra safety
- make generalized type signatures reliable
(the ordering, and also the naming, see later)
- What should be the keyword?
'notation' seems also good for me.
The idea behind 'notation' is that this language construct
makes informal sentences like "Let Γ Δ Θ denote contexts." formal.
Plans (not implemented yet)
- automatic generalization of record fields and constructor types
- allow 'generalize' keyword in submodules and between record fields
- make generalizable variables importable?
- 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.
https://github.com/divipp/agda
For Agda implementors
---------------------
The main patch is
https://github.com/divipp/agda/commit/d172d1ade15abe26be19311300f7d640563a6a57
- metavariables of generalizable variables are solved locally during
typechecking of terms and reverted later
- generalizable variables are stored in the signature as if they were
introduced by 'postulate'
The Generalize.agda file succeeds when I load it into emacs, but fails
if I call Agda directly. Somehow I could not filter out metavariables
introduced by 'generalize', so Agda tries to serialize them.
It would great if you could help me to let this feature in.
Best Regards,
Peter
_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda

_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda

Jesper Cockx

2018-05-18 12:13:39 UTC

Hi Peter,

First of all: thanks for working on this feature, this is something I (and
many other people it seems) have wished for many times. I think we should
aim to integrate it into the main Agda repository soon after the coming
release of Agda 2.5.4, so that we can release it in the next version of
Agda (either 2.5.5 or 2.6). That should give us plenty of time to address
the questions raised by Nisse and others, and give it some more testing
before we decide to release it. Could you please make a pull request
against the stable-2.5 branch on github.com/agda/agda? If there are any
problems I'd be glad to help. Thank you again!

-- Jesper

Post by Peter Divianszky
Dear Agda users and implementors,
I implemented a first version of forall-generalization, and I would like
to get feedback on it.
For users
---------
An example Agda file can be found at
https://github.com/divipp/agda/blob/master/test/Succeed/Generalize.agda
postulate
Con : Set
Ty : (Î : Con) â Set
Sub : (Î Î : Con) â Set
Tm : (Î : Con)(A : Ty Î) â Set
There is a new keyword 'generalize', which accept declarations like
generalize
{Î Î Î} : Con
{A B C} : Ty _
{Ï ÎŽ Îœ} : Sub _ _
{t u v} : Tm _ _
After these 12 declarations
(1) Î, Î and Î behave as Con-typed terms, but they are automatically
forall-generalized, so, for example
postulate
id : Sub Î Î
_â_ : Sub Î Î â Sub Î Î â Sub Î Î
means
postulate
id : â {Î} â Sub Î Î
_â_ : â {Î Î Î} â Sub Î Î â Sub Î Î â Sub Î Î
(2) A, B and C behaves as (Ty _)-typed terms (their types contain a
dedicated metavariable for each of them),
and they are also automatically forall-generalized.
For example,
postulate
_â¹_ : â Î â Ty Î â Con
Ïâ : Sub Î (Î â¹ A) â Sub Î Î
means
_â¹_ : â Î â Ty Î â Con
Ïâ : â{Î Î}{A : Ty Î} â Sub Î (Î â¹ A) â Sub Î Î
(3) The metavariables of generalizable variables are also automatically
generalized.
For example,
postulate
ass : (Ï â ÎŽ) â Îœ â¡ Ï â (ÎŽ â Îœ)
means
postulate
ass : â{Î Î Î£ Î©}{Ï : Sub Î£ Î©}{ÎŽ : Sub Î Î£}{Îœ : Sub Î Î}
â ((Ï â ÎŽ) â Îœ) â¡ (Ï â (ÎŽ â Îœ))
(4) The place and order of generalized variables are fixed by the
A) generalized bindings are placed at the front of the type signature
B) the dependencies between the generalized variables are always respected
C) whenever possible, introduce A before B if A < B
- for non-metas, A < B if A was declared before B with a 'generalize'
keyword
- a meta is smaller than a non-meta
- for metas, A < B if A was declared before B with a 'generalize' keyword.
For example, Ï : Sub _1 _2 was declared before ÎŽ : Sub _3 _4 so
instances of _1, _2, _3, _4 are ordered according to the indices.
----
- make type signatures shorter
- the type schema of generalizable variables helps
to make even more guesses by the type system
- avoid accidental generalization
- only the given names are generalized
- the type of generalizable variables are checked
against the given schema, which adds extra safety
- make generalized type signatures reliable
(the ordering, and also the naming, see later)
- What should be the keyword?
'notation' seems also good for me.
The idea behind 'notation' is that this language construct
makes informal sentences like "Let Î Î Î denote contexts." formal.
Plans (not implemented yet)
- automatic generalization of record fields and constructor types
- allow 'generalize' keyword in submodules and between record fields
- make generalizable variables importable?
- 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.
https://github.com/divipp/agda
For Agda implementors
---------------------
The main patch is
https://github.com/divipp/agda/commit/d172d1ade15abe26be1931
1300f7d640563a6a57
- metavariables of generalizable variables are solved locally during
typechecking of terms and reverted later
- generalizable variables are stored in the signature as if they were
introduced by 'postulate'
The Generalize.agda file succeeds when I load it into emacs, but fails if
I call Agda directly. Somehow I could not filter out metavariables
introduced by 'generalize', so Agda tries to serialize them.
It would great if you could help me to let this feature in.
Best Regards,
Peter
_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda

Peter Divianszky

2018-05-22 16:44:29 UTC