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

[Guillaume Brunerie]

Thanks, it does help a bit but not as much as I would have hoped.
I’ll keep on looking for where the problem is :)

Best,
Guillaume

Den ons 20 maj 2020 kl 09:05 skrev Andreas Abel <andreas.abel at ifi.lmu.de>:

>  > 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
> >
> _______________________________________________
> 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/20200522/fd6545d6/attachment.html>