[Agda] new generalize feature, first version

[Peter Divianszky]

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.


On 2018-04-02 03:01, Martin Stone Davis wrote:
> 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
> -}
> ```
> 
> 
> On 03/29/2018 05:13 AM, Peter Divianszky wrote:
>> 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
>> _______________________________________________
>> Agda mailing list
>> Agda at lists.chalmers.se
>> https://lists.chalmers.se/mailman/listinfo/agda
> 
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda