[Agda] interactive Bin arith performance

[Sergei Meshveliani]

On Fri, 2019-02-01 at 11:44 +0100, Ulf Norell wrote:
> 
> 
> 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).
>  

?!
Thank you.
So, to run the code in interpreter, it is highly desirable to replace
  
                                    let foo = foo1 in foo2
with
     case foo1 of \ { foo -> foo2 }

everywhere in the application?

And   
  let (a , b) = f x
      (c , d) = g x a
      e       = h c
  in
  f1 a c e

to replace with

   case f x of \ { (a , b) -> case g x a 
                              of \ 
                              { (c , d) -> case h c 
                                           of \ 
                                           { e -> f1 a c e }
                              }
                 }
?

>         
>         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.
> 

Somehow unneeded code for the goal evaluation ...

To use some library of provers, like say RingSolver, these prover
functions need to be interpreted during type check.
Right?

Concerning this, is it a hard problem to enable the Agda interpreter to
run a compiled code?

Thank you for explanations,

------
Sergei