[Agda] new generalize feature, first version

Martin Stone Davis martin.stone.davis at gmail.com
Sun Apr 1 15:01:54 CEST 2018


Peter, many accolades to you for developing and sharing. Now for the 
complaints!

My trouble is shown in the code below, which is failing on the last 
line. Is this a bug in the new feature?

```
{-# OPTIONS --generalize #-}

postulate
   Class : Set -> Set
   method : {X : Set} {{_ : Class X}} -> X -> Set
   Nat : Set
   Fin : Nat -> Set

generalize
   {n} : Nat
   {x} : Fin _

postulate
   instance ClassFin : Class (Fin n)
   works1 : {x : Fin n} -> method x
   works2 : method {{ClassFin}} x
   works3 : method {X = Fin n} x
   fails  : method x
{-
Unsolved meta not generalized
when checking that the expression method x has type Set _22
-}
```

On 03/29/2018 05:13 AM, Peter Divianszky 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



More information about the Agda mailing list