Zulip Chat Archive

Stream: general

Topic: performance of `stream`

Yury G. Kudryashov (Oct 26 2021 at 20:13):

Once we move stream from core to mathlib (see #9988), I'm going to review stream API (there are some duplicates, lots of lemmas should be @[simp] etc). Since it is used in meta code, probably I should not make performance worse that it is now. So, I have a few questions:

  1. Is there an easy way to benchmark a single function? Something like %timeit in Jupyter notebooks.
  2. How much does Lean cache? E.g., if I have
    def f1 : ℕ → ℕ
    | 0 := 1
    | (n + 1) := f1 n + 5

    def g1 (f : ℕ → ℕ) : ∀ n, list ℕ
    | 0 := []
    | (n + 1) := g1 n ++ [f n]

    #eval g1 f1 10
    `` then how many times will it compute f 2`?

  3. Am I right that stream is designed to be used with recursively defined functions, so I should assume that stream.nth is probably not $O(1)$?

Mario Carneiro (Oct 26 2021 at 20:21):

I'm not aware of any code that uses stream. It is not particularly computationally efficient. Well, it's a function type, so it is as computationally efficient as the functions you use to build it, but if you just chain cons or something you will get linear time functions. Lean does not do any kind of memoization here, so a function is run exactly as many times as you call it. In your example, you call f1 9, f1 8, ..., f1 0, and each f1 n calls all previous values, so f1 2 is called a total of 8 times. You can verify this by putting trace in the computation of f1.

Yury G. Kudryashov (Oct 26 2021 at 20:23):

I saw an import data.streamin control.fix and assumed that it is used for some purpose.

Mario Carneiro (Oct 26 2021 at 20:23):

Ah, I suspected it might be Simon's doing. He likes FP style programs

Yury G. Kudryashov (Oct 26 2021 at 20:24):

Another file that imports data.stream is system.random.basic.

Yury G. Kudryashov (Oct 26 2021 at 20:25):

Am I right that I may refactor stream without computational complexity in mind?

Mario Carneiro (Oct 26 2021 at 20:27):

I tried commenting out everything that depends on stream in control.fix, control.lawful_fix, and system.random.basic and it seems that there are no other consequences in tactic, meta and system

Mario Carneiro (Oct 26 2021 at 20:30):

the material that is there is mostly theoretical, e.g. connecting it to omega-CPO's and part. I thought that it might get used by slim_check in its sampleable type class but the fact that commenting it out has no consequences says otherwise

Yury G. Kudryashov (Oct 26 2021 at 20:32):

Thank you!

Last updated: Aug 03 2023 at 10:10 UTC