Peter Divianszky

2018-03-29 12:13:48 UTC

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

https://github.com/divipp/agda/commit/d172d1ade15abe26be19311300f7d640563a6a57

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

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

https://github.com/divipp/agda/commit/d172d1ade15abe26be19311300f7d640563a6a57

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