<div dir="ltr"><div>Hi Peter,</div><div><br></div><div>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 <a href="http://github.com/agda/agda" target="_blank">github.com/agda/agda</a>? If there are any problems I'd be glad to help. Thank you again!<br></div><div><br></div><div>-- Jesper</div><br><div class="gmail_extra"><br><div class="gmail_quote">On Thu, Mar 29, 2018 at 2:13 PM, Peter Divianszky <span dir="ltr"><<a href="mailto:divipp@gmail.com" target="_blank">divipp@gmail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Dear Agda users and implementors,<br>
<br>
I implemented a first version of forall-generalization, and I would like to get feedback on it.<br>
<br>
<br>
For users<br>
---------<br>
<br>
An example Agda file can be found at<br>
<a href="https://github.com/divipp/agda/blob/master/test/Succeed/Generalize.agda" rel="noreferrer" target="_blank">https://github.com/divipp/agda<wbr>/blob/master/test/Succeed/Gene<wbr>ralize.agda</a><br>
<br>
Suppose that the following Set formers were postulated:<br>
<br>
postulate<br>
  Con :                       Set<br>
  Ty  : (Γ : Con) →           Set<br>
  Sub : (Γ Δ : Con) →         Set<br>
  Tm  : (Γ : Con)(A : Ty Γ) → Set<br>
<br>
There is a new keyword 'generalize', which accept declarations like 'field' for records:<br>
<br>
generalize<br>
  {Γ Δ Θ} : Con<br>
  {A B C} : Ty _<br>
  {σ δ ν} : Sub _ _<br>
  {t u v} : Tm _ _<br>
<br>
After these 12 declarations<br>
<br>
(1) Γ, Δ and Θ behave as Con-typed terms, but they are automatically forall-generalized, so, for example<br>
<br>
postulate<br>
  id  : Sub Γ Γ<br>
  _∘_ : Sub Θ Δ → Sub Γ Θ → Sub Γ Δ<br>
<br>
means<br>
<br>
postulate<br>
  id  : ∀ {Γ} → Sub Γ Γ<br>
  _∘_ : ∀ {Γ Δ Θ} → Sub Θ Δ → Sub Γ Θ → Sub Γ Δ<br>
<br>
(2) A, B and C behaves as (Ty _)-typed terms (their types contain a dedicated metavariable for each of them),<br>
and they are also automatically forall-generalized.<br>
For example,<br>
<br>
postulate<br>
  _▹_ : ∀ Γ → Ty Γ → Con<br>
  π₁ : Sub Γ (Δ ▹ A) → Sub Γ Δ<br>
<br>
means<br>
  _▹_ : ∀ Γ → Ty Γ → Con<br>
  π₁ : ∀{Γ Δ}{A : Ty Δ} → Sub Γ (Δ ▹ A) → Sub Γ Δ<br>
<br>
(3) The metavariables of generalizable variables are also automatically generalized.<br>
For example,<br>
<br>
postulate<br>
  ass : (σ ∘ δ) ∘ ν ≡ σ ∘ (δ ∘ ν)<br>
<br>
means<br>
<br>
postulate<br>
  ass   : ∀{Γ Δ Σ Ω}{σ : Sub Σ Ω}{δ : Sub Δ Σ}{ν : Sub Γ Δ}<br>
        → ((σ ∘ δ) ∘ ν) ≡ (σ ∘ (δ ∘ ν))<br>
<br>
(4) The place and order of generalized variables are fixed by the following rules:<br>
<br>
A) generalized bindings are placed at the front of the type signature<br>
B) the dependencies between the generalized variables are always respected<br>
C) whenever possible, introduce A before B if A < B<br>
- for non-metas, A < B if A was declared before B with a 'generalize' keyword<br>
- a meta is smaller than a non-meta<br>
- 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<br>
instances of _1, _2, _3, _4 are ordered according to the indices.<br>
<br>
----<br>
<br>
The design goals were the following:<br>
<br>
- make type signatures shorter<br>
  - the type schema of generalizable variables helps<br>
    to make even more guesses by the type system<br>
- avoid accidental generalization<br>
  - only the given names are generalized<br>
  - the type of generalizable variables are checked<br>
    against the given schema, which adds extra safety<br>
- make generalized type signatures reliable<br>
  (the ordering, and also the naming, see later)<br>
<br>
Question:<br>
<br>
- What should be the keyword?<br>
  'notation' seems also good for me.<br>
  The idea behind 'notation' is that this language construct<br>
  makes informal sentences like "Let Γ Δ Θ denote contexts." formal.<br>
<br>
Plans (not implemented yet)<br>
<br>
- automatic generalization of record fields and constructor types<br>
- allow 'generalize' keyword in submodules and between record fields<br>
- make generalizable variables importable?<br>
- 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.<br>
<br>
You can try the current implementation with my fork:<br>
<a href="https://github.com/divipp/agda" rel="noreferrer" target="_blank">https://github.com/divipp/agda</a><br>
<br>
<br>
For Agda implementors<br>
---------------------<br>
<br>
The main patch is<br>
<br>
<a href="https://github.com/divipp/agda/commit/d172d1ade15abe26be19311300f7d640563a6a57" rel="noreferrer" target="_blank">https://github.com/divipp/agda<wbr>/commit/d172d1ade15abe26be1931<wbr>1300f7d640563a6a57</a><br>
<br>
It contains several hacks, I'm not sure that this is the right thing to do:<br>
- metavariables of generalizable variables are solved locally during typechecking of terms and reverted later<br>
- generalizable variables are stored in the signature as if they were introduced by 'postulate'<br>
<br>
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.<br>
<br>
It would great if you could help me to let this feature in.<br>
<br>
<br>
Best Regards,<br>
<br>
Peter<br>
______________________________<wbr>_________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mail<wbr>man/listinfo/agda</a><br>
</blockquote></div><br></div></div>