[Agda] expensive `with'

[James Wood]

Hi Sergei,

I think 
https://agda.readthedocs.io/en/latest/language/with-abstraction.html#performance-considerations 
gives a nice concise overview of the likely performance issues for 
`with`. Most depend on the type of the goal and context (i.e, the type 
signature of the function you're writing) more than the expression being 
abstracted. A simple test is to abstract over, say, `tt` of type `⊤` and 
see how long that takes.

It is true that using `case` rather than `with` can alleviate a lot of 
performance issues, simply because it does less work. Sometimes `case` 
is not good enough, but you can still avoid `with` by manually 
desugaring the with-abstraction (as described in the Technical details 
section of the same documentation page). This technique is sometimes 
called “rolling one's own `with`”.

All the best,
James

On 11/01/2021 19:16, mechvel at scico.botik.ru wrote:
> CAUTION: This email originated outside the University. Check before 
> clicking links or attachments.
> 
> Dear Agda developers,
> 
> I have the code fragment
> 
> ------------------------------------------------------------
>        ... | yes hmS | yes hmF₂ =  inj₂ (hmS , degS≤k)
>               where
>               open ≤-Reasoning
>               s       = f₁+f₂
>               degF₂   = deg f₂ hmF₂
> 
>               degF₂≤k : degF₂ ≤ k
>               degF₂≤k = <⇒≤ (degF₂<k hmF₂)
> 
>               degS≤k : deg s hmS ≤ k
>               degS≤k = case deg[f+g]≤max f₁ f₂ hmF₁ hmF₂
>                        of \
>                        { (inj₁ nullS) → contradiction hmS
>                                                (null⇒¬HasMon {s} nullS)
>                        ; (inj₂ (hmS' , degS'≤degF₁⊔degF₂)) →
>                            begin deg f₁+f₂ hmS   ≡⟨ refl ⟩
>                                  deg f₁+f₂ hmS'  ≤⟨ degS'≤degF₁⊔degF₂ ⟩
>                                  degF₁ ⊔ degF₂   ≤⟨ ⊔-least degF₁≤k
> degF₂≤k ⟩
>                                  k
>                            ∎
>                        }
> -----------------------------------------------------------
> 
> where the file is type-checked in 1 minute (on a 3 GHz machine).
> 
> Initially, there was `with' instead of the last `case'.
> And 20 minutes was not enough.
> Then I set types explicitly in most places and also change the last
> `case` with
>                      with deg[f+g]≤max f₁ f₂ hmF₁ hmF₂
>                  ... | inj₁ _ = anything
>                  ... | inj₂ _ = anything
> 
> After 25 minutes it reports
> Checking ... .agda).
> agda: Heap exhausted;
> agda: Current maximum heap size is 3758096384 bytes (3584 MB).
> 
> The `top' command shows that after 5 minutes about 3 Gb is taken by
> Agda,
> then it stops eating memory, and finally breaks by heap.
> 
> I tend to think that when the type checker becomes very slow, it is
> desirable
> to use `case' rather than `with' in the responsible code.
> 
> Can people, please, comment?
> 
> ------
> Sergei
> 
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda 
>