[Agda] new generalize feature, first version

[Martin Escardo]

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

On 29/03/18 13:13, divipp at gmail.com 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

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