Data.Nat.Show.show is really slow for large numbers

[Taneb]

A little while ago I was experimenting with a faster definition for Data.Nat.Base._^_. When I came to actually time my code, however, I couldn't see any difference between the execution time. I profiled, and execution was absolutely dominated by show (as I was printing the results to ensure they were forced).

Data.Nat.Show.show is defined using Data.Digit.toNatDigits, which in turn uses repeated division by the base. This is quadratic in the number of digits, and slow for huge numbers in practice.

I compared how GHC implements show for Integer, which seemed to be much faster, and was surprised by how complex the implementation is. Disregarding details concerning sign and precedence, which isn't relevant to us here, it uses a divide-and-conquer method to split the number into 10^k sized blocks, with k chosen as large as possible such that 10^k is less than machine word size (with, presumably, faster division). These blocks are then converted to strings using repeated division and concatenated.

Would such an approach work for us, and would it be faster?

[Taneb]

I wrote this to try it out and it seems much faster:

{-# OPTIONS --without-K #-}

module NatShow where

open import Data.Nat.Base
open import Data.List.Base
-- open import Data.Product.Base


open import Data.Nat.DivMod
open import Data.Nat.Properties
open import Relation.Nullary

jsplitb : (base : ℕ) → .{{_ : NonZero base}} → List ℕ → List ℕ
jsplitb base [] = []
jsplitb base (n ∷ ns) = n / base ∷ n % base ∷ jsplitb base ns

-- maybe this should take a nonempty list?
jsplith : (base : ℕ) → .{{_ : NonZero base}} → List ℕ → List ℕ
jsplith base [] = []
jsplith base (n ∷ ns) with n / base
... | 0 = n % base ∷ jsplitb base ns
... | q@(suc _) = q ∷ n % base ∷ jsplitb base ns

{-# TERMINATING #-}
toNatDigits : (base : ℕ) → .{{_ : NonTrivial base}} → ℕ → List ℕ
toNatDigits base n with n <? base
... | yes n<base = [ n ]
... | no  n≮base = jsplith base {{nonTrivial⇒nonZero base}} (toNatDigits (base * base) {{m≢0∧n>1⇒m*n>1 base base {{nonTrivial⇒nonZero base}}}} n)

open import Data.String.Base using (String; fromList)

import Data.Nat.Show as S

show′ : ℕ → String
show′ n = fromList (map S.toDigitChar (toNatDigits 10 n))

[gallais]

Related: #678, #687

[jamesmckinna]

And, less importantly, #2218 homes in on some intrinsic inefficiencies in Data.Digit: wrt the code above

jsplith base (n ∷ ns) with n / base
... | 0 = n % base ∷ jsplitb base ns
... | q@(suc _) = q ∷ n % base ∷ jsplitb base ns

Am I (not?) right in thinking that in the 0 clause, if n / base is 0, then already n < base , so that

... | 0 = n ∷ jsplitb base ns

would suffice?

[Taneb]

Yes, you're right. I was mostly adapting the Haskell implementation, which does a divMod and then checks, so it already has the n % base handy in that branch. But that code snippet I intend to be more of a proof of concept than what gets merged into the library

[JacquesCarette]

Certainly working on "big blocks" is going to be quite a bit faster. This is old (very old) wisdom from the implementation of CAS. Especially for compilers, mapping down to hardware instructions makes a world of difference.

I'm pretty sure that for really large numbers (100,000 digits), the fastest operation is actually to start 'at the top' and chop down as quickly as possible. Logarithms are your friends wrt to estimating ahead of time how many digits your number has, and so what kind of strides to take.