`Nat` too slow in the evaluator

[rgrover]

A simple recursion to compute half of a natural number is expensive to execute on Idris2.

Steps to Reproduce

Executing half (in the following code) scales super-linearly with the argument.

import Data.Vect
import Data.Nat -- remove this for Idris1

-- View for dividing a Nat in half; taken literally from libs/base/Data/Nat/Views.idr (Idris1)
data Half : Nat -> Type where
     HalfOdd : {n : Nat} -> Half (S (n + n))
     HalfEven : {n : Nat} -> Half (n + n)

-- Covering function for the `Half` view
half : (n : Nat) -> Half n
half Z = HalfEven {n=Z}
half (S k) with (half k)
  half (S (h + h)) | HalfEven = HalfOdd
  half (S (S (h + h))) | HalfOdd =
    let result = HalfEven {n = S h} in
      rewrite plusSuccRightSucc h h in result

Expected Behavior

The time complexity should be at most linear in n (or faster). The same on Idris1 was almost instantaneous.

Observed Behavior

half 40 took more than 20 seconds on my laptop.

[rgrover]

A straightforward recursive implementation of half also takes super-linear time to execute:

half : (n : Nat) -> Nat
half = go 0
  where
    go : (acc : Nat) -> (x: Nat) -> Nat
    go acc Z = acc
    go acc (S k) =
      case k of
        Z => acc
        S j => go (S acc) j

half 1000 took around 1 second half 2000 took around 5 seconds half 4000 took around 20 seconds

In this case, the slowdown was also observed with Idris1.

[rgrover]

The following code, which transfers one counter into another has the same poor performance as half above.

construct : (n : Nat) -> Nat
construct = go Z
  where
    go : (acc: Nat) -> (x: Nat) -> Nat
    go acc 0 = acc
    go acc (S k) = go (S acc) k

This tells me that perhaps there is a quadratic cost for constructing Nats. The S operator could be quadratic.

Can someone please point me towards resources I could use to investigate further?

[fabianhjr]

Hi @rgrover, in idris 0.9.10 and subsequent releases of Idris1 there was work to optimize "nat like" data types to GMP Integers (Unbounded big integers): https://github.com/idris-lang/Idris-dev/blob/53f6fc98b1dbedd2536eba58104c6f78f62252a6/CHANGELOG.md#new-in-0910

There is also this useful note: https://github.com/idris-lang/Idris-dev/blob/master/docs/reference/erasure.rst

[fabianhjr]

Here is how Agda does it for nat:

https://github.com/agda/agda/blob/master/src/data/lib/prim/Agda/Builtin/Nat.agda

They use annotations on the data type / function declarations like so:

data Nat : Set where
  zero : Nat
  suc  : (n : Nat) → Nat

{-# BUILTIN NATURAL Nat #-}

And the translation to more efficient implementations is implemented in their compiler here:

https://github.com/agda/agda/blob/master/src/full/Agda/Syntax/Builtin.hs https://github.com/agda/agda/blob/master/src/full/Agda/TypeChecking/Monad/Builtin.hs

[ziman]

It seems that this applies only to the REPL. Running construct 4000 takes a long time but running :exec printLn $ construct 4000 doesn't.

On my machine, compiled construct seems to be faster and linear:

• printLn $ construct 200000000 — real 0m0.609s
• printLn $ construct 400000000 — real 0m1.048s
• printLn $ construct 800000000 — real 0m1.940s
• printLn $ construct 1600000000 — real 0m3.727s

So there's something in the evaluator that makes this slow. I'll edit the title of the issue.

@fabianhjr thanks for the suggestions but this seems to be an evaluator-only issue so it does not matter how you compile Nats. (And Idris 2 already compiles Nats to GMP integers, anyway.)

[ziman]

time echo 'construct 500' | idris2 -q x.idr
real    0m0.506s

time echo 'construct 1000' | idris2 -q x.idr
real    0m1.768s

time echo 'construct 1500' | idris2 -q x.idr
real    0m3.960s

time echo 'construct 2000' | idris2 -q x.idr
real    0m7.101s

[fabianhjr]

Oh my, I didn't know Idris2 already erased/squashed into a GMP Integer, thanks for the info @ziman. I am also interested in investigating this, could you point me to where that happens in Idris2?

[ziman]

https://github.com/edwinb/Idris2/blob/master/src/Compiler/CompileExpr.idr#L131

[edwinb]

The compile time evaluator, that you get at the REPL, is optimised for suspending evaluation when it's not necessary during type checking. The Idris 1 evaluator, on the the other hand, is faster at evaluating to normal forms - that is, it doesn't try to suspend under lambdas/constructors, which is nice for faster evaluation, but wastes a lot of time during type checking. As a result, getting normal forms at the REPL is quite a bit faster in Idris 1.

Not that I know exactly why you get that complexity, having not looked closely yet. But that is at least the reason Idris 2 is slower at this sort of thing. We could add another evaluator just for this purpose, although you'd still get the same time complexity. It might be useful in any case.

Optimising Nats at compile time is possibly worth it, though I've not yet seen a program where it's been the bottleneck (I'm sure such programs exist).

[edwinb]

I've just converted this to a function on Integer and got exactly the same strange performance, which means that this is likely nothing to do with Nat and leads me to wonder if there is some weird complexity problem in the evaluator that nobody has spotted until now. I will investigate.

[edwinb]

Yes, it turns out, there was a weird complexity problem in the evaluator: evaluating the variable being inspected in a 'case', but not caching the result, so recomputing it many times.

Most of the cost in the evaluator is from converting the Integer to the Nat in the first place (try timing the Nat 2000 for example, the comparing against construct 2000. In the first half, though, you're also doing a rewrite and at compile time, it will construct the proof to check that it really is a proof before completing the rewrite. So that'll add up.