[Agda] Performance: opening parameterized modules before the fields of a record

[Andreas Abel]

 > Could it be that this adds ~100 let-ins in the type of each of the 
fields?

No, but it creates a new module which contains specializations of all 
the definitions in CCat+.  These will be positivity-checked.

Could you check whether you can get some speedup by restricting to the 
actually needed imports?  Something like

   open CCat+ ccat using (Ob; foo; bar) renaming (Mor to MorC)

Best,
Andreas

On 2020-05-19 12:59, Guillaume Brunerie wrote:
> Hello, (not sure if I should post that here or on the bug tracker)
> 
> I’m trying to figure out why some project that I have been working on 
> requires as much memory as it does, and I have a specific question about 
> opening parameterized modules inside records.
> 
> I know that inserting definitions between/before fields in a record 
> results to them being translated to let-ins in all the subsequent 
> fields, and I have learned recently (from issue #4331) that applying 
> parameterized modules simply generate a bunch of new functions for 
> everything exported by the module.
> 
> Now I noticed the following code in my project, there are many other 
> similar pieces of code, but this is the simplest instance.
> 
>     record CCatwithUU (ccat : CCat) : Set₁ where
>        no-eta-equality
>        open CCat+ ccat renaming (Mor to MorC) 
> 
>        field
>          UUStr  : (i : ℕ) (Γ : Ob n) → Ob (suc n)
>          UUStr= : {i : ℕ} {Γ : Ob n} → ft (UUStr i Γ) ≡ Γ
>          UUStrNat' : {i : ℕ} (g : MorC n m) (Δ : Ob n) (g₀ : ∂₀ g ≡ Δ)
>     (Γ : Ob m) (g₁ : ∂₁ g ≡ Γ)
>                   → star g (UUStr i Γ) UUStr= g₁ ≡ UUStr i Δ
> 
>        UUStrNat : {i : ℕ} {g : MorC n m} {Δ : Ob n} (g₀ : ∂₀ g ≡ Δ) {Γ :
>     Ob m} {g₁ : ∂₁ g ≡ Γ}
>                   → star g (UUStr i Γ) UUStr= g₁ ≡ UUStr i Δ
>        UUStrNat g₀ {g₁ = g₁} = UUStrNat' _ _ g₀ _ g₁
> 
> 
> It’s not very important what everything means, but the thing that I’m 
> worried about is that I apply and open the parameterized module CCat+ 
> (which is a rather big module, with ~100 definitions) before the fields 
> of the record.
> 
> Could it be that this adds ~100 let-ins in the type of each of the fields?
> I have quite a few (~30) similar records, more complicated than this 
> one, and which often open each other, so that could quickly explode.
> 
> As a test, I duplicated the "open CCat+ ccat …" line 10 times inside the 
> record, and it took much longer to type check (5 seconds as opposed to 
> less than half a second), most of it on positivity checking.
> 
> Thanks,
> Best,
> Guillaume
> 
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>