Data.List.upTo/applyUpTo can be made faster

[Taneb]

In a quick experiment, the following definition runs circles around the current implementation of upTo

goUpTo : ℕ → ℕ → List ℕ
goUpTo _ 0 = []
goUpTo n (suc i) = n ∷ goUpTo (suc n) i

upTo′ : ℕ → List ℕ
upTo′ = goUpTo 0

I suspect this is because applyUpTo builds huge closures.

[jamesmckinna]

(Deleted my original comment, but now reinstating it) Can the implementation be further improved/speeded-up by considering a tail-call optimisation?

[Taneb]

Can the implementation be further improved/speeded-up by considering a tail-call optimisation?

I don't think so. The recursion here is already guarded behind a constructor. I don't know what a tail recursive implementation would look like.

[MatthewDaggitt]

Yes, I never had performance in mind when I add any of my definitions. Apologies! There's probably plenty more of these lurking in the library...

[jamesmckinna]

So...: instead have

upTo : ℕ → List ℕ
upTo = go 0
  module UpTo where
    go : ℕ → ℕ → List ℕ
    go _ zero    = []
    go n (suc i) = n ∷ go (suc n) i

downFrom : ℕ → List ℕ
downFrom zero    = []
downFrom (suc n) = n ∷ downFrom n

to avoid building the closures in applyUpTo/applyDownFrom? or is it easier simply to compute downFrom, and then compute upTo = reverse ∘ downFrom?

allFin seems trickier, because the closures, even if only specialised to powers of suc, do seem necessary? (although the reverse trick would again avoid such unpleasantness? UPDATED: er, no?)

Not clear what the knock-on effects on Data.List.Properties might be, but ...