[Agda] new generalize feature, first version
Peter Divianszky
divipp at gmail.com
Tue May 22 18:44:29 CEST 2018
Hi Jesper,
I unified and rebased my patches on top of the current stable-2.5 branch.
I made a pull request, and I described in the pull request what is
missing from my implementation:
https://github.com/agda/agda/pull/3071
It would be great if you could help in any of the issues described there.
I am ready to add more documentation to my code if needed.
Cheers,
Peter
On 2018-05-18 14:13, Jesper Cockx wrote:
> Hi Peter,
>
> First of all: thanks for working on this feature, this is something I
> (and many other people it seems) have wished for many times. I think we
> should aim to integrate it into the main Agda repository soon after the
> coming release of Agda 2.5.4, so that we can release it in the next
> version of Agda (either 2.5.5 or 2.6). That should give us plenty of
> time to address the questions raised by Nisse and others, and give it
> some more testing before we decide to release it. Could you please make
> a pull request against the stable-2.5 branch on github.com/agda/agda
> <http://github.com/agda/agda>? If there are any problems I'd be glad to
> help. Thank you again!
>
> -- Jesper
>
>
> On Thu, Mar 29, 2018 at 2:13 PM, Peter Divianszky <divipp at gmail.com
> <mailto: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
> <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
> <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 <mailto:Agda at lists.chalmers.se>
> https://lists.chalmers.se/mailman/listinfo/agda
> <https://lists.chalmers.se/mailman/listinfo/agda>
>
>
More information about the Agda
mailing list