[Agda] new generalize feature, first version

[Jesper Cockx]

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? 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> 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/d172d1ade15abe26be1931
> 1300f7d640563a6a57
>
> 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
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20180518/075be92a/attachment.html>