Discussion:
new generalize feature, first version
Peter Divianszky
2018-03-29 12:13:48 UTC
Raw Message
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

Suppose that the following Set formers were postulated:

postulate
Con : Set
Ty : (Γ : Con) → Set
Sub : (Γ Δ : Con) → Set
Tm : (Γ : Con)(A : Ty Γ) → Set

There is a new keyword 'generalize', which accept declarations like
'field' for records:

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
following rules:

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.

----

The design goals were the following:

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

Question:

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

You can try the current implementation with my fork:
https://github.com/divipp/agda

For Agda implementors
---------------------

The main patch is

It contains several hacks, I'm not sure that this is the right thing to do:
- 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
Nils Anders Danielsson
2018-03-29 16:23:31 UTC
Raw Message
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
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 ≡ _
Post by Peter Divianszky
- 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.
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
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}
--
Peter Divianszky
2018-03-30 08:25:42 UTC
Raw Message
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.
first example) and generalize with meta (like in your second example) is
valid.

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

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 Nils Anders Danielsson
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
Raw Message
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
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.
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
--
Peter Divianszky
2018-03-30 20:27:36 UTC
Raw Message
Post by Nils Anders Danielsson
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 Nils Anders Danielsson
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
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.
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
Raw Message
Post by Peter Divianszky
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.
--
Peter Divianszky
2018-03-30 22:00:35 UTC
Raw Message
Post by Nils Anders Danielsson
Post by Peter Divianszky
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 Nils Anders Danielsson
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
Post by Peter Divianszky
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.
Nils Anders Danielsson
2018-03-31 09:58:01 UTC
Raw Message
Post by Peter Divianszky
Post by Nils Anders Danielsson
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.
Post by Peter Divianszky
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.
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 [...]
--
Arseniy Alekseyev
2018-03-31 12:19:59 UTC
Raw Message
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.
Post by Nils Anders Danielsson
Post by Peter Divianszky
Post by Nils Anders Danielsson
{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 [...]
--
_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda
Peter Divianszky
2018-03-31 19:11:34 UTC
Raw Message
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 [...]
--
_______________________________________________
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
Raw Message
Post by Nils Anders Danielsson
Post by Peter Divianszky
Post by Nils Anders Danielsson
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 Nils Anders Danielsson
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 Nils Anders Danielsson
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
Raw Message
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

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.
--
Peter Divianszky
2018-03-30 21:46:01 UTC
Raw Message
Post by Nils Anders Danielsson
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 Nils Anders Danielsson
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.
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
Raw Message
Hi,
Post by Nils Anders Danielsson
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

Cheers,
Joachim
--
Joachim Breitner
***@joachim-breitner.de
http://www.joachim-breitner.de/
Jannis Limperg
2018-03-30 15:17:39 UTC
Raw Message
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
the Coq implementors chose to do so.

An example:

Generalizable Variables A.

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

(* 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
Raw Message
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
That's a good point.
--
Martin Escardo
2018-03-29 16:47:20 UTC
Raw Message
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
- 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
Raw Message
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
- 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
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
Raw Message
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
Raw Message
I agree with Nils points,

i think that it is better to return an error if you try to generalize a

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

- 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
Raw Message
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
- 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
Raw Message
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
- 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
Raw Message
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 Γ Δ
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
(because Coq website ( https://coq.inria.fr/ ) seems down).
--
Andrés
Peter Divianszky
2018-04-01 18:04:24 UTC
Raw Message
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.
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 Γ Δ
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
(because Coq website ( https://coq.inria.fr/ ) seems down).
Nils Anders Danielsson
2018-04-01 19:38:28 UTC
Raw Message
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.)
--
Martin Stone Davis
2018-04-02 01:01:36 UTC
Raw Message
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
- 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
Raw Message
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
- 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