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.

[linyue0103]

679 _safe

module base where

open import Funnction public using(id:$$-**）

Eq public using（—=——；refl)

[jamesmckinna]

@linyue0103 not sure I understand your comment, nor how it applies to this issue?

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