[Agda] interactive Bin arith performance

[Ulf Norell]

On Fri, Feb 1, 2019 at 10:50 AM Sergei Meshveliani <mechvel at botik.ru> wrote:

> Can anybody, please, explain what is happening in the below simple and
> self-contained example?
>
> -----------------------------------------------------------------
> f : (m : ℕ) → ∃ (\n → n ≤ m)
>
> f 0       =  (0 , ≤-refl)
> f (suc m) =  let (n , n≤m) = f m
>              in
>              case suc n ≤? m of \
>                              { (yes _) → (n , ≤-step n≤m)
>                              ; (no _ ) → (suc n , s≤s n≤m) }
>
> g = proj₁ ∘ f
> -----------------------------------------------------------------
>
> emacs,   C-c C-l
>              g 22
>
> is evaluated in  25 sec.
>

In this case the problem isn't proof evaluation, but the 'let' which
doesn't share
evaluation of the right-hand side. This means that every occurrence of `n`
corresponds to a new call to `f`, making it exponential. If you change `f`
to

f 0       =  (0 , ≤-refl)
f (suc m) =
  case f m of λ where
    (n , n≤m) →
             case suc n ≤? m of \
                             { (yes _) → (n , ≤-step n≤m)
                             ; (no _ ) → (suc n , s≤s n≤m) }

it runs fast (or as fast as the unary implementation of ≤? allows).


> Still the evaluation cost of the compiled code looks as quadratic.
> I think, this is because  k ≤? l  is solved  m  times for  k  having  k
> `suc' constructors for  k = 0, ..., m.
>

Indeed. _≤?_ is linear in the value of the first argument.


> Does the compiled  g  evaluate proofs?
> If not, then who has removed the  proof evaluation part (PEP)
> from the code?
>
> Type checking produces  Foo.agdai  which has PEP,
> MAlonzo takes Foo.agdai, compiles to Haskell with removing the PEP,
> and  Foo.hs  does not have PEP
> -- is this so?


Essentially yes, but the erasure actually happens when compiling the type
checked code to an intermediate language (called treeless), which the GHC
backend then turns into Haskell code.

Also it's a bit misleading to talk about proof evaluation, since there is no
clear distinction between proofs and terms in Agda.

/ Ulf
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20190201/3062c15e/attachment.html>