[Agda] new generalize feature, first version

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

Thorsten

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

    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
    _______________________________________________
    Agda mailing list
    Agda at lists.chalmers.se
    https://lists.chalmers.se/mailman/listinfo/agda
    




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

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