<div dir="ltr">Thanks, it does help a bit but not as much as I would have hoped.<div>I’ll keep on looking for where the problem is :)</div><div><br></div><div>Best,</div><div>Guillaume</div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">Den ons 20 maj 2020 kl 09:05 skrev Andreas Abel <<a href="mailto:andreas.abel@ifi.lmu.de">andreas.abel@ifi.lmu.de</a>>:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"> > Could it be that this adds ~100 let-ins in the type of each of the <br>
fields?<br>
<br>
No, but it creates a new module which contains specializations of all <br>
the definitions in CCat+.  These will be positivity-checked.<br>
<br>
Could you check whether you can get some speedup by restricting to the <br>
actually needed imports?  Something like<br>
<br>
   open CCat+ ccat using (Ob; foo; bar) renaming (Mor to MorC)<br>
<br>
Best,<br>
Andreas<br>
<br>
On 2020-05-19 12:59, Guillaume Brunerie wrote:<br>
> Hello, (not sure if I should post that here or on the bug tracker)<br>
> <br>
> I’m trying to figure out why some project that I have been working on <br>
> requires as much memory as it does, and I have a specific question about <br>
> opening parameterized modules inside records.<br>
> <br>
> I know that inserting definitions between/before fields in a record <br>
> results to them being translated to let-ins in all the subsequent <br>
> fields, and I have learned recently (from issue #4331) that applying <br>
> parameterized modules simply generate a bunch of new functions for <br>
> everything exported by the module.<br>
> <br>
> Now I noticed the following code in my project, there are many other <br>
> similar pieces of code, but this is the simplest instance.<br>
> <br>
>     record CCatwithUU (ccat : CCat) : Set₁ where<br>
>        no-eta-equality<br>
>        open CCat+ ccat renaming (Mor to MorC) <br>
> <br>
>        field<br>
>          UUStr  : (i : ℕ) (Γ : Ob n) → Ob (suc n)<br>
>          UUStr= : {i : ℕ} {Γ : Ob n} → ft (UUStr i Γ) ≡ Γ<br>
>          UUStrNat' : {i : ℕ} (g : MorC n m) (Δ : Ob n) (g₀ : ∂₀ g ≡ Δ)<br>
>     (Γ : Ob m) (g₁ : ∂₁ g ≡ Γ)<br>
>                   → star g (UUStr i Γ) UUStr= g₁ ≡ UUStr i Δ<br>
> <br>
>        UUStrNat : {i : ℕ} {g : MorC n m} {Δ : Ob n} (g₀ : ∂₀ g ≡ Δ) {Γ :<br>
>     Ob m} {g₁ : ∂₁ g ≡ Γ}<br>
>                   → star g (UUStr i Γ) UUStr= g₁ ≡ UUStr i Δ<br>
>        UUStrNat g₀ {g₁ = g₁} = UUStrNat' _ _ g₀ _ g₁<br>
> <br>
> <br>
> It’s not very important what everything means, but the thing that I’m <br>
> worried about is that I apply and open the parameterized module CCat+ <br>
> (which is a rather big module, with ~100 definitions) before the fields <br>
> of the record.<br>
> <br>
> Could it be that this adds ~100 let-ins in the type of each of the fields?<br>
> I have quite a few (~30) similar records, more complicated than this <br>
> one, and which often open each other, so that could quickly explode.<br>
> <br>
> As a test, I duplicated the "open CCat+ ccat …" line 10 times inside the <br>
> record, and it took much longer to type check (5 seconds as opposed to <br>
> less than half a second), most of it on positivity checking.<br>
> <br>
> Thanks,<br>
> Best,<br>
> Guillaume<br>
> <br>
> _______________________________________________<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/mailman/listinfo/agda</a><br>
> <br>
_______________________________________________<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/mailman/listinfo/agda</a><br>
</blockquote></div>